机械化证明

出处：按学科分类—自然科学总论 天津人民出版社《自然辩证法辞典》第267页（693字）

利用计算机作为辅助手段来证明数学定理的一种方法。

简单的机械化证明是找出证明中需要大量数值的或组合的计算的部分，用计算机来完成计算工作，然后将计算结果重新置于原证明过程加以考察。系统的机械化证明是提出处理某一类有关问题的一般方法，比如对给定的某一类问题确定判定方法，以便知道该类问题中的每一个是否为一条定理。这种一般方法能够利用计算机来实施。关键是找出实施这种方法的适当程序。

机械化证明的研究，从本世纪50年代就已开始了，目前已取得许多显着的成就。其中比较突出的是关于“四色定理”的证明。

它是在1976年由美国数学家阿佩尔(Appel，K．)和黑肯(Haken，W．)完成的。计算机的计算时间为1200小时。此外，美籍华人学者王浩利用计算机在不到9分钟时间内，证明了罗素和怀特海所着《数学原理》中一级逻辑部分的全部定理，有350条之多。

我国数学家吴文俊于1977年找到了一个有关初等几何问题的快速判定过程，适用于那些不包括“在……之间”的关系的初等几何语句。其中有一些难度很大的初等几何定理。机械化证明的出现，改变了数学研究的传统方式，使以往数学研究中大量刻板单调的机械性思维活动为计算机所代替，节省了时间，提高了工作效率，有助于数学工作者的创造性思维活动更好地发挥作用。

有些数学定理的证明，如果依靠人力完成，其工作量要大到超出数学工作者的生理极限，过去常被认为是不可解问题。机械化证明为解决这类问题提供了方向、手段和成功事例，为人和计算机合作从事数学研究开辟了道路，展示了有希望的前景。