关于是否会存在定理证明 机 ，在理论上人们是有过不同的看法的。有些人认为不可能，如著名数学家庞加莱；而有些人却觉得是可能的，并从理论上进行了论证，如著名的数理逻辑学家塔尔斯基。同时他还指出初等代数和初等几何范围的定理证明是可以实现机械化的。而在希尔伯特的《几何基础》中，也已经蕴涵了“万理一证”的定理证明机械化思想，只是由于物质条件的不成熟而计人把他的这个重要思想给忽视了。然而，本世纪初数理逻辑的创立，以及40年代电子计算机的出现却复兴了这一想法，并且使之成为现实。 本世纪 50 年代，在这方面做出先驱性工作的是数理逻辑学家王浩教授，他仅用几分钟的时间就在计算机上证明了罗素和怀特海合著的《数学原理》中的300多条定理。这件事情为从事人工智能研究的人们着实兴奋了一阵，但是这一切技术性的工作并没有太多地引起数学界人士关于计算机对数学影响的重视，因为计算机所做的也就是人工所做的翻版。 然而70年代以后，计算机在数学中的应用却给数学界带来了未曾料想的影响，它使得人们开始重新思考数学的本质问题。因为曾经困扰人们百年多的四色猜想在计算机上得到了证明，而且它的证明过程是人工无法检验的；而以大自然中具有 自 相似形状的物体为研究对象的分形几何，更是计算机下的产物。事实上，越来越多的数学问题的解决需要计算机的帮助，甚至是必须的。所有这些事实与人们从 19 世纪所接取过来的丰硕成果是这样不同，于是自然地就引起了人们对数学哲学问题的思考和讨论。 理论上的争论 纵观历史的发展，人们 想 把推理机械化的思想很早以前就有，如柏拉图、莱布尼茨、霍布斯、笛卡尔等等。而在近代，著名的德国数学大师希尔伯特在1899年出版的经典名著《几何基础》中，就已经指出了几何定理可以 不是 逐一证明，而是一类定理可以用统一的方法一起证明。其大致的方向是从公理化出发，通过代数化而达到机械化。只是由于当时数学研究仍处于手工作坊时代，这个重要的机械化方向和意义没有被数学家们及时地认识到。其实连希尔伯特自己也没有明确地意识到。
希尔伯特
到了本世纪初，数理逻辑的发展为推理过程的机械化提供了基础。无论命题演算还是谓词演算都建立了公理系统，这就使得推理过程形式化。于是从一些很简单明白的公理出发，使用一些很简单的机械推理规则，便可一步一步地把人们日常使用的、乃至数学中所使用的极复杂的推理规则推导出来。换句话说，人们日常使用的极复杂的推理规则，可以 化 归为一些简单的、机械的推理动作。最终的这些推理动作是这样的简单，以至于机械也可以实现，数理逻辑的成果让人们认识到，可利用机器来部分地代替人类头脑进行思维，正如可以利用机器来代替人类的体力劳动一样。 这种对推理过程认识的深化，自然地就导致有些数理逻辑学家提出关于定理证明 机 的想法。即∶有可能制造出一种机器以代替人类思维，代替人类进行推理。但是也有人反对，最有代表性的如当时一代数学大师庞加莱就对这个想法大加责难，还带有讽刺般地说：
现在已经有屠宰机器，当 把 牲畜赶到机器的一端时，机器便把这些牲畜宰杀成罐头，从另一端输送出来；现在有人竟然想制造一部机器，当把定理的前件送到机器的一端后，便可以把定理的结论从机器的另一端输送出来（或者公理、定义送到一端后，各式各样的定理便从另一端输送出来），这种想法是注定不可能实现的。
庞加莱的看法绝不仅仅是他一个人特有的想法，实际上是代表了当时数学界流行的、占统治地位的思想。试想一想，在这种想法流行的时候，特别还是那么有声望的大人物所反对的想法，人们还会想方设法制造电子计算机去实现定理证明吗？ 然而随着数理逻辑对推理过程本质研究的渐渐被认识，反对制造定理证明机的人们在日益减少，而支持的人却越来越多。本世纪50年代，塔尔斯基首先从理论上证明了∶在初等几何以及初等代数的定理证明是可以机械化的。不过他给出的机械化方法过于繁复，在实践中真正实现起来是相当困难的。正是因为这样，所以他的结果给人以这样一个感觉∶定理证明能机械化的设想是个例外，因为大部分初等几何及初等代数以外的结果都是不能机械化的。另外，塔尔斯基还提出了制造证明机的设想。无疑这种理论上的阐明是重要的，就如图灵从理论上证明电子数字计算机是可能的一样，它让人觉得自己的实践和试验不是盲目的。 科技的进步为人们的这些设想提供着物质基础，终于人们制造出了证明定理的机器。 五十年代中期，美国开始利用计算机进行证明数学定理的尝试。 1959年，王浩用计算机证明了罗素和怀特海所著的《数学原理》这一经典著作中的300 多条定理，一共只用了9分钟的机器时间。这件事在数学界（特别是数理逻辑界）引起了轰动。他所使用的方法就是罗素和怀特海的技术，因为在《数学原理》中有许多标准的技巧是可以很快地变为机械的手续。接着J.A.Robinson发展了并使之成为一种标准的方法。这个结果就导致许多人对定理机器证明的前途看好，甚至有人还在1958年做出预测说，在10年之内计算机将发现并证明一个重要的数学新定理。也有人设想，前人像皮亚诺、怀特海、罗素、希尔伯特以及图灵等的梦想都将实现，然而事情的进展并没有人们预想的那样顺利，不过随着时间的推移，这些设想终究成为了现实。 首先是20世纪70年代，美国的数学家阿佩尔和黑肯借助于计算机证明了著名的四色猜想，震动了数学界。它标志着计算机证明数学定理有着很好的 前景 。尽管如王浩先生的说法，四色猜想的证明是一种使用计算机的特例机证，但是它是一个 由 人没有能够解决的数学问题。而且它的证明又非传统上的形式，于是就引起了人们继数学基础研究、希尔伯特探讨数学证明之后的又一次对数学证明的思考：什么是数学证明？ 而上世纪70年代，在国际上掀起的一股研究以"非"字当头的科学中，由曼德布罗特创立的分形几何学，更是得力于计算机的强大功能。计算机在这里并不是证明定理，而是帮助人们提出猜想，引发思考。我们当如何看待这门学科呢？有人认为它不是数学。但也有更多的人认为它是一门数学学科，特别是物理学家，因为分形几何正在成为研究大自然中许多复杂现象的有力工具。双方争执的焦点是"什么是数学"这个基本的数学哲学问题。 四色猜想证明的历史 1976年1月，困扰了无数智者100多年的四色猜想由人机合作终于获得了解决。面对这一事实，有人带着些惊喜、有人带着些遗憾、也有人带着些怀疑，毕竟它不是数学家们所希望的那种传统演绎证明定理的方式。 四色问题
四色问题是一个属于拓扑学的问题，它的粗略描述可以追溯到1840 年。当时数学家莫比乌斯在给学生的讲课中提到。在平面上很容易指出四个区域，其中每两个区域都有一个公共的边界线，并要求学生证明：在平面上决不可能指出五个区域都具有上述性质。从这个论断的证明中，可得出莫比乌斯假设∶平面或球面上的每张地图都可以用四种颜色来着色。 明确提出四色问题的是伦敦大学学院毕业不久的学生弗朗塞斯·古斯里（1852）。他在一封给他兄弟弗雷 赘 克的信中说∶
看来，每幅地图都可以只用四种颜色着色，使得有共同边界的国家着上不同的颜色。
这是原始四色问题的描述。由于他的兄弟无法解决，所以就这个问题的证明去请教他的老师——英国著名的数学家、逻辑学家德·摩根，据说德·摩根当天就写了封信给当时正在英国三一学院执教的著名数学家、物理学家哈密顿。然而这两位数学家实际上都没有能够解决这个看上去非常简单的问题。 后来英国著名的数学家凯莱于1878年伦敦数学家会议上正式公布了这个问题。他呼吁与会者去解决这一问题。就这样，和费马大定理一样，这个表面 看似 明易懂，其实很奇特的问题进入了数学家的圈子。从此受到了数学界人士的普遍重视以及数学爱好者们的兴趣。以后，宣布证明了四色问题的声明源源不断，可是一经检查，总是有或大或小的、难以弥补的缺陷。 在众多声称证明了这一论断的解答中，最值得一提的是1879年有一位名叫肯普的会员（同时也是律师）提交的一篇论文。凯莱和当时其他的一些数学家检查后确定证明是正确的。谁知过了10年，也即在1890年，年仅 29岁的英国数学家希伍德在证明中 却 发现了漏洞。这样，四色猜想依然固我，没有被解决。直到如今才借助于计算机给予解 快 。 肯普的证明是有 错误 ，然而他的证明思路非常有价值。因为一方面 20 世纪的人们正是沿着他的证明思路，逐渐改进而借助于计算机最终解决了四色问题；另一方面，希伍德在肯普方法的基础上还证明了"五色定理"，特别是对欧拉示性数为K时的曲面上的地图着色数P_k给出了上界： 四色问题的解决 前面已经提及，肯普的证明有错误，但包含了许多天才的思想。 肯普是采用反证法证明四色猜想的，具体思路是∶ 如果有需要五种颜色的地图，则此种地图中必定有一个最小的，也就是在需要五种颜色的地图中有一个区域数目是最少的（这种地图称为最小五色地图）。于是只要证明这种最小的地图是不存在的，问题就可以获得解决。因为假如给定了这样的一种地图，最后总能够对它进行"归约"而找到一种更小的地图，而这幅地图也需要五种颜色。为此，肯普先把问题转化为只研究一种所谓的正规地图，在这种地图中由有两个邻国、三个邻国、四个邻国及五个邻国组成的一组构形是不可避免的，也即他需要证明总得有一个国家其邻国数小于等于5。在这个条件下，肯普把上述论证又简化成四条引理: （1）每一 地图 都含有五个或五个以下邻域的区域； （2）最小的五色地图不可能含有恰好有两个或恰好有三个邻域的区域（因为如果那样我们将能够找到一个更小的需要五种颜色的地图）； （3）同样地，这样的地图不 可能 含有恰好有四个邻域的区域； （4）这样的地图不可能含有恰好有五个邻域的区域。 对这四种情况经过检查看是否有"可约构形"出现，如果都有，矛盾就出现了。肯普对于引理1）一3）证明得很成功，但是在4）上却失败了。 20世纪的数学家们从肯普跌倒的地方开始了艰难的跋涉。 首先是美国数学家伯克霍夫。1913年他在肯普的基础上引进了一些新技巧，这促进了富兰克林于1939年证明22国以下的地图都可以用四色着色；1950年温（Winn）又把22国改进为35国；再接着是1968年奥尔（他是唯一的一本关于四色问题专著的作者）把数目提高到39国；1975 年又报道，对 52 国以下的地图四色猜想都成立。从时间上可以看出，四色问题解决的进展是极其地缓慢。其中一个一直难以解决的困难，是肯普证明中关于五个邻国时可约构形的判断问题。具体地说是如何把 4）中的情况分得足够细。 在四色问题的解决之路上，数学家H.希什也做出了很大的贡献。他从1936 年就开始对四色问题进行研究，且始终坚信四色问题可以通过寻找可约构形的不可避免组得到解决。到1950年他从不断的试验中猜测，如果把情况分细到可以证明的地步，则这个组里的构形可能需要大约一万多种情况才行。要对如此多的构形逐一证明，工作量之大是非人力所能完成的。恰逢电子计算机在计算速度、精确度等方面都得到了惊人的进展，希什敏锐地意识到，若把证明构形可约的方法形式化，在理论上有一部分是可以通过计算机解决的。于是他很快就试着利用人机结合去解决，这也是早期人工智能的一种尝试。 最初他与其学生是围绕着怎样用计算机检查图形是否可约构形进行的。尽管希什曾猜测可能要分一万种情况，可是谁也不知道是否真得需要有一万种，况且即使是对一种不太复杂的情况，若要检查也要用上百个小时，而对较复杂的情况，无论是在时间上，还是在存储上，计算机都不能承受。 美国伊利诺斯大学的黑肯教授在总结以往各种证法后指出，如果运用现有的一切数学方法，不可能给出四色猜想一个传统上的证明，而在还没有一个更强有力的计算机之前，能否给出一个计算机证明也是没有把握的。就在这样的信念下，黑肯对希什的方法作了重要的改进，接着是与阿佩尔合作着手研究四色问题。两人一方面从理论上继续简化问题，另一方面又利用计算机的试算和人机对话。从中获得有益的启示。后来二人连手设计了一个能做出特殊类型放电过程的计算机程序，并经过上机不断地反复试验、不断地修改，特别是在计算机专家科克的参与下，最后终于在1976年1月6日，由三人找到了一个合适的可行程序，证得了可约构形的不可避免组。于是百年来让人们苦苦思索的这个叙述简单明了的四色猜想，在IBM360机上运行达1200多小时后得到了证明。他们是利用"穷举检验"法分情况检查的，当时一共分了1482种情况，经查证它们都是可约构形。 四色猜想的证明是如此的繁复，尽管在 1977 年的一次数值数学与计算机会议上，有人又官布了一个相对简单的证明，可是也要用50机时。所以它不像数学中上其它问题的证明，获得数学家们的一致赞扬，而是引起了许多的争议。 争议 从四色猜想的解决过程可以看到，它是众多数学家合作的结晶，是对历史上智者探索的完善。阿佩尔等人是采用汇编语言编写程序解决了四色问题、其程序之复杂到如今都还有人时不时地检查出错误，虽然是不影响全局的；而且就目前的解决方法来看，其工作量之大是人力所永远无法达到的。面对四色问题的这种复杂的、又是借助于计算机的证明，人们给以各种各样的反应。正如国际上的数学家们所认为的，阿佩尔和黑肯等人的贡献并不在于证明了四色问题，而在于借用电子计算机完成了这个至今人还没有能够解决的问题。但是，也有一些数学家反对四色猜想已经成为一个定理，于是自然地就引发一场争论。这场争论的焦点集中在计算机证明的可靠性和四色猜想的计算机证明是不是数学证明的问题。 关于机器证明的可靠性问题 反对四色定理的人认为∶如果一个定理不能用手工进行检查，无法核实其证明是否可靠，就不能接受它是一个定理。计算机用了 1200个小时才证明了四色定理，这是用手工几代人也无法检查完的。事实上，在1961年，就有人声称借助于计算机找出了一个不可免完备集，其中的构形全是可约的（果然如此的话，四色猜想当然获证）。但是，惠特尼和塔特却各自独立地发现，有一个构形的可约性被计算机误算了，从而那个证明是错误的。事实上，自从黑肯和阿佩尔在 1976 年解决四色猜想之后，人们一直都在不断地从证明中发现一些错误，庆幸的是这些错误都可以被修正而不影响证明的全局。但是谁也无法保证，有一天不会从中找出一个致命的错误；机器中的硬件或软件的错误。这就是机器证明的可靠性问题。 但是，赞成四色猜想是一个定理的人却认为∶
机器的可靠性主要是工程技术和物理学鉴定的事情，这是一门深奥的自然科学，它向我们保证，计算机的工作是可靠的，就象电子显微镜的工作是可靠的一样。
美国著名数学家瑟斯顿在《数学的证明和进展》一文中谈道：
实际上，一个可以运作的计算机程序，其正确性和完备性标准比起数学界关于可靠的证明的标准要高出几个数量级。
关于四色猜想的计算机解决是不是数学证明的问题 不承认四色猜想的计算机解决是属于数学证明的人认为，没有一个数学家曾看到过四色猜想的证明，也没有一个数学家看到过它的证明的证据，没有数学家全面地验证过四色猜想的证明。如著名苏格兰数学家波塞尔在其文章《切合实际的数学观》一文中提到的：
如果这样的一个问题（例如四色问题）利用某种聪明的新思想解决了，那是很了不起的。但是、如果解决的方法只是一个现存方法的反复使用，那就只能证明解决者的聪明罢了。如果解决的方法包括用计算机来证明特殊情况，那也是糟糕的，按我的观点，这样的解根本不属于数学科学。
不加验证地接受计算机给出的信息，还不如接受另一个数学家的告诫。事实上，例行公事似的编制程序十分乏味，极可能造成程序的错误。如果让部分论证隐藏在计算机的铁盒中，我们就不可能得到所认为的证明中的实质东西——我们自己对问题的了解。 1988年的纽约时报上还刊登了这样一篇文章：《没人能检验的证明算是数学证明吗？》。 赞成者认为，机器证明是有可靠性问题，但是，有的数学定理被数学家证明了，但过了几十年，人们又发现其证明是错误的，这说明人工证明也有一个可靠性问题。所以只对机器证明提出可靠性问题是不公平的。 而另一方面，电子计算机正越来越多地介入到数学中的各个领域里来。特别是近年在数学中的某些领域，有许多的问题如果不借助于大型的计算机，常常是无法解决的，如关于大数素性的检验、关于一个有限单群的构造性的证明等问题。 总之，围绕着四色猜想的计算机解决，人们提出了许多重大的问题∶技术上的和哲学上的。四色猜想的计算机证明之意义，决不仅仅在于一个历时多年的难题的解决。就从目前的趋势看，它很可能将成为数学发展史上一系列新思想的引子。分形几何的创立就是一个说明。
