四色定理

一个直觉：给英格兰各郡上色时，一个学生发现总也用不到第五种颜色#

1852 年，一个叫弗朗西斯·格思里的年轻人正在给一张英格兰各郡的地图涂色，想让相邻的郡颜色不同。他注意到一件怪事：不管地图多复杂，自己好像永远只要四种颜色就够，从没被逼着拿出第五种。他把这个观察告诉弟弟，弟弟又转告了老师德·摩根——一句涂地图涂出来的疑问，就此变成数学难题。

这个问题"小学生都听得懂，数学家却证不出来"。它熬了一个多世纪，直到 1976 年，伊利诺伊大学的阿佩尔和哈肯让计算机连续算了约 1200 小时，逐一核对 1936 种构形，才得出结论。庆功时阿佩尔在黑板上写道："只要仔细核对无误，看来四种颜色就够了。"那阵子，系里寄出的每封信都盖着一枚邮戳——"Four colors suffice"（四色足矣）。这是历史上第一个靠计算机才完成的数学证明，也由此引出一个争论：人脑无法逐行复核的证明，还算证明吗？

定理陈述#

四色定理（Four Color Theorem）是图论和拓扑学中的经典定理。

任何平面地图都可以用至多四种颜色着色，使得任意两个相邻区域（共享一段边界，而非仅一个点）的颜色不同。

等价的图论表述：任何平面图的色数不超过 4，即 $\chi(G) \leq 4$。

直觉理解#

四色定理的陈述简单到小学生都能理解：给一张地图上色，相邻国家用不同颜色，只需四种颜色就够了。

为什么是 4 而不是 3？想象三个区域互相相邻（如三个国家各两两接壤），需要 3 种颜色。但第四个区域如果与前三个都相邻，就需要第 4 种颜色。四色定理说：4 种颜色永远足够——无论地图多么复杂。

为什么不是 5？这就是定理的深刻之处——虽然构造需要 4 种颜色的地图很容易，但证明 4 种颜色总是够用却极其困难。

证明思路#

四色定理的证明是数学史上最具争议的——它是第一个借助计算机证明的数学定理。

肯普的尝试（1879）#

阿尔弗雷德·肯普（Alfred Kempe）声称证明了四色定理。他的方法是"不可避免集"和"可约构形"。

• 不可避免集：任何平面地图中必然包含某些特定的局部构形
• 可约构形：如果地图包含某个可约构形，则可以用更少的颜色着色

肯普证明了所有平面图都包含一个"可约"的构形，因此不需要 5 种颜色。但 1890 年，希伍德发现肯普的证明有一个错误——五色定理是成立的，但四色定理的证明有缺陷。肯普的方法没有作废：不可避免集加可约构形，仍是后来计算机证明的骨架。错的是某几步归约。希伍德用修好的骨架给出五色定理——平面图五色够用，证明可以手写。四色把缺口留了一个世纪。1976 年阿佩尔与哈肯把构形清单交给机器逐条核对；1997 年 Robertson、Sanders、Seymour、Thomas 把清单缩短并写成更可复核的程序。争论从"四种够不够"变成"人无法逐行读完的证明算不算证明"。计算机没有取消数学，它把检验标准从纸面搬到了可重复运行。

把四色说成地图问题，对偶之后就是平面图的顶点着色。格思里涂的是国家，数学家画的是顶点与边。肯普 1879 年的论证已经用上了欧拉公式保证低度顶点、以及沿双色路径交换颜色的技巧；希伍德 1890 年指出其中一处交换在四色情形会互相干扰，于是四色倒下、五色站住。海因里希·黑施（Heinrich Heesch）在二十世纪中叶把可约构形与放电法（discharging）写成可执行的清单策略，阿佩尔与哈肯接的是这根接力棒，不是从空白处发明穷举。

阿佩尔和哈肯的证明（1976）#

肯尼斯·阿佩尔和沃尔夫冈·哈肯在 1976 年完成了四色定理的证明：

1. 找到了一个包含 1936 个构形的不可避免集
2. 用计算机逐一验证每个构形都是可约的
3. 因此任何平面地图都包含一个可约构形，四色定理成立

计算机运行了约 1200 小时。这一证明引发了关于"什么是数学证明"的哲学讨论。人不能也不该假装把一千多个构形在黑板上走完。可重复运行、独立实现、后来的 Coq 形式化，是新的核对方式。证明的社会合同从"杰出读者点头"扩成"机器与人一起担保"。拒绝承认计算机证明的人，要回答：人类审稿是否真的逐行看过所有长证明。四色把这个问题从礼貌变成了必须表态。

罗伯逊等人的简化证明（1997）#

罗伯逊、桑德斯、西摩和托马斯将不可避免集缩小到 633 个构形，但仍需计算机验证。2005 年，乔治·贡蒂尔用 Coq 证明助手给出了完全形式化的验证。

历史背景#

四色猜想由弗朗西斯·格思里（Francis Guthrie）在 1852 年提出——他在给英国地图着色时发现了这一规律。他的老师德·摩根将其传播开来。

四色定理的证明历程： - 1879：肯普的错误证明 - 1890：希伍德证明五色定理 - 1976：阿佩尔和哈肯的计算机证明 - 1997：罗伯逊等人的简化计算机证明 - 2005：贡蒂尔的形式化验证

四色定理是数学中为数不多的"表述简单但证明极难"的问题——它推动了图论、拓扑学和计算机辅助证明的发展。相邻必须共享一段边界，只在一个点相碰不算相邻。这个定义把"点邻接"的假反例挡在门外。画一张看起来需要五色的图，检查下来总有两块其实只点碰。小学生能听懂的题，细节写在"相邻"两个字上。寄存器分配把变量冲突画成图，色数对应同时活着的变量数；那是图着色，不一定平面，四色管不到。定理的工程亲戚是着色，不是地图本身。平面性是四色的门票。一旦允许边交叉，色数可以任意大：完全图 K_n 需要 n 色。无线基站的干扰图很少是平面的，所以工程上用的是启发式着色，不是四色定理的推论。把定理直接写成"频率分配只要四种"，会把平面条件丢掉。数学够用的地方，先问图能不能画在平面上不交叉。

泰特（Peter Guthrie Tait）在十九世纪给出过一个等价说法：每个无桥的三次平面图，边可以用三种颜色着色。这个表述把四色译成了边着色，也引出了"斯纳克"（snark）这类反例候选——非三边可着色的三次图。它们大多不是平面的，所以并不推翻四色，只说明离开平面性之后着色可以立刻变难。工程上的干扰图、寄存器冲突图很少保证平面，因此四色定理几乎从不直接给频率或寄存器发通行证。

应用#

1. 地图着色：实际地图制作中的颜色分配
2. 频率分配：无线通信中避免相邻基站使用相同频率
3. 寄存器分配：编译器优化中的变量寄存器分配问题
4. 调度问题：考试排课、交通信号等避免冲突的调度
5. 计算机辅助证明：四色定理的证明开创了计算机辅助数学证明的先河

与其他定理的关系#

• 五色定理：$\chi(G) \leq 5$——可以用纯数学方法证明
• 欧拉公式：$V - E + F = 2$——平面图的基本性质，是可约性分析的基础
• 库拉托夫斯基定理：平面图的刻画——不包含 $K_5$ 或 $K_{3,3}$ 的细分
• 海希特-塔特定理：三色定理的充分必要条件
• 哈德维格猜想：四色定理的推广——至今未解决。若图的色数至少 t，则它应包含完全图 $K_t$ 作为 minor；t = 4 时该猜想等价于四色，更高的 t 仍未完全解决。于是四色既是终点也是台阶：它关掉了平面地图的颜色问题，同时给更一般的 minor 理论留了一扇必须继续推的门。

数学细节#

为什么五色定理容易证明#

五色定理（$\chi(G) \leq 5$）可以用纯数学方法简洁证明：

步骤 1：由欧拉公式 $V - E + F = 2$，平面图中必存在度数 $\leq 5$ 的顶点。

步骤 2：对顶点数 $n$ 做归纳。设 $G$ 有 $n$ 个顶点，取度数 $\leq 5$ 的顶点 $v$。去掉 $v$ 后的图 $G - v$ 可以用 5 种颜色着色。

步骤 3：如果 $v$ 的邻居用了 $\leq 4$ 种颜色，则 $v$ 可以用第 5 种颜色。如果 $v$ 的邻居恰好用了 5 种颜色，通过 Kempe 链论证可以重新排列颜色，腾出一种给 $v$。

为什么四色定理困难#

从 5 到 4 的跨越极其困难。Kempe 链论证在 4 种颜色时失效——因为需要处理的特殊情况太多。阿佩尔和哈肯的方法本质上是穷举所有特殊情况，这需要计算机。

计算机证明的哲学问题#

四色定理的证明引发了深刻的问题： - 一个只有计算机能验证的证明还算"证明"吗？ - 如果人类无法理解证明的每一步，我们能"知道"定理为真吗？ - 未来的数学证明是否都需要计算机辅助？

这些问题至今仍在讨论中。

更强的结果#

四色定理有一些有趣的推广和变体：

• 五色定理：$\chi(G) \leq 5$——可以用纯数学方法证明
• 六色定理：$\chi(G) \leq 6$——证明更简单
• 平面图的边着色：维辛定理——平面图的边色数为 4 或 5
• 希伍德地图着色定理：亏格为 $g$ 的曲面需要 $\lfloor(7 + \sqrt{1 + 48g})/2\rfloor$ 种颜色
• 四色定理的对偶：每个平面图是 4-可着色的 $\Leftrightarrow$ 每个平面图的对偶是 4-边可着色的

四色定理与其他着色问题#

四色定理属于图着色理论的一部分，该领域有许多相关但不同的问题：

列表着色：每个顶点有一个允许颜色的列表，问题是能否从各自列表中选择颜色使得相邻顶点颜色不同。列表着色猜想（1979）断言：每个图的列表色数等于其色数——至今未解决。

全着色：同时对顶点和边着色，使得相邻顶点、相邻边、以及关联的顶点和边颜色不同。全着色猜想（Behzad，1965）断言：每个图的全色数不超过最大度加 2。

分数着色：允许顶点分配颜色的概率分布——分数色数可以取非整数值。分数色数与线性规划和信息论有深刻联系。

无圈着色：着色的每个颜色类导出的子图都是森林。无圈色数通常比普通色数大，但不超过最大度的两倍。

形式化验证的意义#

2005 年贡蒂尔用 Coq 证明助手完成了四色定理的形式化验证，这一成就的意义超越了四色定理本身：

可靠性：形式化验证消除了对计算机程序正确性的信任假设——证明的每一步都由证明助手检查。人类审查者只需验证少数公理和推理规则。

方法论：形式化验证展示了交互式证明助手在复杂数学证明中的潜力。此后，Hales 的开普勒猜想（Flyspeck 项目）和 Feit-Thompson 奇数阶定理也被形式化验证。

未来展望：随着 AI 辅助证明（如 Lean、Isabelle/HOL）的发展，形式化数学可能成为数学研究的标准实践——从"证明可能有错"到"证明已被机器验证"的范式转变。

计算复杂性#

四色定理的计算版本——给定一个平面图，找到其 4-着色——是多项式时间可解的。然而：

• 判定一个图是否是 3-可着色的是 NP-完全问题
• 判定一个图是否是 2-可着色的（二分图判定）是多项式时间可解的
• 平面图的 3-着色问题仍是 NP-完全的

这意味着从 3 色到 4 色的跨越在计算复杂性上具有本质差异——知道 4 色总是够用使得问题变得更容易。

跨域连接#

• 证明：证明的社会功能是让别人能复核。当结论依赖上千种构形的机器枚举，复核权就从个人转移到了程序与硬件。争议的真正焦点不是结论对不对，而是我们凭什么说自己知道它对——这是对证明这一概念本身的追问，而不是对图论的追问。
• 形式化方法与验证：后来的形式化把信任压缩到一个很小的核上：只要相信证明助手的内核，并相信定理陈述译得对，中间的海量步骤都不必人看。这是一条通用策略——把不可复核的庞大论证换成可复核的小基底，代价是必须先把问题完整地翻译进形式语言。
• 记忆系统：人能同时把握的项数极少，逐一比对上千种构形超出容量好几个数量级。所谓"人类可读的证明"从来就有一个认知上限，只是过去的数学恰好没撞到它。撞到之后，"可读"不再是证明的定义性要求，而成了一种对人有用的附加属性。
• 知识论：相信一个自己没走完的证明，属于证词性知识——你信的是来源可靠。机器证词与人的证词并非同类：程序的可靠性可以被独立测试并重复运行，人的可靠性只能靠声誉估计，这一点反而让机器证词更容易被审查。
• 循证医学：证据等级制度面临同样处境：当结论建立在超出个人复核能力的数据合并之上，临床医生实际相信的是流程而非内容。推论是流程必须可被外部审计——原始数据、分析代码与预注册方案的公开，作用相当于数学里的形式化脚本。

参考文献#

1. Kenneth Appel & Wolfgang Haken, "Every Planar Map is Four Colorable" (1977).
2. Robin Wilson, Four Colors Suffice (2002).
3. Thomas L. Saaty & Paul C. Kainen, The Four-Color Problem (1986).
4. Georges Gonthier, "Formal Proof—The Four-Color Theorem" (2008).
5. David Barnette, Map Coloring, Polyhedra, and the Four-Color Problem (1983).
6. Heinrich Heesch, Untersuchungen zum Vierfarbenproblem (1969).
7. Neil Robertson, Daniel Sanders, Paul Seymour & Robin Thomas, "The Four-Colour Theorem" (1997).

四色定理断言：任何平面地图都可用四种颜色着色，使相邻区域颜色不同。它由阿佩尔与哈肯于 1976 年借助计算机逐一检验一个含 1936 个可约构形的不可避免集而证明，是首个本质依赖计算机的重大数学证明，并由此引发了关于"机器证明是否算证明"的长期讨论。