关于是否会存在定理证明机，在理论上人们是有过火歧的意见的。有些人认为不可能，若有名数学家庞加莱；而有些人却以为是可能的，并从理论上进行了论证，若有名的数理逻辑学家塔尔斯基。同时他还指出初等代数和初等几何范围的定理证明是可以实现机器化的。而在希尔伯特的《几何根本》中，也已经蕴涵了“万理一证”的定理证明机器化思想，只是由于物质条件的不成熟而计人把他的这个主要思想给忽略了。然而，本世纪初数理逻辑的创立，以及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年的纽约时报上还刊登了这样一篇文章：《没人能考验的证明算是数学证明吗？》。
附和者认为，机器证明是有可靠性问题，但是，有的数学定理被数学家证明了，但过了几十年，人们又创造其证明是缺点的，这解释人工证明也有一个可靠性问题。以是只对机器证明提出可靠性问题是不公正的。
而另一方面，电子打算机正越来越多地参与到数学中的各个领域里来。特殊是近年在数学中的某些领域，有许多的问题如果不借助于大型的打算机，常常是无法办理的，如关于大数素性的考验、关于一个有限单群的布局性的证明等问题。
总之，环绕着四色猜想的打算机办理，人们提出了许多重大的问题∶技能上的和哲学上的。四色猜想的打算机证明之意义，决不仅仅在于一个历时多年的难题的办理。就从目前的趋势看，它很可能将成为数学发展史上一系列新思想的引子。分形几何的创立便是一个解释。
