四象猜想 (5-1)

关于是否会存在定理证明机，在理论上人们是有过不同的看法的。有些人认为不可能，如著名数学家庞加莱；而有些人却觉得是可能的，并从理论上进行了论证，如著名的数理逻辑学家塔尔斯基。同时他还指出初等代数和初等几何范围的定理证明是可以实现机械化的。而在希尔伯特的《几何基础》中，也已经蕴涵了“万理一证”的定理证明机械化思想，只是由于物质条件的不成熟而计人把他的这个重要思想给忽视了。然而，本世纪初数理逻辑的创立，以及40年代电子计算机的出现却复兴了这一想法，并且使之成为现实。

本世纪 50 年代，在这方面做出先驱性工作的是数理逻辑学家王浩教授，他仅用几分钟的时间就在计算机上证明了罗素和怀特海合著的《数学原理》中的300多条定理。这件事情为从事人工智能研究的人们着实兴奋了一阵，但是这一切技术性的工作并没有太多地引起数学界人士关于计算机对数学影响的重视，因为计算机所做的也就是人工所做的翻版。

然而70年代以后，计算机在数学中的应用却给数学界带来了未曾料想的影响，它使得人们开始重新思考数学的本质问题。因为曾经困扰人们百年多的四色猜想在计算机上得到了证明，而且它的证明过程是人工无法检验的；而以大自然中具有自相似形状的物体为研究对象的分形几何，更是计算机下的产物。事实上，越来越多的数学问题的解决需要计算机的帮助，甚至是必须的。所有这些事实与人们从 19 世纪所接取过来的丰硕成果是这样不同，于是自然地就引起了人们对数学哲学问题的思考和讨论。

理论上的争论‍‍‍‍‍

纵观历史的发展，人们想把推理机械化的思想很早以前就有，如柏拉图、莱布尼茨、霍布斯、笛卡尔等等。而在近代，著名的德国数学大师希尔伯特在1899年出版的经典名著《几何基础》中，就已经指出了几何定理可以不是逐一证明，而是一类定理可以用统一的方法一起证明。其大致的方向是从公理化出发，通过代数化而达到机械化。只是由于当时数学研究仍处于手工作坊时代，这个重要的机械化方向和意义没有被数学家们及时地认识到。其实连希尔伯特自己也没有明确地意识到。

• 希尔伯特

到了本世纪初，数理逻辑的发展为推理过程的机械化提供了基础。无论命题演算还是谓词演算都建立了公理系统，这就使得推理过程形式化。于是从一些很简单明白的公理出发，使用一些很简单的机械推理规则，便可一步一步地把人们日常使用的、乃至数学中所使用的极复杂的推理规则推导出来。换句话说，人们日常使用的极复杂的推理规则，可以化归为一些简单的、机械的推理动作。最终的这些推理动作是这样的简单，以至于机械也可以实现，数理逻辑的成果让人们认识到，可利用机器来部分地代替人类头脑进行思维，正如可以利用机器来代替人类的体力劳动一样。

这种对推理过程认识的深化，自然地就导致有些数理逻辑学家提出关于定理证明机的想法。即∶有可能制造出一种机器以代替人类思维，代替人类进行推理。但是也有人反对，最有代表性的如当时一代数学大师庞加莱就对这个想法大加责难，还带有讽刺般地说：

现在已经有屠宰机器，当把牲畜赶到机器的一端时，机器便把这些牲畜宰杀成罐头，从另一端输送出来；现在有人竟然想制造一部机器，当把定理的前件送到机器的一端后，便可以把定理的结论从机器的另一端输送出来（或者公理、定义送到一端后，各式各样的定理便从另一端输送出来），这种想法是注定不可能实现的。

庞加莱的看法绝不仅仅是他一个人特有的想法，实际上是代表了当时数学界流行的、占统治地位的思想。试想一想，在这种想法流行的时候，特别还是那么有声望的大人物所反对的想法，人们还会想方设法制造电子计算机去实现定理证明吗？

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。