2.2.7 几何定理证明和数学机械化

哥德尔证明一阶整数（算术）是不可判定的，但几乎同时塔尔斯基则证明一阶实数（初等几何和代数）是可判定的。塔尔斯基的结果意味着可以存在算法能对所有初等几何和代数问题给出证明。但塔尔斯基的原始算法是超指数的，被后人多次改进后仍然很难被当作通用

算法。数学家吴文俊受到中国数学思想的启发，针对某一大类的初等几何问题给出了高效的算法。后来又将这种方法推广到一类微分几何问题上。

在定理证明的早期，研究者追求“一招鲜吃遍天”，即找到一个超级算法能证明所有问题，最典型的例子是归结方法和 superposition。王浩不认可这种思路，他认为他自己的早期工作和吴文俊的方法都表明最有效的方法是先找对一个相对可控的子领域，然后针对这个子领域的特性，找到有效的算法。

吴文俊院士喜欢用“数学机械化”而不是“机器定理证明”来描述自己的工作。笛卡儿认为代数使得数学机械化，因此使得思考和计算步骤变得容易，无须花很大脑力。小学算术很难的题目，在初中代数中通过方程很容易被解决。每一次数学的突破，往往以脑力劳动的机械化来体现。

王浩和吴文俊是在人工智能领域做出突出贡献的中国人。