就数学定理计算机证明发展的前途而言，任何人估计都可以看出来这条道路的远大前景。和人类相比，计算机不知疲倦和逻辑严密的优点使得其前途不可限量。计算机当然也会犯错误，但是这种错误归根结底是容易检验的——其正确性归结为这些软件内核的正确性，而内核一共也就几百行、上千行代码而已，经反复、多次检验，正确性会有足够的保证。一代代数学家永远都要从零开始学习、逐步成长和长期积累，而计算机则总是建立在已有成果的肩膀上，假以时日，计算机会不会成为有史以来最伟大的数学家呢？

国外已出现一些人机交互的计算机推理系统。借助这些系统，能够用来进行不同的数学领域的推理，所生成的证明和数学家的工作很类似。

对于人类面临的很多难题，既然单个群体无法解决，那我们齐心协力一起解决不是很好么！数学家提供理论基础，计算机科学家设计算法并编程实现，而物理学家和工程师保证计算机的稳定性。

我们坚信，机器证明不但不会像有些数学家担心的那样“使数学走向衰败”，还将使数学家摆脱大量的繁琐的机械计算和推理，使他们把节省下来的时间和精力用于更加富有创造性的工作中去。

对于数学定理计算机证明来说，真正的挑战仍然体现在对未知证明的寻找上。如何让计算机学会迅速发现合适的证明路径，是这一领域里最困难也最迷人的问题之一。毕竟即使数学家自己往往也说不清楚数学证明的灵感是怎样产生又怎样被自己捕捉到的，更不用说让计算机来模拟这一过程了。对于计算机“思考方式”的设计和研究，本身当然就是很深刻的数学问题。从某种意义上说来，这一自我缠绕的局面不但没有构成对传统意义上的数学之美的消解，反而是它的延续。归根结底，这一领域的任何进展，都标志着人们对于“智慧思考”这一问题更深刻的理解，这已经足以令人骄傲了。

但我们仍然不得不看到，数学定理计算机证明这条道路从开始的第一天起就伴随着巨大的争议和疑虑。

人们对计算机证明的批评多半集中于它极端的繁琐和不直观。然而，既然人们已经知道如何把一个传统证明翻译为计算机证明，那么把一个计算机生成的计算机证明翻译成人们可以直接阅读和理解的直观证明，从理论上说来也并非全然不可能。就这一点来说，计算机证明和传统证明之间的鸿沟并非是不可逾越的，尽管还有很长的路要走。现在已经实现的几何定理可读机器求解，所生成的解答其推理过程的简洁优美可以与人工解答媲美。虽然解决的只是一小类数学问题，远没有达到解决四色定理、费马大定理一类难题的水平，但至少说明了计算机证明和人工证明之间并没有不可逾越的鸿沟，人类的创造力再一次得到展现。我们可以设想，在未来的某一天，这两种证明之间的界面变得极其友好，于是任何一个数学家都会把计算机证明作为日常数学工具加以掌握，任何一本数学杂志都会要求提交的证明必须是经过计算机验证的。

数学证明，是人类理性最光辉的成果之一，蕴藏在深刻美丽的数学定理背后的那些那种苦心孤诣的劳动和成功之后宛若天成的光辉，吸引了一代又一代伟大的头脑投身于其中。如果这些定理最终都只不过是被一些代码算出来的，这种美还有什么意义吗？

计算机一直被认为是数学家最引以为自豪的发明之一，然而当它转过头来开始侵蚀数学家的传统领地“定理证明”时，数学家的首要反应是捍卫自己的尊严。一个由计算机生成的证明，从广义上说来，当然也是人类智慧的产物，可是如果有朝一日，困扰人类数百年的某个著名猜想被计算机所证明，数学家会怎样考虑和看待这一问题呢？

当然，计算机证明之路已经打开，你可以像很多数学家一样投去怀疑甚至不屑一顾的目光，但是你不能无视它的存在，因为道路已经打开，纵然迷雾重重，但是没有理由不继续走下去。前途光明，奋斗仍需继续，让我们共同努力吧！