机器证明在数学领域的兴起和进展

机器证明的思想渊源可追溯到几何代数化思想的出现，然而历史上最先从理论上明确提出定理证明机械化思想的是希尔伯特。1899年，他在《几何基础》这部经典名著中指出，初等几何中只涉及从属平行的定理可以实现证明的机械化，他还提出了有名的“希尔伯特机械化定理”。希尔伯特的几何机械化思想遵循的就是一条几何代数化的道路：从公理系统出发，建立坐标系，引进数系统，把几何定理的证明转化为代数式的计算。这是一条从公理化走向代数化直至数值化的道路。1950年，波兰数理逻辑学家塔尔斯基进一步从理论上证明，初等代数和初等几何的定理可以机械化。他还提出了以他的名字命名的机械化定理以及制造证明机的设想。

机器证明史上的第一项奠基性的突破，是由美国的卡内基大学—兰德公司协作组做出的。1956年，这个协作组的西蒙、纽厄尔和肖乌等人在电子计算机上成功地证明了罗素和怀特海所著的《数学原理》第二章52条定理中的38条。这一年可作为历史上计算机证明定理的开端。1963年，他们又在计算机上证明了全部52条定理，西蒙等人使用的是LT(逻辑理论机)程序。这种程序不是刻板的固定算法程序，而是使用了心理学方法，将人脑在进行演绎推理时的逻辑过程、所遵循的一般规则和所经常采用的策略、技巧，以及简化步骤的一些方法等编进计算机程序，让计算机具有自己去探索解题途径的某种能力。这一程序为机器证明提供了一个切实可行的算法，通常称它为“启发式程序”。

在机器证明的开拓者中，还有著名的美籍华人王浩教授。1959年，他只用9分钟的机器时间，就在计算机上证明了罗素和怀特海《数学原理》一书中的一阶逻辑部分的全部定理350多条，在当时数学界引起了轰动。

改进算法程序是提高机器证明效率的一个重要方面。在这方面，美国数学家鲁滨逊首先取得了重大突破。1965年，他提出了有名的归结原理。这一原理的基本出发点是，要证明任何一个命题为真，都可以通过证明其否定为假来得到。它要求把问题用一阶逻辑表示出来，并且变为只具有永真式或永假式性质的公式。由于许多定理都可以在一阶逻辑中得到表示，因而这一程序具有较大的实用性，对提高机器证明的效率有着重要的方法论意义，大大地推动了机器证明的研究。(www.xing528.com)

70年代，机器证明得到新的重大进展。1976年，美国数学家阿佩尔和黑肯借助计算机成功地解决“四色猜想”的证明问题。这是机器证明首次解决传统人脑支配手工操作所长期没能解决的重大问题。1971—1977年间，莱得索等人给出了分析拓扑学和集合论方面的一些著名定理的机器证明。1979年，波依尔和穆尔等人作出了递归函数方面的机器证明系统。

我国数学家在机器证明研究上取得了显著的成果，引起了国内外学术界的关注。1977年，吴文俊教授证明了初等几何主要一类定理的证明可以机械化。1980年，他还用一部微机在20和60个机器小时左右分别发现了两个几何学的新定理。吉林大学和武汉大学的研究人员也在定理的机器证明方面取得了许多可喜的成果。

上面我们考察和分析了数学史上发生的6次重大突破。除了这6次重大突破外，还有许多重大事件也都具有一定的突破性，它们都不同程度地带来了数学思想方法的重大变化。如非欧几何的发现，群论的产生，勒贝格积分的建立，突变理论的出现，非标准分析的诞生，就是这样的事件。现代科学技术革命的兴起，向数学提出了一系列新的重大课题，可以预想，对这些课题的探讨，必将会引起数学在思想方法上发生新的重大突破，使数学的面貌发生新的改观。