1976年6月，发生了一件轰动数学界的大事：困扰数学家们100多年的“四色定理”终于被证明了。证明是由美国数学家阿佩尔和哈肯利用高速计算机工作1200个小时才完成的。如果这一过程要人工计算的话，大概得用几十万年的时间。真不可想象！

　　1852年，刚从伦敦大学毕业的弗南希斯在对英国的地图着色时，发现了一个有趣的现象：无论多么复杂的地图，只需要用四种颜色就能将它区分开来，也就是说，用四种颜色着色就能保证不会有两个相邻地区的颜色相同。

　　弗南希斯将自己的发现告诉给哥哥弗德雷克，引起了弗德雷克的浓厚兴趣，他深信弟弟所发现的这个结论是正确的，并企图从数学的角度对这个结论给予证明，但所有的努力都失败了。在百思不得其解的情况下，只得专程去请教他的老师、英国著名的数学家德·摩根教授。摩根教授绞尽脑汁研究这个问题，可也一无所获。后来，他将这一猜想写信告诉了在都柏林的著名数学家哈密尔顿，于是“四色猜想”首次以数学的形式提了出来。

　　乍看起来，四色猜想很简单，现在世界上的国家和地区，也不过200多个，用四种颜色着色区分，这是不难办到的。但是，作为一个数学问题来说，它所要讨论的不是哪一张具体地图，而是概括所有可能的地图着色问题。它所涉及的国家地区的数目可以是任意的，而且边界也可以是各式各样的。

　　此外，四色问题所讨论的地图，还有两条限制：

　　一条是在地图中，每个国家必须连成一片。不能分成不相连的两片或更多片。

　　另一条是，在地图中，两个国家（或地区）的边界必须是直线或者曲线，不能是一点。

　　著名数学家哈密尔顿对“四色猜想”产生了极大的兴趣，经过长达13年的努力，直到1865年去世，其研究工作依然毫无结果。

　　四色猜想刚被提出时，并没引起很大的注意，许多数学家低估了它的难度。爱因斯坦的老师闵可夫斯基是著名的数论专家，也是一位非常谦虚的人。他曾认为四色猜想的证明并不复杂，其所以一直没有获得解决，仅仅是因为当时世界上一流的数学家没有研究它。有一次给学生上课时，偶然谈到了这个猜想，他说可以给出证明，并试图当堂证给学生看。可是他证得满头大汗，却是一筹莫展，只好第二次上课时接着证。一连几堂课，费尽九牛二虎之力，仍然证不出来。有一次，证明时正好天下大雨，雷声震耳，他惭愧地对学生说：“老天在责备我讲大话了，我证明不了四色猜想。”

　　此后，许多数学家都曾声称给出了这个猜想的证明，但后来逐渐都被发现其证明是有毛病的。这样，四色问题就成了世界上著名的难题之一。一百多年来，没有人能证明它成立，也没有人能举出反例来推翻它，它使数学家们深受困扰。

　　1879年，肯普曾宣布他证明了四色问题。他的证明虽然在11年后被数学家赫伍德否定了，但是人们认为他的证明思路，有很多可取之处。20世纪以来，许多人一直在继续按照他的思路，推进着四色问题的证明工作，并且取得了不少成就。可惜这些成就所提供的检验方法太复杂，人们难以实现。例如有人在1970年设计的方案，用当时的计算机来算，也需要连续不断地工作十万个小时，也就是说，要连续不断地计算11年以上，才能得出结论，所以难以证实。

　　之后，人们又大大地改进了证明方案，而且计算机的能力及其使用方法也有了飞快的进步，为机器证明四色猜想创造了条件。

　　本世纪70年代中期，美国伊利诺斯州立大学的数学家阿佩尔和哈肯独树一帜，利用高速计算机对“四色猜想”进行证明。他们运用了一种“不可避免性”理论，从一万多张地图中挑选了近两千张上机检验，对每一张地图都使用了二十万种可能的方法着色，计算机作了两百亿个逻辑判定，经过1200小时的计算，终于在1976年6月证明了这个数学名题。伊利诺斯数学杂志的审稿人，对阿佩尔与哈肯证明的审查，也是通过计算机来实现的。

　　阿佩尔与哈肯的工作，使延续了124年之久的四色问题得到证明，成为四色定理。计算机在证明数学难题方面立下了功勋。这一成果轰动世界，引起了极大的反响。

　　四色定理本身没有多少实用价值，人们可以用四种颜色绘制地图，也可用更多的颜色区分填充。但它曲折的证明历程使人深思，激发人们敢于面对困难，迎接挑战，去探索问题的真谛。美国数学家的贡献主要不在于证明四色定理本身，而在于用计算机解决了人们多年来无法解决的理论问题。它表明，靠人与机器合作，有可能完成连最著名的数学家至今也束手无策的工作，标志着人类认识能力的一个飞跃，极大地推动了以计算机为基础的人工智能的发展。目前，尚有一些问题留待人们去解决：已有的证明能不能简化？可不可以不用计算机而给出证明？这些问题仍吸引着有志者继续进行探索。