所谓四色问题，简单说，就是在绘制地图时，不论是在平面上或球面上，若限制相邻两区域不能用相同颜色，则是否四种颜色就足够了？此问题是刚从伦敦大学毕业的葛斯瑞（Francis Guthrie）在1852年提出的一个猜测。1879年，剑桥大学三一学院数学系毕业生肯普（A.B. Kempe）给出了一个错误的证明，但有趣的是，在接下来11年时间，这个证明居然被大家接受。直到1890年，年仅29岁的英国数学家希伍德（P. J. Heawood）指出其错误。然而，希伍德也指出，运用肯普的证明思路，五种颜色一定足够，这就是著名的五色定理。

　　但有好几年，肯普证明中的漏洞并不视为多么严重，且四色定理被认为本质上已经证明。年复一年，数学家们终于意识到，四色问题的难度远超过当初之想象，差不多当时所有著名的数学家都会涉足四色问题。虽然经过许多数学家的努力，此问题仍旧悬而未决：可证明五色足够，且猜想四色足矣。但如同费马大定理，此猜想在相当长一段时间内，既证不出，也找不到反例。

　　进入20世纪以后，四色问题的研究主要是沿着两条道路开展的：一条是定性的，主要是肯普发明的“肯普链”方法；另一条是定量的，主要是希伍德的方法，其思想基础是寻找一个极小的反例。开始的做法就是对区域数目很少的地图证明四色定理，进而由少及多。半个多世纪又过去了，能够证明四色足够的地图，其区域数目才增至40个。区域数越多，可能的构形数目也就越大。直到1976年，虽然区域数目已接近100个，但四色问题距离解决还差得很远。

　　要想完整地证明四色定理，还需要引入新的概念，特别是可约化的构形，也就是把区域数多的问题简化为区域少的情形。20世纪70年代，希什（H. Heesch）推测这种构形应该有个上限，并估计不超过10000个。这在当时即使用计算机也办不到。但这种试图用有限驾驭无穷的想法，成为四色定理获证的一个关键思想。1976年，美国数学家阿佩尔（K. Appel）和哈肯（W. Haken）借助计算机，利用“穷举检验”法分情况检查，筛查出1482种可约的构形，也就是分了这么多种情形，并在IBM360计算机上运行达1200多个小时后终获证明。这成为第一个用计算机证明的大定理。美国芝加哥的邮局信封上也印有“四色足够”的字样。

　　虽然四色定理在1976年获得了计算机辅助证明，但是数学界对此并不放心，主要原因有二：一是使用计算机的部分无法用手算复核；二是能够用手算复核的部分因过于繁琐，无人能够独立完成。这些不太令人满意的地方导致人们对定理的真实性持怀疑态度，甚至上升到了对数学证明含义的哲学探讨。然而，即使到目前为止很多人还以为就只有这一代证明。

　　事实上，第一代证明以后，数学家们并没有放弃寻求严格的数学证明，也因此推动了图论整个学科的发展，这也是为什么图论的大多数问题都与图着色问题有关的原因。20世纪80—90年代，西缪尔（P. Seymour）与罗伯逊（N. Robertson）等人一直致力于研究地图着色问题，企图通过手写完成证明，但没有成功。他们的贡献在于使用的可约构形数目大大减少了，减少到633种构形。整个证明简单，而且容易复核，虽然仍需计算机帮助，但再次肯定四色问题的确是定理。

　　30多年来，计算机科学也一直在为四色问题寻找答案：形式程序证明（formal program proof）。这种证明法的思想是编写一种既能描述机器应该做什么，也能刻画它为什么必须这么执行的编码——形式正确性证明。证明的有效性是由不同程序进行复核的客观数学事实，而程序本身的正确性可以通过运行多种输入程序凭实验确定。尽管困难重重，四色定理还是迎来了它的第三代证明。2005年3月，贡蒂尔公布了他的形式证明，也就是一种把所有逻辑步骤都写出了的证明。这进一步肯定四色定理确是一个定理，而且对数学和计算机科学都有着十分重要的意义。但我们不能说数学家对这种新事物评价很高，西缪尔就曾说，“这基本上是我们所给证明的机器确证”。对数学家来讲，更为令人信服的方法，当然是纯粹数学的证明，而且越简单越好。

　　数学问题成千上万，但重要的数学问题不仅能产生新的概念、新的方法，而且能创造新的学科、新的问题。四色问题看起来是一个带有数学游戏性质的孤立的问题，可是它却创造出图论许多新的分支。数学家的本事在于他们能够把复杂的事物变成简单的对象。四色问题就可以做这样的化简：不妨把一个区域看成一个点，任何两个区域相邻（或者不相邻），就把代表两区域的点连上线，否则就不连线。这样的结构就称为图。四色问题也就变成图的顶点着色问题。现在，图的着色理论已经成了一个深刻而漂亮的研究领域。四色问题就像其他的好数学问题一样，它推动图论的发展，成为图论的核心部分，激起了许多重要的新数学思想的形成。把地图四色问题推广到任意曲面上，辟建拓扑图论并推动其发展。例如，一个平面或球面上的地图，四色足够，但在轮胎面（即环面）上，四种颜色就不够了，至少需要7色才行。另外，对图的平面性的研究在缩图结构理论中达到了高潮。最多产的图论大师塔特（W.T.Tutte）在谈到四色问题对数学的影响时说，“四色问题是冰山一角、楔之尖端、孟春一啼”。图论在网络理论中的作用更是不言而喻，在当今的网络世界中离开图论可以说是寸步难行。抚今追昔，这一切均由四色问题所赐。

　　（作者单位:河北师范大学数学与信息科学学院）