四色定理

四色地图的一个例子

四色定理（英语：four color theorem）又称为四色地图定理（英语：four color map theorem），是一个数学定理：如果在平面上划出一些邻接的有限区域，那么可以用四种颜色来给这些区域染色，使得每两个邻接区域染的颜色都不一样；另一个通俗的说法是：每个无外飞地的地图都可以用不多于四种颜色来染色，而且不会有两个邻接的区域颜色相同。被称为邻接的两个区域是指它们有一段公共的边界，而不仅仅是一个公共的交点。例如右图左下角的圆形中，红色部分和绿色部分是邻接的区域，而黄色部分和红色部分则不是邻接区域。

“是否只用四种颜色就能为所有地图染色？”的问题最早是由南非数学家法兰西斯·古德里在1852年提出的，被称为“四色问题”或“四色猜想”。人们发现，要证明宽松一点的“五色定理”（即“只用五种颜色就能为所有地图染色”）很容易，但四色问题却出人意料地异常困难。曾经有许多人发表四色问题的证明或反例，但都被证实是错误的。

1976年，数学家凯尼斯·阿佩尔和沃夫冈·哈肯借助电子计算机首次得到一个完全的证明，四色问题也终于成为四色定理。这是首个主要借助计算机证明的定理。这个证明一开始并不为许多数学家接受，因为不少人认为这个证明无法用人手直接验证。尽管随着计算机的普及，数学界对计算机辅助证明更能接受，但仍有数学家希望能够找到更简洁或不借助计算机的证明。

严格叙述

四色定理的通俗版本是：“任意一个无外飞地的地图都可以用四种颜色染色，使得没有两个相邻国家染的颜色相同。”

作为一个数学定理，四色定理有着更为严谨的数学叙述。

拓扑学阐述

最初的染色问题是用几何学的概念描述的，严谨的版本则需要用到拓扑学的概念来定义。设有一平面或其一部分，将其划分为互不重叠的区域的集合。一个“地图”为以下划分方式：

• 将平面划分为有限个区域，使得任意两个区域的交集是空集，所有的区域的并集是整个平面；
• 所有区域中，只有一个区域是无界区域，其余区域都是有界区域。

所谓有界区域，是指能够用一个长和宽都有限的矩形覆盖的区域。无界区域则是不能用这样的矩形覆盖的区域。每个区域相当于通俗说法中的“国家”，而区域之间的边界（“国家”之间的“国界线”）则定义为连续不自交的曲线，也称为连续简单曲线。连续简单曲线是指一个从[0, 1]映射到平面$\mathbb {R} ^{2}$的连续函数$c$的像集：$C=\{c(t);\quad t\in [0,1]\}$，并且要满足：

任意$0\leqslant t_{1}<t_{2}\leqslant 1$，只要不是$t_{1}=0,t_{2}=1$，就必定有$c(t_{1})\neq c(t_{2})$

这样说明曲线不与自身相交（没有“打结”的地方）。如果$c(0)\neq c(1)$，就称曲线为弧，否则称曲线为圈。可以看出，用边界定义地图更为本质：

平面$\mathbb {R} ^{2}$中的一张地图是指有限个简单曲线的集合：${\mathcal {L}}=\{C_{1},C_{2},\cdots ,C_{m}\},\,m\in \mathbb {N} ,m\geqslant 2$，其中$\forall 1\leqslant i\leqslant m,\,C_{i}=\{c_{i}(t);\quad t\in [0,1]\}$，$c_{i}$为[0, 1]映射到$\mathbb {R} ^{2}$的连续函数。并且任意$1\leqslant i<j\leqslant m$，曲线$C_{i}$和$C_{j}$要么没有交点（交集为空集），要么交点是两线的一个公共顶点$E_{i,j}=c_{i}(\epsilon _{1})=c_{j}(\epsilon _{2}),\;\;\epsilon _{1},\epsilon _{2}\in \{0,1\}$

${\mathcal {L}}$中每一条连续简单曲线称为地图的边。任意边的端点称为顶点。可以说，一张地图实际上是由一个简单有界平面图定义的。定义地图的边和顶点后，设所有属于边或顶点的点为中性点，其集合设为${\mathcal {N}}_{\mathcal {L}}=\{x;\,x\in C_{i},\,1\leqslant i\leqslant m\}$，则 ${\mathcal {L}}$将其余的点划分为若干个道路连通的开集。用拓扑学的语言来说，每个“国家”是$\mathbb {R} ^{2}-{\mathcal {N}}_{\mathcal {L}}$的一个极大连通子集。或者说，取一个非中性点$x$，所有能够从$x$，经过一条不含中性点的弧到达的点构成的集合，就是一个国家。这样定义的国家必然满足之前所说的特性，只有一个无界国家。要注意的是这里定义的国家必然是没有飞地的。

最后可以定义染色。假设将使用到的颜色编号为$1,2,3,\cdots ,n$号颜色，为地图染色是指一个将地图中的国家映射到$\{1,2,3,\cdots ,n\}$上的函数。一个可行的n-染色方案是指使得相邻的国家对应的颜色不同的函数。四色定理说明：每个地图都存在可行的4-染色方案。

图论阐述

拓扑学版本的四色问题阐述可以转化为更为抽象的图论版本。这里的转化指的是一种对偶的概念。即将一个地图转化为图论中的一个无向平面图。具体来说，是将地图中的每一个国家用其内部的一个点代表，作为一个顶点。如果两个国家相邻，就在两个顶点之间连一条线。这样得到的图必然是一个平面图（不会有两条边相交），而与每个国家选取的代表点无关。四色定理可以叙述为：必然可以用四种颜色给平面图的顶点染色，使得相连的顶点颜色不同。

一个四个国家的地图转化为一个平面图

要注意的是，并非所有的地图都可以转化为图论中的平面图。如果一个国家有飞地的话，就不能用只一个点来代表一个国家。另外，如果一个国家是“国中国”，那么即便可以地图其转化为平面图，也会造成讨论上的不便。但是，“国中国”的着色十分容易解决，因为它只有一个邻国，只需将它染成和邻国不一样的颜色就可以。所以在大部分有关四色问题的讨论中可以忽略“国中国”的情形。同样地，只有两个邻国的情形也可以被忽略。如果规定不能够有四个或者以上的国家有公共边界，那么地图转化成的平面图里面，每个区域都是至多由三条边围成的。这样的地图被称为正规地图。如果任何一个顶点都连出三条边，那么就称其为“三度图”（trivalent map）。可以证明，如果存在四色定理的反例，那么国家数最少的反例必定是三度图。因此在四色问题的证明过程中，常常会假设地图对应的图是三度图。

问题的提出

德摩根写给哈密顿的信件，首次提到四色猜想。现存于都柏林三一学院。

“只需要四种颜色为地图着色”最初是由法兰西斯·古德里在1852年提出的猜想。法兰西斯·古德里于1831年生于伦敦。1850年，他在伦敦大学学院完成他的数学学士学位后，又花两年时间修得法学学士学位。1852年，古德里在绘制英格兰分郡地图时，发现许多地图都只需用四种颜色染色，就能保证有相邻边界的分区颜色不同。他将这个发现告诉他的弟弟弗雷德里克·古德里。弗雷德里克这时正在伦敦大学学院读数学，师从法兰西斯上学时的老师奥古斯塔斯·德摩根。10月23日，弗雷德里克将他哥哥的发现作为一个猜想向老师德摩根提出。德摩根对此猜想很感兴趣，在同一天就在通信中将这个问题向爱尔兰数学家威廉·哈密顿提出。德摩根的信如今仍然保存在都柏林三一学院中。与德摩根的热情相反，哈密顿对这个问题丝毫不感兴趣。他在三天后的回信中告诉德摩根，他“不会尝试解决这个四元颜色问题”。

奥古斯塔斯·德摩根

四色问题之所以能够得到数学界的关注，德摩根功不可没。他推动四色问题研究的工作如此尽力，以至于许多人认为德摩根才是首先提出这个猜想的人。德摩根在接下来的两年里又尝试向别的数学家通信。他在1853年12月9日与1854年6月24日分别写信给他以前的老师威廉·魏巍尔以及魏巍尔的妹夫罗伯特·莱斯利·艾里斯，讨论四色问题。1860年4月14日，德摩根在《雅典娜杂志》上发表对魏巍尔新书的书评，其中再次提到四色定理。1854年古德里兄弟中的一人也曾在同一本杂志上发表过四色定理的文章。尽管德摩根的书评直到1876年才引起大规模的注意，但从其发表开始，已经有了一定影响。美国逻辑学家、哲学家查尔斯·桑德斯·皮尔斯看到杂志上的文章后，便向哈佛大学数学学会投递了一份尝试性证明（非真正证明），对可能的证明思路进行了一定探讨。

肯普的证明

1878年6月13日，在伦敦王家数学学会的一次会议上，阿瑟·凯莱向其他与会者询问，四色足够为地图着色的问题是否已经被证明。不久之后，他就此问题写了一篇短小的论文，对问题作了简要介绍和分析，投给英国王家地理学会，并于次年（1879年）在学会会刊上发表。凯莱的文章使得四色定理重新进入到数学家们的视野中。这一次，四色定理引起更多的注意。凯莱的论文发表尚不到一年，一份“可能是最有名的四色问题的错误证明”就出现了。

阿瑟·凯莱

作出这个证明的人是伦敦律师兼数学家阿尔弗雷德·布雷·肯普。肯普曾是凯莱在剑桥大学的学生，之前因为在联动设备模型方面的工作而出名。《自然》杂志首先确认了他的证明，于1879年7月17日登载“四色猜想得到证明”的消息。完整的证明很快在当时刚刚成立不到两年，尚未出名的《美国数学杂志》上发表。其中原因主要是创办《美国数学杂志》的詹姆斯·约瑟夫·西尔维斯特是凯莱的好友，因此肯普“应杂志主编要求”，将这篇很有分量的论文发表在相对不知名的杂志上。

《美国数学杂志》的顾问编辑威廉·爱德华·斯多利对这个问题也很感兴趣。他对肯普的证明做了一些简化，并加上多个肯普未曾处理的特殊情况下的证明，收录在再版时的附录里。1879年11月5日，在约翰·霍普金斯大学科学协会的一次会议上，这个最终版本的证明首次公开。皮尔斯当时也在约翰·霍普金斯大学任教，他也出席了这次会议，并提出自己以前的工作，又在12月的另一次会议中提出他使用逻辑方法对证明作出的改进。至此，数学界认为四色猜想已经被完全解决。

1880年，物理学家彼得·古德里·泰特也在《爱丁堡皇家学会会刊》发表一个四色猜想的新证明，然而其中只是将四色问题进行了一定的变形，依赖于肯普的工作，并没有实质的证明。

肯普的证明思路

肯普的证明是基于对国家数目进行的归纳法。很容易能证明国家数4以内时四色定理成立。肯普假设当国家数目不多于n时四色定理成立，他的目的是证明n+1个国家构成的地图都可以约化为不超过n个国家构成的地图，从而证明四色定理成立。

图1

图2

图3

肯普首先证明一个有关平面图的结论：任意地图中必定存在一个国家（顶点），其邻国数目小于等于5。证明很简单，在图论版本中，地图被转换成简单平面图。而一个简单平面图中，设V为顶点数，E为边数，F为区域数，则由于每个区域至少由三条边围成，每条边正好隔开两个区域，所以区域数和边数满足：2E ≥ 3F。假设每个顶点都至少有6条边，那么由于每条边对应两个顶点，所以顶点数和边数满足：2E ≥ 6V。合起来就有：

$V+F\leqslant {\frac {1}{3}}E+{\frac {2}{3}}E=E$

但这与图论中著名的欧拉公式：V + F = E + 2矛盾。因此不可能每个顶点都至少有六条边，也就是说，必定有一个国家的邻国数目不超过5。

接下来肯普考察n+1个国家中邻国数目最小的国家，称之为A国。A国邻国的数目不超过5个。如果A国的邻国数目不超过3个，那么可以把A国“去掉”（比如和其中一个邻国连成一体），形成一个n个国家的地图，这个地图可以用4种颜色着色，而原来的3个邻国至多用了3种颜色。这时候将A国“放回去”，染上第4种颜色，就等于找到给原地图4-着色的方法。

这种能够“去掉”一个国家，减少国家数的局部后来被称为“可约构形”（reducible configuration）。接下来肯普证明A国有4个邻国和5个邻国的情况仍然是可约构形，于是都能够化为不多于n个国家的情况。因此任何n+1个国家的地图仍然可以用四种颜色染色，因而通过归纳法可知，四色定理成立。

A国有4个邻国的时候，假如有两个邻国同色，那么可以把它们“当作”同一个国家，和A国连成一体进行约化，而由于此时这4个邻国至多用了3种颜色，所以可以将A国“放回去”，染上第4种颜色。假如4个邻国都不同色，不妨设为红、黄、蓝、绿（如右图1）。肯普的思路是将其转化为两个邻国同色的情形，他采用的方法后来被称为“肯普链”方法（Kempe chain）。具体来说，肯普希望将其中一个邻国的颜色换成“对面”的颜色，比如将绿色（图1中的绿1）换为红色。如果绿色邻国没有红色的邻国，那么换色没有任何问题；如果它有红色邻国（图1中的红1），那么需要将其红色换成绿色，……如此换下去。因此需要换色的是一条绿－红－绿－红……的“链条”，也就是所谓的“肯普链”。如果对面的红色国家不在这个链条里，那么只需要将链中的国家红绿互换，就能转化成两个邻国同色的情况（图2）。如果对面的红色国家也在链条里面（如图3），那么红绿互换就没有意义了。但是这时候可以看到，红绿“肯普链”与A国形成一个圈，所以黄色邻国和蓝色邻国必有一个在圈里（图3中是黄色邻国）。这样圈外的（蓝色）邻国的“肯普链”与圈内的（黄色）邻国必定没有交集，于是将其黄蓝互换，就能转化成两个邻国同色的情况。这说明A国与4个邻国构成可约构形。

对于A国有5个邻国的构形，肯普仍然使用肯普链的换色方式来证明其可约性。他使用了两次换色，将5种颜色降至3种，从而成为可约的构形。这也是后来希伍德找出错误的地方。

无法修正的错误

四色猜想在短短的两年时间里被一个并非“专业”数学家的“外行人”解决，让很多当初认为这个问题是难题的数学家觉得，这个问题也许并没有涉及到数学中深层的本质难点。对四色问题的研究逐渐减少，数学家们已经将其视为事实。刘易斯·卡罗尔将四色问题化为游戏：一方设计地图，另一方来为其着色。1886年，英国男校克里夫顿学院校长将四色问题作为给全校学生挑战的难题，要求答案长度“不得超过一页纸的文字，30行算式以及一页纸的图”。

德国数学家菲利克斯·克莱因甚至将这个问题和1840年莫比乌斯提出并解决的另一个问题相混淆起来，认为四色问题不过是后者的直接推论。这个误解被几何学家理查德·巴尔策在1885年重复，导致直到21世纪仍有类似的传言。而实际上莫比乌斯解决的是完全图$K_{5}$不是平面图的问题，与四色问题没有直接联系。

然而，在肯普的证明发表的11年之后，珀西·约翰·希伍德发表一篇文章，指出肯普的证明中包含一个错误。希伍德在文章中遗憾地指出，他无法修正这个错误，以得到一个四色问题的正确证明，因此他的文章更多是摧毁而非建设（rather destructive than constructive）。不过，尽管无法得到四色定理，希伍德仍然在肯普的思路上前进，得到一个较弱的定理：五色定理。

根据希伍德的说明，肯普的错误在于证明5邻国是可约构形时，构造两条肯普链以换色，然而第二次换色时，肯普的方法并不总是成功的。希伍德提供一个包含25个国家的地图作为反例。

希伍德的报告是由肯普自己提交给伦敦皇家数学学会的。肯普承认自己的证明中存在缺陷，并且他未能去除这个缺陷。然而希伍德的工作并没有受到应有的重视。数学界普遍认为这只是无关紧要的错误，很快就能得到纠正。1894年创刊的《L'intermédiaire des mathématiciens》杂志以四色问题作为头一个征解问题，结果很快就收到解答，称其已被解决，并引用了肯普、泰特等人的论文。E.吕卡的《娱乐数学》（Récréations mathématiques）第四卷提到肯普的证明，但丝毫没提到希伍德已经指出肯普证明的错处。

直到世纪之交时，数学家们仍旧认为，四色问题所需要的只是某个灵光一现的妙想。一个广为流传的故事是闵可夫斯基在教拓扑学课时提到四色问题，说：“这个问题一直没有解决，只是因为试图解决它的都是三流的数学家”。他声称要在课上证明之，但直到下课仍然无法成功，在耗费若干堂课的时间后，只能承认失败。

从欧洲到美国

20世纪起，欧洲数学界对四色定理的研究出现停滞。相反地，这个问题在美国得到更多的关注。不少杰出的数学家研究了这个问题，并作出很大贡献。一部分的努力是修正肯普的证明；另一方面的努力是延续泰特的思路，将四色问题进行转化，以使用更多有力的数学工具。

对四色问题的转化在泰特之后并未停止过。从拓扑学的版本转化至图染色的版本后，希伍德又在1898年提出新的变形。肯普和泰特已经注意到，证明四色问题只需要考虑三个国家有共同“交点”的情况，更多国家有共同交点的情形可以转化为前者。因此这样对应的染色图中，每个顶点恰会连出三条边。这样的图被称为“三度图”（trivalent map）。希伍德观察到，如果三度图中任意由边围成的区域，边的个数都是3的倍数，那么图可以被4-染色。他进一步发现，只要存在一种给图的顶点赋值+1或-1的方法，使得每个区域的顶点数字之和都被3整除，那么图可以被4-染色。可以证明，4-染色和存在赋值方法是等价的。

乔治·戴维·伯克霍夫

在美国，数学家对四色定理的研究从未停止过。除了约翰·霍普金斯大学的皮尔斯以及斯多利等人外，另一个研究者是保罗·温尼克。从当时的学术圣地哥廷根大学毕业的温尼克来到美国后在肯塔基大学任教。他1904年发表的论文中已经出现了可约性的雏形。然而美国数学界在四色问题上首次实质性的进展出现在1912年后。普林斯顿大学的奥斯瓦尔德·维布伦（经济学家托尔斯坦·范伯伦的侄子）是这波浪潮的先锋。他的工作重心是拓扑学，1905年证明了若尔当曲线定理。对庞加莱发展出的新代数工具有深入了解的他，很自然地开始对四色定理的研究。他使用有限几何学的观念和有限域上的关联矩阵作为工具，将四色问题转化成有限域系数空间上的方程问题。这个方向被后来的密码学家、数学家威廉·托马斯·塔特称为“量化方法”（the quantitative method）。同年，他的普林斯顿同僚乔治·戴维·伯克霍夫也开始探索这个方向，但一年之后他开始转向肯普的方法，也即是塔特所称的“定性方法”（the qualitative method），并提出可约环（reducible ring）的概念。1913年，伯克霍夫发表名为《地图的可约性》（The Reducibility of Maps）的论文，利用可约环证明了：由不超过12个国家构成的地图都能用四色染色。1922年，伯克霍夫的学生菲利普·富兰克林运用同样的方法，将结论加强到：不超过25个国家构成的地图都能用四色染色。由于别克霍夫首次证明四色定理对不超过12个国家的地图成立，历史上证明的可染色地图的国家数上限记录被称为别克霍夫数。

不可避免的可约构形集

伯克霍夫等人的证明是肯普的方法的延续和系统化，归纳为寻找一个不可避免的可约构形集（an unavoidable set of reducible configurations）。这个理念已经体现在肯普的证明中。他首先说明任一地图中必然存在以下四种构形：2邻国国家、3邻国国家、4邻国国家和5邻国国家；然后证明每种构形都是可约构形。后来希尔将这种分类方式称为“不可避免集”。伯克霍夫的构想是使用反证法：反设存在至少需要五种颜色染色的地图，那么其中必然存在国家数最小的“极小五色地图”（five-chromatic map）。这个地图必然是“不可约的”（irreducible）。而只要找到一组构形，使极小五色地图中不可避免地会出现其中一种构形，并且每个构形都是可约的，那么就能够通过约化，将地图的国家数减少，从而导致矛盾。

肯普使用的不可避免构形集：邻国有2、3、4、5个的国家。

伯克霍夫菱形：由6个国家（红点）构成的环围着4个国家组成的构形。

肯普找的不可避免集由四种构形组成，但他无法证明最后一种（5邻国国家）的可约性，因此伯克霍夫开始寻找刻画不可避免集的新方法。他提出以相邻国家连成的环来将整个地图M分为三个部分：环内部分A、环外部分B以及环本身R。若环上的国家数为n就称其为n-环。如果R的任意染色都不妨碍A进行染色，那么就可以“忽略”A而将M的染色问题约化为B+R的染色问题。这时便称A+R是可约构形，R称为可约环。伯克霍夫证明了：当R是4-环，或者R是5-环且A中国家不止一个，或者A+R是“伯克霍夫菱形”时，A+R都是可约的构形。因此极小五色地图不可能包含这些构形。富兰克林进一步证明：极小五色地图中必定包含三个邻接的五边国（5邻国的国家），或者邻接的两个五边国与一个六边国，或者邻接的一个五边国和两个六边国。他从而得出一系列的可约构形，形成了25国以下地图的不可避免的可约构形集。因此推出，极小五色地图必定至少包含26个国家。

富兰克林发现，极小五色地图必定包括以上6种情形之一。

这种方法的终极目标是找到所有地图的不可避免的可约构形集。然而随着国家数增多，要找到不可避免集并证明其可约化性就越难。这主要是因为随着环的增大，染色的方法数目会迅速增大。6-环的4-染色方法有31种，而12-环则有22144种。因此对大环围成的构形验证可约性是十分繁杂的工作。1926年，C.N.Reynolds将别克霍夫数从25提高到27。1938年，富兰克林将其推进到31。1941年，C.E.Winn将之提高到35。而直到1968年，别克霍夫数才更新为40。

四色问题研究的下一个突破并不是在美国，而是由哥廷顿大学出身的德国数学家亨利·希尔带来的。他在1948年提出不可避免集的存在性，但他提出的不可避免集可能包含10000个构形，其中还有18-环的庞大构形。希尔的另一个成果是在1969年提出“放电法”（discharging method），为寻找不可避免集给出了系统的方法。

放电法

放电法利用地图转换成图染色后成为平面图的特性，将其看作是平面的“电网”，并将每个“节点”按照度数（连出的边数）分类。首先在每个度数为k的节点放置6 - k的电荷。根据平面图和极小五色地图的特性，有下列恒等式：

$A_{5}-A_{7}-2A_{8}-3A_{9}-\cdots -(s-6)A_{s}=12.$

其中$\forall k\in \mathbb {Z} ,\,\,A_{k}$表示度数为k的节点个数，s为节点最大度数。“放电”的过程（discharging procedure）指的是将这些电荷以特殊的规则进行重新分配，从而找出“电网”结构上的特性，建立不可避免集。具体来说，可以假设某些构形全不存在，然后构造一个放电过程，使得接受电荷的总量不再等于释放电荷的总量，从而导出矛盾（电荷不守恒）。每个良好设计的放电过程都能证明一个不可避免集的存在。

计算机的辅助

人工寻找不可避免构形集和验证构形可约性过于缓慢，数学家开始考虑使用当时新出现的计算机作为辅助，以提高验证的效率。构造出放电法的同时，借助于计算机来验证构形可约性的工作也飞速进展。希尔在Karl Dürre的帮助下在1965年设计了第一个算法来验证构形的可约性。他们使用的是Algol 60语言，在德国汉诺威技术学院计算机中心的一台CDC 1504A电脑上首次运行。1967年前，由于内存不足，只能验证12-环以下的构形。而希尔找出的不可避免集含有的大构形可以达到14-环甚至更多，计算机的能力并不足以快速完成可约性的验证。

当时美国的计算机技术领先于欧洲，因此希尔希望能够借助美国的大型计算机来证明四色定理。1967年，美国纽约布鲁克海文国家实验室（BNL）应用数学院院长邀请希尔来美国访问，并允许他使用当时世界上最快的计算机CDC 6600。其后几年，希尔两度到美国寻求大型计算机的使用机会。这段时间中，Dürre将程序用FORTRAN进行重写。抱着在德国最终解决四色问题的希望，希尔回到德国，但令他失望的是，德国学术界对他的计划持否定态度，并不愿为他的程序拨出计算时间。

在数次访美时，希尔开始与沃夫冈·哈肯合作。哈肯在1948年曾经旁听过希尔提出不可避免集的课程，之后对四色定理产生了持续的兴趣。两人通过信件交流合力作出很多进展，为最终解决四色问题铺平道路。1971年，阿佩尔也开始在哈肯的介绍下研究四色问题。然而当时哈肯对解决四色问题的前途感到悲观，因为寻找并验证合适的不可避免可约构形集实在过于复杂，即便借助计算机也需要过多的时间。塔特当时也认为，即便最乐观的估计中，不可避免集也要包含至少8000个构形。然而塔特等人也将希尔的工作介绍到美国（当时希尔的工作只在德国发表过），并引发了很多人的热情。包括弗兰科·阿莱尔、爱德华·雷尼尔·斯瓦特、弗兰科·R·伯恩哈特等人都开始寻找不可避免集以及检验可约性。哈肯和阿佩尔依赖于计算机的工作能力，因此不断改良放电过程。他们将通过放电过程寻找不可避免集的算法和验证可约性结合起来，当某个不可避免集的构形不是C-可约（可约性的一种）或难以被验证为C-可约的时候，就放弃这个不可避免集，以提高效率。两人设定了很多经验性的修正规则，比如设定三个经验性的“障碍”（三种特定的构形），当某个构形中含有这种障碍就直接认为是不可约的；又比如构形的大小不能超过14-环，等等。

定理的证明

1975年，哈肯找到一种很好的放电过程，但难以化为算法程序。于是两人暂时开始回归纸笔计算。这时候他们得到当时还是博士学生的约翰·科赫（John A. Koch）的支持，后者对他们提供了可约性验证算法工作上的帮助。1976年3月，他们终于得到一个由1936个构形组成的不可避免集，对应的放电过程由487条规则构成。同时伊利诺伊大学的主电脑也更换成运算速度更高的IBM 360，为计算节省大量时间。经过电脑1200小时的验证，他们终于在6月得出：1936个构形都是可约构形。这代表着四色定理最终的解决。这时候他们的几个竞争对手如阿莱尔、斯瓦特等的工作也将近尾声。

1976年6月22日，哈肯和阿佩尔首次在美国数学协会（M.A.A.）于多伦多大学召开的美国数学学会（A.M.S.）夏季会议公布他们的结果。不久，伊利诺伊大学数学系的邮戳上加上了“四种颜色就够了”（FOUR COLORS SUFFICE）的一句话，以庆祝四色猜想得到解决。9月，美国数学学会的公告专栏上刊登了两人证明四色定理的消息。

1977年，哈肯和阿佩尔将结果写成名为《任何平面地图都能用四种颜色染色》（Every planar map is four colorable）的论文，分成上下两部分，发表在《伊利诺伊数学杂志》（Illinois Journal of Mathematics）上。

争议、修正与改良

如果四色问题有一个不依赖计算机的证明，我会更加开心，但我也愿意接受阿佩尔和哈肯的证明——谁叫我们别无选择呢？

（I would be much happier with a computer-free proof of the four color problem, but I am willing to accept the Appel–Haken proof – beggars cannot be choosers.）

“

”

保罗·埃尔德什，1991年

参见：电脑协助证明

四色定理是第一个主要由电脑验证成立的著名数学定理。这一证明刚开始并不被所有的数学家接受。1979年，逻辑哲学和数学哲学家托马斯·蒂莫兹佐在《四色定理及其哲学意义》一文中提出，四色定理与其证明能否称之为“定理”和“证明”，尚有疑问。“证明”的定义也需要进行再次审视。蒂莫兹佐的理由包括两点：一方面，计算机辅助下的证明无法由人力进行核查审阅，因为人无法重复计算机的所有运算步骤；另一方面，计算机辅助的证明无法形成逻辑上正则化的表述，因为其中的机器部分依赖于现实经验的反馈，无法转换为抽象的逻辑过程。即便在数学界中，对四色定理证明的误解也存在着。有的数学家认为证明是杰出的进展，也有人认为依赖计算机给出的证明很难令人满意。也有人认为，计算机辅助证明数学定理不过是对人的能力进行延伸的结果，因为电子计算机不过是依照人的逻辑来进行每一步的操作，实际上只是将人能够完成的工作用更短的时间来完成。还有人将计算机辅助证明和传统证明的差别比喻为借助天文望远镜发现新星和用肉眼发现新星的区别。

针对证明过程冗长、难以理解的问题，哈肯等人也着手对证明进行改良。简化证明的一个方向是寻找更小的不可避免集和更加容易验证的可约构形。哈肯等人很快将不可避免构形集的大小从1936个改进到1476个。1994年，罗宾·托马斯等人又将其改进到只包含633个构形、32个放电规则的放电过程推出的不可避免构形集。由于著名的前车之鉴，数学家们对证明进行详细审视，发现了大量缺漏和错误。特别是厄里奇·史密德等人曾经检查人工证明部分的40%，并发现放电过程中的一个关键性错误。幸好，这些缺陷和错误都是能够修正的。不过，修正的工作也持续了若干年，才最终完成。修正过程中也出现各种传言，说四色定理的证明其实是错误的。1986年，哈肯和阿佩尔应《数学情报》杂志的邀请写了一篇短文，用清晰易懂的语言总结他们的证明工作。1989年，最终的定稿以单行本的形式出版，超过400页。

对于机器证明的可靠性问题，2004年9月，数学家乔治·龚提尔使用证明验证程序Coq来对当时交由计算机运算的算法程序进行形式上的可靠性验证。证明验证程序是一个由法国开发的软件，能够从逻辑上验证一段电脑程序是否正常运行，并且是否达到了它应该达到的逻辑目的。验证表明，四色定理的机器验证程序确实有效地验证所有构形的可约性，完成了证明中的要求。至此，除了机器硬件、软件可能存在问题外，四色定理的理论部分和计算机证明算法部分都得到验证。

尽管绝大多数数学家对四色定理的证明已经不再有疑问，某些数学家对经由电脑辅助的证明方式仍旧不够满意，希望能找到一个完全“人工”的证明。正如汤米·R·延森和比雅尼·托夫特在《图染色问题》一书中问的：“是否存在四色定理的一个简短证明，……使得一个合格的数学家能在（比如说）两个星期里验证其正确性呢？”

实际应用

如果A国有飞地，则必须有第五种颜色。

虽然四色定理证明任何地图可以只用四个颜色着色，但是这个结论对于现实上的应用却相当有限。据凯尼斯·梅所言：“（实际中）用四种颜色着色的地图是不多见的，而且这些地图往往最少只需要三种颜色来染色。地图学和地图制图史相关的书籍也没有四色定理的记载。”现实中的地图常会出现飞地，即两个不连通的区域属于同一个国家的情况（例如美国的阿拉斯加州），而制作地图时仍会要求这两个区域被涂上同样的颜色。此外，即便地图能够只用四种颜色染色，为了区分起见，也会采用更多的颜色，以提示不同地区的差别。

染色算法

地图染色算法是一个应用的问题：能否给出一个算法，将一个地图进行k-染色，或判定它不能k-染色？当k = 2时，存在多项式时间的算法。只需将某个国家随机染上一种颜色，然后它的邻国就只能染成另一种颜色，邻国的邻国的颜色也随之确定……这个算法等价于广度优先搜索，因此是多项式时间的。当k = 3时，可以证明这个问题是NP完备的，即若P≠NP，则不存在多项式时间的算法。对于k = 4的情况，阿佩尔和哈肯在1989年的单行本的附录中给出一个完整的多项式时间的算法及其证明。

曲面地图染色

一个需要7色的环面地图：每个国家都和其余6个相邻。

平面地图卷成环面地图的示意图

参见：曲面染色

四色问题探讨的是平面上地图的染色问题。更一般的情况：曲面上地图的染色问题是由希伍德开始研究的。他在1890年的论文中不仅指出肯普的错误，而且运用肯普的方法证明了五色定理。在此之后，希伍德又将注意力转移到更一般的曲面染色问题上。他证明能够对S_k上面任何的地图进行染色，使得相邻两国不同色所需要的最少颜色数目Col(S_k)有上限：

7－染色的环面

$\operatorname {Col} (S_{k})\leqslant \left\lfloor {\frac {7+{\sqrt {1+48k}}}{2}}\right\rfloor .$

其中的S_k是指亏格为k（有k个“洞”）的曲面（或者说二维可微流形），$\left\lfloor \cdot \right\rfloor$表示下取整函数。他还证明当亏格为1，也就是曲面为环面的时候，存在至少要用7种颜色才能染色的地图。而环面对应的上限不等式是：

$\operatorname {Col} (S_{1})\leqslant \left\lfloor {\frac {7+{\sqrt {1+48}}}{2}}\right\rfloor =7.$

因此希伍德证明了$\operatorname {Col} (S_{1})=7$：最多用7种颜色就能为任何环面上的地图染色。

希伍德猜测，一般的曲面地图染色中，上面的不等式也可以变成等式。他提出猜想：任意的可定向曲面上，最多只用$\left\lfloor {\frac {7+{\sqrt {1+48k}}}{2}}\right\rfloor$种颜色就能为任意的地图染色，其中k是曲面的亏格。这个猜想被称为希伍德地图染色问题或者希伍德猜想。当k = 0的时候，这个猜想就变成四色猜想。

进一步的推导可以将这个猜想分为12种情况。但仅仅在证明了其中一种和几个较小的k的情况后，由于文献上的误导，不少数学家错误地以为问题已经得到解决。1950年后，有关的研究才重新开始。1968年，杰拉德·林格尔和约翰·威廉·西奥多·杨格斯最终证明了这个猜想在k ≥1时的情况。而随着1976年，k = 0情况（也就是四色定理）的最终证明，希伍德猜想最终获得完整的解决。此后希伍德猜想也开始被称为希伍德地图定理或林格尔－杨格斯定理。

参见

• 图染色

  更加一般的染色问题，讨论任意的图的点或边染色时的性质。

• 哈德维格－尼尔森问题

  需要用多少种颜色给平面上的点染色，才能够使任何两个距离是1的点染的颜色都不同？

• 拉姆齐问题

  最少要有几个人，才能保证其中必然有k个人两两相识，或者l个人两两不相识？这等价于讨论完全图2-染色的性质。

• 曲面染色

外部链接

• Hazewinkel, Michiel (编), Four-colour problem, 数学百科全书, Springer, 2001, ISBN 978-1-55608-010-4 
• 埃里克·韦斯坦因. Blanuša snarks. MathWorld. 
• 埃里克·韦斯坦因. Map coloring. MathWorld.