学过初中数学的人都知道，定理证明看起来是件非常需要动脑子的事。一般来说，绝大部分人都会觉得自己面对定理证明都会智商不够。
幸好，计算机不这么认为，至少比起听说读写来，机器更愿意去证明定理。
事情还得从亚里士多德的三段论讲起。什么是三段论呢？就是给出一个大前提，再给定一个小前提，那么可以推导出一个结论。例如：给定一个大前提“所有人都会死的”，小前提是“苏格拉底是人”，那么可以推出“苏格拉底会死”。这就是一个简单的定理证明过程，要证明的定理是“苏格拉底会死”，三段论就是这个定理的证明过程。
三段论毕竟太简单了，用自然语言描述的事情也不够精确。于是，费雷格、怀特黑德、罗素等人就想办法用数学语言对人类的推理过程进行了定义，构建了著名的“数理逻辑”。基于数理逻辑严格的表达方式，就可以从已经知道的事实推论出未知的事实，只要已经事实是正确的，那么未知事实也一定是正确的。从已经事实推出未知事实这一思维过程称为“演绎”。再扩展一下，如果我们定义了一套数学公理作为已知事实，原则上就可以演绎出和这些公理相关的所有数学定理。
基于这一思路，普林斯顿高等研究院的马丁-戴维斯(Martin Davis）于1954年在一台称为“大强尼”(JOHNNIAC)的电子管计算机上实现了第一个定理证明程序，证明了两个偶数相加还是偶数。
图2：马丁-戴维斯，1954年实现首个自动定理证明
1956年，Newell，Shaw和Simon给出了一个称为“逻辑机器”（Logic Theory Machine，LTM）的定理证明程序。Newell等人首先分析了人类解决数学问题的方法，发现人们通常会将难的问题分解成简单问题，并利用已知的定理、公理和解题规则进行试探性推理，直到所有子问题都得到解决，则原来较复杂的问题即可得到解决。他们将这些思路运用到LTM 程序上，利用正向推理（即由原因推理出结果）和启发式搜索（在搜索时利用领域相关知识以减小搜索范围），取得了极大成功。他们将LTM运行在JOHNNIAC上，证明了罗素、怀德黑德所著《数学原理》中前52个定理的38个。1963年，经过改进的LTM最终完成了《数学原理》第二章全部52条数学定理的证明。
1959年，美籍华人学者、洛克菲勒大学教授王浩给出了效率更高的“王浩算法”。在一台速度不高的IBM704电脑上，该算法用9分钟的时间将《数学原理》中所有定理（350条以上）统统证明了一遍。因为这一成就，王浩教授在1983年的国际人工智能联合会议上荣获首届定理证明里程碑奖。
从此以后，数学定理证明得到长足进展，人们提出了很多新方法和新思路，包括Robinson的归结法，吴文俊教授的几何问题代数化方法等。1976年6月22日，哈肯和阿佩尔宣布他们用机器证明了四色猜想，成为自动定理证明的代表性工作[2]。
图3：为庆祝四色定理证明，UIUC数学系发布的邮戳
总结起来，计算机将定理证明转化为一个搜索过程，只要给以足够的时间，找到一条由已知事实到目标结论的推理路径是可能的。因为任务明确，方案简单，自动定理证明在人工智能领域算是相对容易的，至少在定义清晰、条件简单的任务上是如此。因此，定理证明在人工智能发展初期即取得了重要成果。当然，实际情况也不会那么轻松，如何对已知事实和目标结论进行形式化，如何设计搜索方法以提高效率，这些都不是简单事情。同时，机器给出的证明方法往往比较冗长，不易理解，因此即便机器证出来了，人们还是会想办法去寻找适用于人类思维的证明过程。
参考文献：
[1].Davis M. The early history of automated deduction: Dedicated to the memory of Hao Wang[M]//Handbook of Automated Reasoning. North-Holland, 2001: 3-15.
[2].Appel K., Haken W. (1978) The Four-Color Problem. In: Steen L.A. (eds) Mathematics Today Twelve Informal Essays. Springer, New York, NY.