四色定理的机器证明

四色定理最先是由一位叫古德里的英国大学生提出来的。德・摩尔根1852年10月23日致哈密顿的一封信中提供了有关四色定理来源的最原始的记载。他在信中简述了自己证明四色定理的设想与感受。

四色问题的内容是：“任何一张地图只用四种颜色就能使具有共同边界的国家着上不同的颜色。”用数学语言表示，即“将平面任意地细分为不相重迭的区域，每一个区域总可以用1，2，3，4这四个数字之一来标记，而不会使相邻的两个区域有相同的数字。”

100多年以来，数学家们为证明这条定理绞尽脑汁，所引进的概念与方法刺激了拓扑学与图论的发展，但一直没有得出证明。

1976年，美国数学家阿佩尔与哈肯借助电子计算机，用了1200个小时，作了上百亿次判断，终于完成了四色定理的证明，轰动全世界。美国为此发行一枚纪念邮票，上面写着“四种颜色就够了”。

但新事物的产生和发展，往往不是一帆风顺的。

在计算机还没发明的时候，就有数学家提出机器证明（设计一种机器代替人推理）的设想，遭到了很多数学家的反对。数学大师庞加莱认为：“你可以将牲畜赶到机器的前端，机器将其宰杀后储存成罐头输出。难道你可以把定理的条件送到机器的前端，机器自动输出结论吗？这实在是不可思议！”

而在四色定理被机器证明之后，反对声仍然强烈。有评论认为：机器证明破坏了数学的优美。一个好的数学证明应当像一首诗――而这纯粹是一本电话簿！

普林斯顿数学教授约翰・康威在接受《纽约时报》采访时说：“我不喜欢它们（计算机证明），因为你感觉不知道究竟发生了什么。你不能从中获得任何新的见地。”

持这种观点的数学家不是个别的，他们认为：如果一个难题被一种新方法解决了，这是一件了不起的事情。但是如果解决的方案只是现存方法的反复使用，那只能证明解决者的聪明而已。这不利于数学的发展。

但是，机器证明四色定理毕竟丰富了我们的知识。以不能产生新方法为理由就拒绝承认，是说不过去的。用机器作为数学研究的辅助工具，这本身就是新的方法。

从历史上看，工具对数学的发展有重大的影响。筹算和珠算无疑推进了位置记数法和相应的计算系统的发展；圆规和直尺的使用不但推动了几何作图的研究，对近世代数的产生也有深远影响。计算机能够计算，能够作图，也应当能够推理。事实上，在计算机出现之前，数学家已经论证了推理化为计算的可能。

计算机的能力远远超过筹算、珠算、圆规和直尺的总和。数学家有了这样强大的工具，数学的面貌自然会有深刻的变化。

摘自张景中、彭翕成所著的《数学哲学》