四色定理

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

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

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

四色定理的通俗版本是：“任意一个无飞地的地图都可以用四种颜色染色，使得没有两个相邻国家染的颜色相同。”作为一个数学定理，四色定理有着更为严谨的数学叙述。

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

所谓有界区域，是指能够用一个长和宽都有限的矩形覆盖的区域。无界区域则是不能用这样的矩形覆盖的区域:44。每个区域相当于通俗说法中的“国家”，而区域之间的边界（“国家”之间的“国界线”）则定义为连续不自交的曲线，也称为连续简单曲线。连续简单曲线是指一个从映射到平面${\displaystyle {\mathbb{R}}^2}$）第四卷提到肯普的证明，但丝毫没提到希伍德已经指出肯普证明的错处:108。

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

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

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

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

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

肯普找的不可避免集由四种构形组成，但他无法证明最后一种（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都是可约的构形。因此极小五色地图不可能包含这些构形:169。富兰克林进一步证明：极小五色地图中必定包含三个邻接的五边国（5邻国的国家），或者邻接的两个五边国与一个六边国，或者邻接的一个五边国和两个六边国。他从而得出一系列的可约构形，形成了25国以下地图的不可避免的可约构形集。因此推出，极小五色地图必定至少包含26个国家。

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

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

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

其中${\displaystyle \mathrm{\forall <!--\; \forall \; -->}k\in <!--\; \in \; -->\mathbb{Z},A_k}$）的论文，分成上下两部分，发表在《伊利诺伊数学杂志》（）上。

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

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

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

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

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

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

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

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

因此希伍德证明了${\displaystyle \mathrm{Col}<!--\; \; -->(S_1)=7}$：最多用7种颜色就能为任何环面上的地图染色:218。

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

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