机器证明可靠吗？
用机器证明的数学定理中，最为人津津乐道的当属四色定理。100多年以来，数学家们为证明这条定理绞尽脑汁，所引进的概念与方法刺激了拓扑学与图论的发展，但一直没有得出证明。1976年，美国数学家阿佩尔与哈肯借助电子计算机，用了1200个小时，作了上百亿次判断，终于完成了四色定理的证明，轰动全世界。美国邮局为此在一些明信片上加盖邮戳：“四色足够了！”
当一些数学家为一个高难度的定理得到解决而庆祝时，更多的数学家却对计算机给出的证明表示质疑。质疑的理由有二。一是对于相当多的定理证明，特别是那些被称为“下金蛋”的数学问题，最重要的意义不在于论证最终的真假，而是在求证过程中不断发现的新方法。二是计算机凭借高速计算能力作出的所谓证明，数学家无法人工检验，谁知道中间会不会出错呢？
计算机得出的结果，有些是容易检验、容易相信的。例如，把某一个很大的整数分解为两个大于1的整数的乘积，这是破解一类密码的关键任务。大型高速计算机工作几个月才分解了一个整数，人只要几分钟就能检验结果是否正确。
类似地，计算机算出来的方程解是否正确也不难检验，但定理证明是另一回事。在例证法中，面对计算机用10万个例子证明了的一条几何定理，我们会有什么想法？与此类似，用代数方法经过成百上千项的多项式计算而证明的几何定理，我们会有什么想法？
我们可以相信某一条被计算机宣布成立的定理前提，认为计算机的硬件是可靠的，计算机的操作系统是可靠的，机器证明软件的程序是可靠的，程序依据的算法和理论是可靠的。
算法和理论的可靠性，通过学习和讨论，不难确认。其他几种可靠性，可以经过大量实践验证。譬如让另外一批人，用另外的算法编程，用另外的机器运行，假如推导出来的结论与之一致，那么可靠性得到了增强。因为一个定理，反映一个客观事实。这个事实不会因发现的人的不同而改变，同样也不会因为证明程序的不同而改变。这样做，从哲学上看，是不是改变了数学真理的性质呢？
另一种方法，是计算机给出人工能够检验的证明。1976年，中国科学院的吴文俊院士发表了检验几何命题的有效的机械化方法。吴法的成功激起了几何定理机器证明的研究热潮。到1992年，基于几何不变量的消点方法出现，实现了几何定理可读证明在计算机上的自动生成。这一工作被国际同行誉为计算机处理几何问题的里程碑。
伴随着计算机技术的进步，直到1996年出现了基于前推模式的“几何信息搜索系统”，成功地证明了上百个非平凡的几何命题，收到了良好的效果。
在计算机还没发明的时候，就有数学家提出机器证明（设计一种机器代替人推理）的设想，遭到了很多数学家的反对。数学大师庞加莱认为：“你可以将牲畜赶到机器的前端，机器将其宰杀后储存成罐头输出。难道你可以把定理的条件送到机器的前端，机器自动输出结论吗？这实在是不可思议！”
在四色定理被机器证明之后，反对声仍然强烈。有评论认为：“机器证明破坏了数学的优美。一个好的数学证明应当像一首诗——而这纯粹是一本电话簿！”普林斯顿大学数学教授约翰·康威更是在接受《纽约时报》采访时说：“我不喜欢它们（计算机证明），因为你感觉不知道究竟发生了什么。你不能从中获得任何新的见地。”持这种观点的数学家不是个别的，他们认为如果一个难题被一种新方法解决了，这是一件了不起的事情。但是如果解决的方案只是现存方法的反复使用，那只能证明解决者的聪明而已。这不利于数学的发展。
还有人指出，传统数学研究四色定理，虽未获得最终成功，但促进了某些数学分支的发展（主要是图论、拓扑学等），而机器证明四色定理结论是对的，又能怎样呢？只得到没有灵魂的空壳而已，因为四色定理本身的意义并不大。现在数学界普遍承认五色定理了，但世界上绝大多数的地图颜色都超过5种。因为除了考虑颜色种类最少，现实生活中还有其他考虑。
一位反对机器证明的数学家说，数学的光荣，便在于它现有的一切证明方法，都是脉络绵密，层次分明，就像天衣无缝，出不了差错的。而使用计算机则有可能出现人无法检验出来的差错，而这差错可能是致命的。
现在已经实现的几何定理可用机器求解，所生成的解答其推理过程的简洁优美可以与人工解答媲美。虽然解决的只是一小类数学问题，远没有达到解决四色定理、哥德巴赫猜想一类难题的水平，但至少说明了机器证明和人工证明之间并没有不可逾越的鸿沟。人类的创造力再一次得到展现。
国外还出现了一些人机交互的计算机推理系统，如Coq、Otter、Roo等。借助这些系统，能够用来进行不同的数学领域的推理，所生成的证明类似于数学家的工作。
其实对于人类面临的很多难题，既然单个群体无法解决，那我们齐心协力一起解决不是很好么？数学家提供理论基础，计算机科学家设计算法并编程实现，而物理学家和工程师们则要保证计算机本身的稳定性。
我们相信，机器证明不但不会像有些数学家担心的那样“使数学走向衰败”，还将使数学家摆脱大量的繁琐的机械计算和推理，把节省下来的时间和精力用于更加富有创造性的工作中去。
