德国大数学家大卫·希尔伯特（David Hilbert，1862—1943）在 1899 年出版的著作《几何基础》里成功地建立了欧氏几何的形式化的、严谨的公理体系，重新塑造了欧氏几何的数学基础，现在称为“希尔伯特公理体系”。随后他还提出了著名的希尔伯特计划—号召全世界数学家一起来将所有的数学真理形式化，让每一个数学陈述都能用符号表达出来，让每一个数学家都能用定义好的规则来处理这些已经变成符号的陈述，在这个基础上再去证明数学是完整的，这里的“完整”就是说所有真的陈述都能被证明，这被称为数学的完备性；然后，再证明数学是一致的，也就是说不会推出自相矛盾的陈述，这被称为数学的一致性。当时几乎全世界的数学家都相信完备性和一致性是数学必定具有的，但是后来希尔伯特计划的美好愿景被哥德尔彻底粉碎，哥德尔不完备定理无情地证明了希尔伯特计划是不可能完全实现的。尽管如此，对常用的数学形式化仍然是现代数学一项非常重要的工作。
将话题从数学切换回人工智能，我们来观察一下形式化的描述方法对计算机和人工智能领域带来的影响。上一章曾提到纽厄尔和司马贺在达特茅斯会议上拿出的最吸引眼球的成果—能够自动证明《数学原理》中多个定理的“逻辑理论家”程序。这个程序能够自动证明的定理，必须全部是使用形式语言去描述已知的前提，且结论可通过有限步骤推理完成的定理。“逻辑理论家”的基本思路是利用计算机的运算速度优势，遍历出形式化之后的定理前提的所有可能的变换形式，说白了，其实也就是常见的树搜索，再配以适当的剪枝算法。“逻辑理论家”以已知前提为树的根节点，把根据规则可以进行的每一种变换都作为该节点的下一个分支，如果某个分支中出现了与结论一致的变换形式，那这个分支经过的每一个节点按顺序连接起来就是定理证明的步骤。“逻辑理论家”采用的算法和今天计算机自动定理证明这个学科分支的主流算法（如归结原理、DPLL 算法）并没有直接关系，甚至可以说只是对形式化的前提进行简单乃至粗暴的搜索，这也正是后来计算机自动定理证明领域的著名学者王浩教授批评“逻辑理论家”，认为它没有多少技术含量的主要原因。
74
第二部分 学派争鸣
○一 精确定义基础概念并不是简单的工作，罗素在《数学原理》中用了超过 300 页篇幅才实现了自洽的“数字 1”的定义。