机器证明：必要性和可能性

定理机器证明的出现不是偶然的，而是有其客观必然性，它既是电子计算机和人工智能发展的产物，也是数学自身发展的需要。

首先，现代数学的发展迫切需要把数学家从繁难的逻辑推演中解放出来。我们知道，任何数学命题的确立都需要严格的逻辑证明，而数学命题的证明是一种极其复杂而又富有创造性的思维活动，它不仅需要根据已有知识和给定条件进行逻辑推理的能力，而且常常需要相当高的技巧、灵感和洞察力。有时为寻找一个定理的证明，还需要开拓一种全新的思路，而这种思路的形成竟要数学家们付出几十年、几百年乃至上千年的艰苦努力。如果把定理的证明交给计算机去完成，那就可以使数学家从冗长繁难的逻辑推演中解放出来，从而可以把精力和聪明才智更多地用于富有开创性的工作，诸如建立新的数学概念，提出新的数学猜想，构造新的数学命题，创造新的数学方法，开辟新的数学领域等等，由此提高数学创造的效率。

其次，机器证明的必要性，还表现在数学中存在着大量传统的单纯人脑支配手工操作的研究方法难以奏效的证明问题。这些问题往往因为证明步骤过于冗长，工作量十分巨大，使数学家在有生之年无法完成。电子计算机具有信息储存量大，信息加工及变换的速度快等优越性，这就突破了人脑生理机制的局限性与时空障碍。也就是说，如果借助电子计算机的优势就有可能使某些复杂繁难的证明问题得以解决。“四色猜想”的证明就是一个令人信服的范例。“四色猜想”提出于19世纪中叶，它的内容简单说来就是：对于平面或球面的任何地图，用四种颜色，就可使相邻的国家或地区区分开。沿着传统的手工式证明的道路，数学家们做了各种尝试，结果都未能奏效。直到1976年，由于借助于电子计算机才解决了这道百年难题。为证明它，高速电子计算机花费了120个机器小时，完成了300多亿个逻辑判断。如果这项工作由一个人用手工去完成，大约需要30万年。

第三，机器证明的可能性，从认识论上看，是由创造性工作和非创造性工作之间的关系决定的。我们知道，在定理的证明过程中，既有创造性思维活动，又有非创造性思维活动，而思维活动中的创造性工作和非创造性工作并不是完全割裂的，而是互为前提、相互制约、相互转化的，非创造性工作是创造性工作的基础，创造性工作又可以通过某种途径部分地转化为非创造性工作。当我们通过算法程序把定理证明中的创造性工作转化为非创造性工作之后，也就有可能把定理的证明交给计算机去完成。(www.xing528.com)

第四，理论上的研究已经表明，的确有不少类型的定理证明可以机械化，可以放心地让计算机去完成。希尔伯特和塔尔斯基的机械化定理，就是对定理证明机械化可能性的一种理论探讨。吴文俊教授对几何定理证明机械化的可能性曾作过深入的研究。他将可施行机械化证明的实现划分为三种不同的类型，并给出了实现机器证明的一个行之有效的一般方法。这个一般化方法的基本思想是：首先借助坐标系，把定理的假设与求证部分用一些代数关系式来表示，然后再把表示代数关系的多项式做适当处理，即把终结多项式中的坐标逐个消去，当消去的结果为零时，定理也就得证。

目前，机器证明作为数学研究的一种方法，还存在着许多理论和技术上的问题，这些问题的解决将有待于算法理论、计算机科学和人工智能等各个领域出现新的重大突破。