四色定理获证历程及对图论的影响

邓 硕 王献芬

（1.河北地质大学数理学院，河北 石家庄050031；2.河北师范大学数学与信息科学学院，河北 石家庄050024）

四色定理获证历程及对图论的影响

邓 硕1王献芬2

（1.河北地质大学数理学院，河北 石家庄050031；2.河北师范大学数学与信息科学学院，河北 石家庄050024）

通过回溯四色问题从猜想到定理的历史过程，揭示了简化思想在数学方法中的主导作用，最后简述四色问题对图论发展的影响，以对相关研究有所助益。

图论；四色定理；证明；图着色；拓扑图论

图论是组合数学的一个分支，是离散数学的重要组成部分。近些年来，随着计算机科学的发展，图的理论及其在其他科学领域的广泛应用，越来越受到数学界乃至科学界的重视。同其他数学学科相比，图论的历史虽不太久远，但是其内容的丰富、问题的难度、技巧的精湛及其理论的交叉融合，却是难以想象的。一个表述简单的问题，证明起来却有着意想不到的艰难。限于篇幅，本文简要论述四色问题从猜想到证明的历程，从中获得有益启示。

1 早期历史

所谓四色问题，简单说就是，若给平面（或球面）上任意地图着色，使得相邻两区域不能用相同颜色，问是否四种颜色足够？此问题是刚从伦敦大学毕业不久的英国青年葛斯瑞（F.Guthrie,1831-1899）在1852年的一个猜测。迄今为止，人们发现的第一个正式的文字记录是德·摩根在1860年4月14日写的一篇书评[6]。由于英国大数学家凯莱（A.Cayley，1821-1895）在1878年6月13日召开的伦敦数学会上当场发问，四色问题是否已被证明，从而引起了数学界极大的反响[1]。各国数学中心和主要数学杂志此后源源不断地收到四色问题的各种证明。

1879年，剑桥大学三一学院数学毕业生肯普（A.B.Kempe,1849-1922）首先给出了一个 “证明”。11年后，即1890年，希伍德（P.J. Heawood，1861-1955）首先给出一个反例图（即希伍德图），指出了肯普证明的疏漏。四色问题又成了未解之谜！

尽管肯普和希伍德均未能破解四色问题，但是，他们二人均为四色问题的最终获证乃至图论的发展做出了早期贡献。进入20世纪，数学家研究四色问题正是沿着肯普和希伍德开辟的道路前行的：一方面是定性方法，主要围绕肯普提出的“肯普链”展开；另一个则是定量方法，即希伍德构造极小反例的方法。利用这两种方法，数学界开始的做法是对区域数目很少的地图验证四色定理成立，由少及多，然而半个多世纪过去了，能被验证四色足够的地图，其区域数目才增至40个！实际上，区域数越多，可能的构形数目也就越大，就越困难。到20世纪60年代，这种依靠扩充区域数目的推广尽管已推至100多个，但四色问题距离解决还差得很远。

2 1976年的突破

要想完整地证明四色定理，还需要引入新的概念，特别是可约化的构形，亦即把区域数多的问题简化为区域少的情形。20世纪70年代，德国数学家希什（H.Heesch，1906-1995）推测这种构形应该有个上限，并估计不超过10000个，这相当于说，要把情况细分到可以证明的地步，要大约10000种情况才行！这是一个大胆预测。这使他成为继肯普之后第一位公开宣称四色问题能够通过可约构形思想来证明的数学家。显然，构造如此庞大的一个集合并证明其中每一个元素都可约用手算太不现实，即使使用计算机，在当时也办不到！尽管如此，但这种试图用有限驾驭无穷的想法，却成为四色定理获证的一个关键思想。为了寻找不可避免集，希什引入了一种类似在电网络中移动电荷的“放电”思想，这一创新思想成为四色定理最终获证的又一关键。

正是在这个时候，阿佩尔（K.Appel,1932-2013）和哈肯（W. Haken,1928—）勇敢地接过来希什手中的“接力棒”。他们把研究重点放在调整放电法则而不是一味地扩充不可避免集中可约构形的数目。他们运用希什的思想，重点着眼于不可避免集中那些看上去不可能可约的构形，然后重新设计放电算法以排除这些特殊构形。1976年，他们由于找到了一种新的放电程序，利用“穷举检验”法分情况检查，筛选出1482种可约的构形，即分了1482种情况，借助IBM360计算机，运行达1200多个小时后，终于攻克了这个难题。《美国数学会通报》刊出四色定理获得计算机辅助证明的消息，轰动了当时整个数学界[2]。

3 1976年以后

在数学定理证明中，阿佩尔和哈肯史无前例地使用了计算机。人们为之震惊与欢呼之后，便是怀疑与非议。显然，四色定理的机器证明并未得到普遍认可。事实，其中主要原因有二：一是，使用计算机的部分无法用手算核实；二是，应该用手算核实的部分因过于繁琐，无人能够独立完成。这些不太令人满意的地方导致人们对定理的真实性持怀疑态度，甚至上升到了对数学证明含义的哲学探讨。然而，想必很多人还以为就只有这么一代证明吧。

3.1 再次机器证明（1994年）

第一代证明以后，数学家们并没有放弃寻求严格的数学证明，也因此推动了图论学科的发展，这也是为什么图论的大多数问题都与四色问题有关的原因。到20世纪90年代，曾一直致力于研究四色问题的西缪尔（P.Seymour，1950-）团队，宣称得到了一种更加简化的证明方法。1994年，西缪尔应邀参加第22届国际数学家大会，并做1小时大会报告。

西缪尔等人的证明尽管基本思路与阿佩尔、哈肯的大致相同，但这个简化后的证明不乏创新思想。首先，证明篇幅从原来的741页，精简到43页。其中，放电法则从486个减至20个；不可避免构形从1482个减少到633个；图着色算法由4次时间算法优化为2次时间算法；证明所需机时由1200小时缩至24小时。其次，第二代证明达到了人工复核的要求。如果用计算机验证，5分钟就能验证完毕！最后，也是更重要的是，第二代证明澄清了长期以来对定理真实性的种种置疑，再次肯定了四色定理的正确性[3]。第二代证明尽管也要用计算机，但这种证明对人来讲是更透明的，因为每一步都可以转换成人可理解的证明，尽管它还不完全是一个标准的数学证明。时至今日，我们还没有一个通常意义下的四色问题的数学证明。可喜的是，进入21世纪，四色定理又有了新进展。

3.2 形式证明（2005年）

在某种程度上，尽管西缪尔等人的漂亮修正，平息了对于四色定理证明的置疑与非议，但无论如何，总有某些地方似乎“不大受欢迎”。至少英国剑桥微软研究院的高级研究员贡蒂尔（Georges Gonthier）这么认为。

30多年来，随着计算机科学的发展，一种所谓的形式证明进入了数学界。这种证明法的思想是编写一种既能描述机器应该做什么，也能刻画它为什么必须这么执行的编码。证明的有效性是由不同程序进行复核的客观数学事实，而程序本身的正确性可以通过运行多种输入程序凭实验确定。尽管困难重重，四色定理还是迎来了它的第三代证明。2005年，贡蒂尔公布了他关于四色定理的形式证明，这个证明可以由Coq辅助证明系统完全复核[3]。

从某种意义上讲，我们认为，形式证明的提法对数学和计算机科学有着十分重要的意义：首先，再次强烈肯定四色定理确实是一个定理；其次，对于大量已有数学证明的数学定理，如何找出一个形式证明，这给数学家与计算机科学家提供了一个新的研究领域。

然而，对数学家来讲，更为令人信服的方法，当然是纯粹数学的证明，而且越简单越好。

4 推动图论的发展

4.1 图着色理论的诞生

四色问题可以做这样的化简：把一个区域看成一个点，任何两个区域相邻（或者不相邻），就把代表两区域的点连上线，否则就不连线。这样的结构就称为图。四色问题也就变成图的顶点着色问题。从历史上看，20世纪30年代以前，图着色理论主要研究地图的着色，尽管肯普早在1879年就意识到了图的顶点着色与地图的面着色之间的对偶关系，但是除肯普外，其他数学家在当时还没有这种意识，更没有上升到研究一般图的着色问题的高度。直到惠特尼（H.Whitney,1907-1089）和布鲁克斯（R.L.Brooks,1916-1993）[1]的文章发表以后，图着色理论才逐渐由地图着色转向一般图的着色。值得一提的是，惠特尼正是由于对四色问题的研究而对图论做出了大量原创性的贡献[4]。

除了给图的顶点着色外，对图的边进行着色的研究也非常有趣。1880年，泰特给出了四色猜想的一个等价猜想：对任意三次正则地图着色，使相邻两条边界颜色不同，至多需要三种颜色。这自然地就产生一个一般的问题：给一个图的边着色，使其相邻两条边颜色不同，至少需要几种颜色？与顶点着色类似，这个最小的颜色数目叫做边色数。在图的着色理论中，边染色问题主要研究边色数的确定和上下界。顶点度显然是与边染色最直接的相关因素：任意图的边色数不能小于它的最大顶点度。数学家从这个基本的结论出发，研究了边色数与最大顶点度之间进一步的关系。1964年，卫津（V.G.Vizing,1937—）从边着色的研究中提出了图的分类问题。另外，由于实际的需要，很多问题并不能很容易地化归为顶点着色或边着色，这属于经典着色的范畴。于是就有必要引入更广泛的着色模型，并添加各种各样的约束条件。例如，允许一次使用多个颜色，即把几个颜色捆绑起来等。如此一来，图着色的模型甚至多达几十个。例如，清单着色、调和着色、区间着色、循环着色、强着色等推广的图着色问题。正如狄拉克（G.A.Dirac,1925-1984）所言，“抽象的图的着色推广了地图的着色，对抽象的图的着色的研究…打开了组合数学的一个新篇章。”[5]

4.2 拓扑图论的开始

无论是顶点着色还是边着色，研究对象均是简单曲面（所谓简单曲面就是不含有洞的曲面）上的图。对于复杂曲面上图的着色，还要追溯到1890年希伍德的工作[1]。他把地图四色问题推广到任意曲面，从而辟建了拓扑图论并推动了其发展。例如，一个平面或球面上的地图，四色是足够的，那么在环面（轮胎面）上，四色就不够了，至少需要七色才行。关于希伍德成就的综述可以参见G.A.狄拉克[6]。

5 结语

数学问题是数学发展的源泉。这不仅体现在对问题本身的解决上，还体现在随之而来的理论的进展上。对于数学问题，数学家感兴趣的主要是方法方面的问题，这是他们的专业。但是，从知识创新的高度来看，数学家更要关注问题的来龙去脉、数学方法的精髓以及数学问题在解决过程所带来的“副产品”。像四色问题这类叙述简单又极易明白，却让许多数学家毕生求索的“世界难题”，对于数学证明的理解也是十分重要的，本文在四色定理获证的历史中表明，简化永远是数学方法的灵魂。

今天，四色猜想已然成为四色定理。但对于数学家来说，图论研究的事业方兴未艾。四色问题不仅产生了大量新的概念、新的方法乃至新的问题，如已于2006年获证的强完美图定理，而且开辟了许多新的分支。这些似乎正好印证了图论专家鲍耐特（David Barnette）的话：“虽然四色定理已被证明了，但是数学家在大量未成功的尝试中所发展（的理论）将具有永恒的价值。”的确，由它提出的大量形式化了的其他问题还有待解决，例如图的顶点着色、边着色、拓扑图论中的着色问题，以及这三种量的任何组合的着色问题。无怪乎现代图论之父塔特（W.T.Tutte,1917-2002）感慨道，“四色问题是冰山一角、楔之尖端、孟春一啼”。当然，本文只是略论了四色问题对图论发展的影响，但愿可以起抛砖引玉的作用，而由四色问题的研究引导的其他图理论，将另文再续。

［1］Biggs N L,Lloyd E.K,Wilson R J.Graph Theory 1736-1936[M].Oxford: Clarendon Press,1986.

［2］Appel K,Haken W.Every planar map is four colorable,PartⅠ:Discharging, PartⅡ:Reducibility Illinois Journal of Mathematics.1977,21:429-490.

［3］王献芬，胡作玄.四色定理的三代证明[J].自然辩证法通讯.2010(4).

［4］王献芬.惠特尼对图论的贡献[J].自然科学史研究.2010,29(1):101-117.

［5］Chartrand G,Ping Zhang.Chromatic Graph Theory[M].Boca Raton,London, New York:CRC Press,2009.

［6］Dirac G A.Percy John Heawood[J].J.London Math.Soc.1963,38:263-277.

［责任编辑：张涛］

※基金来源：国家自然科学基金（11201113）和教育部博士点新教师类基金（20121303120001）。

邓硕（1987—），女，河北地质大学数理学院，助教，研究方向为代数编码理论。