四色定理：一个百年前的故事，影响至今

——从一张地图，到 AI 时代的「证明」

timeobserver137 配套博客 · 4CT 集 视频讲直觉，博客补严格证明。

写在前面

看完了这期节目，我想说说目前自己对人工智能、以及它所带来的冲击的看法。直接下结论：AI 无论如何也不会、也不应该取代人。

AI 的诞生本身就是具有目的性的，它从来都不是为了"创造一个人"而被造出来的；现在的主流观点倾向于认为，它的目的是成为人类的认知工具——那么它"工具"的性质，也就很明确了。而我们人类的诞生，并不是一开始就有目的性的，因此我们总会做一些看似没有目的性的事情：我们会坚持一场看上去必输无疑的比赛，会享受午后温暖的阳光，也会体会到生离死别的悲伤。这些事情，以后或许能被模拟，但永远替代不了我们自身的感受。

回到数学——AI 是工具，而发现并理解数学之美的，是我们人。

下面这篇文章，就是顺着"什么才算证明、是谁的证明、凭什么相信它"这条线，从一张地图一直走到今天的 AI，去把上面这个结论一步步走实。

— yeqiu

引子：一个被信了十一年的错证明

1852 年，一个刚从法学毕业的年轻人 Francis Guthrie 在给英格兰各郡的地图上色时，注意到一件怪事：好像四种颜色，怎么涂都够。他自己证不出来，便托弟弟 Frederick（当时正是 De Morgan 的学生）去问老师——大数学家 Augustus De Morgan。同年 10 月 23 日，De Morgan 写信给 Hamilton，留下了这个问题最早的书面记录。

二十多年后，1879 年，伦敦执业大律师、业余数学家 Alfred Kempe 发表了一篇短文，宣布证明了它。学界挑不出毛病，便当它解决了。（Kempe 本人于 1881 年当选皇家学会会员，但提名主要是表彰他在连杆机构与运动学上的工作，并非这篇四色证明。）

可十一年后——1890 年——Percy Heawood 发现这个证明是错的。

一个错的证明，被所有人信了十一年。这件事比那道题本身更值得琢磨：当我们说一个命题"被证明了"，究竟是凭什么判断的？是真有人一步步检查过，还是只是大家看着挑不出毛病、就先当它对了？

这篇文章顺着这个问题，从一张地图，一直走到今天的人工智能。

目录

• §1 问题本身 — 四色定理是什么；为什么不是三色、为什么"四"在平面上特殊（$K_4$ / $K_5$）
• §2 从地图到点线图 — 把地图抽象成平面图
• §3 Kempe 链与五色定理 — 欧拉公式、必有度 ≤ 5 的点、Kempe 链对换：先证"五色一定够"
• §4 为什么 Kempe 的"四色"会塌 — Heawood 1890 的漏洞、Errera 图、Tait 边染色
• §5 机器证明 — 不可避免集、可约性、放电法；1976 → Coq，以及"证明本身就是一段程序"
• §6 AI 时代的信任危机 — 同一个问题，在 AI 时代更危险地重演

§1 问题本身

四色定理：任何一张平面地图，只用四种颜色，就能让相邻的区域颜色不同。这里"相邻"指共享一段有长度的边界——只在一个点上碰到不算。

几个先要说清的事实：

• 为什么不是三种？ 你能画出四个两两相邻的区域（即完全图 $K_4$），这时第四块无论涂什么都撞上前三块，所以三色不够。
• 为什么不会被"五个两两相邻"逼出第五种颜色？ 先想清楚我们到底在找什么：要推翻四色定理，最直接的办法就是举一个反例——拿出一张真的需要五种颜色的平面地图。 而最显眼的反例候选，就是"五个区域两两都相邻"：假如真有这样五块，那每一块都和其余四块挨着、颜色必须两两不同——五块就非用五种颜色不可（这正是"逼出第五色"的意思）。所以这样一张图只要真能在平面上画出来，四色定理当场就被推翻了。 可这五个两两相邻的区域，画成点线图正是完全图 $K_5$（五个点、两两连边），而$K_5$ 在平面上根本画不出来——由后面的引理 3.2 直接给出（$K_5$ 有 $10$ 条边，超过 $E\le 3V-6 = 9$ 的上界，任何画法都总有两条边非交叉不可）。所以这个最显眼的反例，在平面上根本造不出来。但请注意：造不出 $K_5$ 这一个反例，并不等于证明了四色一定够——没准还有别的、不长 $K_5$ 样子的平面结构需要五色（其实没有，但要排除"所有"这种可能，得靠后面那个难得多的证明）。
• 换个曲面，"四"立刻失去特殊性。 环面（甜甜圈面）上需要 七 色；克莱因瓶上六色。"四"是平面与球面独有的——这恰恰是它难证的根源。

为什么偏偏是「四」这么难：下界、上界，与中间那个「1」的缝

上面环面要七色、克莱因瓶要六色——这些数字到底是怎么"钉死"的？这里藏着全篇最深的一个区分，也是四色之所以难的真正原因。要确定"某个曲面上够用几种颜色"，必须有两半，缺一不可：

• 下界（至少要几种） 靠构造：在这个曲面上真的排出 $n$ 个两两相邻的区域。它们既然两两挨着，就非 $n$ 种颜色不可——于是"至少要 $n$ 种"。
• 上界（几种就够） 靠欧拉公式：把 $V-E+F$ 在这个曲面上的值算出来，推出"边不会太多"，于是图里总有一个度数不高的顶点；删掉它、把剩下的涂好、再放回来填色，归纳下去就证出"$n$ 种就够"。

只有当下界和上界正好对上同一个数，才能说"恰好 $n$"。

环面就是两边自然合拢的例子：构造上能在甜甜圈表面实打实排出 7 个两两相邻的区域（$K_7$ 摆得下）→ 至少要 7；而环面的 $V-E+F=0$（平面是 2），由此可推出总有一个度 $\le 6$ 的顶点——这是上界论证的起手，但不是结论。从这里再走一遍 §3 那种"删掉低度顶点 → 对更小的图归纳染色 → 放回来给它填色"的套路（只是这次要凑齐的是 7 种、不是 5 种），才证出7 种就够。换句话说，环面的上界 7 和 §3 认真证的"平面度 $\le 5$ ⇒ 五色够"是同一类归纳论证，并不是由"度 $\le 6$"一句话直接白送的——它本身就是一条要证的定理（环面七色定理）。两边都做实之后，下界 7 = 上界 7 → 恰好 7。所以"环面七色"不是只靠那张构造图，是构造（下界）与欧拉归纳（上界）两边一起夹出来的。

而平面，偏偏是两边对不上的那一个：

• 下界：能造出 $K_4$（四个两两相邻）→ 平面至少要 4。
• 上界：同一套欧拉归纳，在平面上 $E\le 3V-6$ → 总有度 $\le 5$ 的顶点 → 轻松能证到「5 种就够」（这正是 §3 我们要动手证的五色定理）。
• 于是你手里是：下界 4、容易够到的上界 5——中间整整差了一个 1。

这条「1」的缝，就是整部四色定理。 "其实四种就够、根本用不到第五种"——把上界从 5 压到 4，正是那个困了数学界一百多年、最后不得不靠计算机才解决的难题。在可定向曲面里，平面与球面是唯一"下界"与"容易上界"差 1 的——从环面往上、那些更复杂的可定向曲面，两边都自然合拢、立刻定死（Ringel–Youngs 1968 一网打尽）。但跨到不可定向曲面，还藏着一个"差-1 的孪生"：克莱因瓶。它的构造下界是 6（$K_6$ 嵌得下、$K_7$ 嵌不下）、欧拉公式给的容易上界是 7，真值却是 6——这要到 Franklin 1934 才解决。所以"容易上界够不到真值"的差-1 现象，整个曲面拓扑里其实只有两处：球面（真值 4、不是 5）和克莱因瓶（真值 6、不是 7）；四色定理是其中之一，也是唯一难到非靠机器不可的那个。（这里要点破一处：这两处"差-1"是同一种现象——容易够到的上界都比真值高 1——但来源并不全一样。球面那个"易上界 5"是五色定理这条已经证出来的真命题，差的是"把真命题再压紧 1"（5 → 4）；克莱因瓶那个"易上界 7"则是 Heawood 公式给出的界，而克莱因瓶恰是 Heawood 公式唯一不达真值的曲面——这正是 Franklin 1934 那个例子出名的原因。机制不同，但都落在"易上界比真值高 1"这同一条上。）所以"四是平面与球面独有，恰恰是它难证的根源"——不是四色简单，而是它卡在那条最难焊的缝上。（注意：这里并不是在用反证法证四色定理；我们只证了"$K_5$ 画不出""平面总有度 ≤ 5 的点"这些扎实的小结论，而把上界 5 压到 4 的那一步，要等 §5 才真正完成。）

关于现实地图的一个注脚：真实世界的地图其实用不上四色定理，因为有"飞地"——一块国土飞在别国境内、按规矩必须与本土同色——这种地图不满足定理前提。但定理本身没错。

§2 从地图到点线图

数学家研究地图，第一步是把它抽象成平面图：每个区域缩成一个顶点，两区相邻就在两顶点间连一条边。国家的形状、大小全不重要了，剩下的只有一件事——谁挨着谁。于是"地图四染色"变成了"平面图的顶点四染色"。

这一步之后，Kempe 引入了他最妙的工具——"链"。（详见 §3。）

历史线索：Guthrie 1852 → De Morgan → 沉寂二十五年 → Cayley 1878 在伦敦数学会重提、1879 正式发表 → 同年 Kempe 的"证明"登场。（有意思的是，Cayley 和 Kempe 都当过多年执业律师才转向数学。）

§3 Kempe 链与五色定理

§2 把"地图四染色"翻译成了"平面图的顶点四染色"。Kempe 1879 真正留下来的、经得起检验的成果，并不是四色，而是用同一套"链"的思想稳稳证到的五色。

承接 §1 那条"下界 vs 上界"的主线：平面地图的下界是 4（$K_4$ 逼出来的，§1），而本节要证的五色定理，正是那个"轻松够得到"的上界 5。从 5 往下压到 4 的那道缝——也就是整部四色定理——则要等到 §4（看两条"用一支笔"的路如何先后失败）和 §5（机器证明把它焊死）。这一节先把上界 5 这台引擎拆开看清楚：它的核心零件，就是"平面图必有度 $\le 5$ 的顶点"这一步（推论 3.3）——度 $\le 5$，于是五色够用。它既是后面理解 Kempe 为何在"四色"上栽跟头的钥匙，本身也是一个干净漂亮的平面性论证。

先把几个词说清楚

证明里反复出现四个词，先用图认一下，后面就不卡壳了：

再约定几个记号：$V,E,F$ 分别是图的顶点数、边数、面数（$F$ 把外面那块无界区域也算一个面）；$\deg(v)$ 是顶点 $v$ 的度，即从它伸出的边数；$G-v$ 指把顶点 $v$ 连同它的边一并删掉后剩下的图。

以下"平面图"均指简单连通平面图（无重边、无自环），并设 $V \ge 3$。

平面图为什么总有"低度"顶点

整套染色论证有一个抓手：无论地图多复杂，平面图里一定有一个"邻居不超过五个"的区域。这件事完全由欧拉公式逼出来。

引理 3.1（欧拉公式）. 连通平面图满足 $$V - E + F = 2. \tag{3.1}$$

这条式子怎么来的？用一个"边数归纳"，每一步都能画出来：

证明. 对边数 $E$ 归纳。若 $G$ 无圈，则 $G$ 是树，$E = V-1$，且只有外部一个面 $F=1$，此时 $V-(V-1)+1 = 2$。若 $G$ 含圈，取圈上一条边 $e$；$G-e$ 仍连通，而 $e$ 原本分隔的两个面在删去后合并为一，故 $V' = V,\ E' = E-1,\ F' = F-1$。由归纳假设 $V'-E'+F'=2$，代回即得 $V-E+F = 2$。(证毕)

引理 3.2（边数上界）. $V \ge 3$ 的简单平面图满足 $$E \le 3V - 6. \tag{3.2}$$

证明. 向 $G$ 添加边只增大 $E$、不破坏平面性与简单性，故只需对极大平面图（再添任一条边即破坏平面性者）证 $E = 3V-6$，一般图作为其子图自然满足 $E \le 3V-6$。极大平面图的每个面都是三角形（否则面内还能添一条对角线），于是按"每面 3 条边界边、每条边恰分隔 2 个面"计数得 $3F = 2E$。以 $F = \tfrac23 E$ 代入 $(3.1)$：$V - E + \tfrac23 E = 2$，重排即得 $E = 3V-6$。(证毕)

推论 3.3（必存低度顶点）. 任何简单平面图都有一个度 $\le 5$ 的顶点。

证明. 反设所有顶点的度 $\ge 6$。由握手定理（每条边连接它的两个端点、给两端各贡献 1 个度，所以把所有顶点的度加起来，每条边正好被数两次——即所有顶点的度之和恰是边数的两倍：$\sum_v \deg(v)=2E$）有 $2E = \sum_v \deg(v) \ge 6V$，即 $E \ge 3V$，与 $(3.2)$ 给出的 $E \le 3V-6 < 3V$ 矛盾。故必有度 $\le 5$ 的顶点。(证毕)

注 3.3.1. 推论 3.3 是整个染色论证的抓手：无论地图多么复杂，平面性都担保了一定存在一个"邻居不超过五个"的区域，让我们能从它入手、对其余部分用归纳。这一步对应视频里"欧拉公式 ⇒ 必有度 ≤ 5 的顶点"那一幕。

下面这段小代码在几个具体的平面图（正多面体的骨架）上核验引理 3.2 与推论 3.3——边数不超过 $3V-6$、且总存在度 $\le 5$ 的顶点：

import networkx as nx

def check(G):
    assert nx.check_planarity(G)[0]                       # 平面
    V, E = G.number_of_nodes(), G.number_of_edges()
    assert E <= 3 * V - 6                                  # 引理 3.2
    mindeg = min(d for _, d in G.degree())
    assert mindeg <= 5                                     # 推论 3.3
    return V, E, 3 * V - 6, mindeg

for name, G in [("octahedron", nx.octahedral_graph()),
                ("icosahedron", nx.icosahedral_graph()),
                ("dodecahedron", nx.dodecahedral_graph())]:
    V, E, bound, mindeg = check(G)
    print(f"{name:12s} V={V:2d} E={E:2d} <= 3V-6={bound:2d}   min-degree={mindeg} (<=5)")
# octahedron   V= 6 E=12 <= 3V-6=12   min-degree=4 (<=5)
# icosahedron  V=12 E=30 <= 3V-6=30   min-degree=5 (<=5)
# dodecahedron V=20 E=30 <= 3V-6=54   min-degree=3 (<=5)

Kempe 的"链"：一步步看它怎么腾出一种颜色

Kempe 最妙的工具，是只盯住两种颜色看。这套机制听着抽象，画出来其实很直白——下面这张图把它从零走一遍：

一句话：Kempe 链就是"某两种颜色撑起的一个连通块"；只要某条链够不到它本该够到的对家，在这条链上整体换色就能凭空腾出一种颜色。这正是下面五色证明的全部火力来源。

定义 3.4（Kempe 链）. 设平面图 $G$ 已有一个合法染色。固定两种颜色 $i, j$，只保留颜色为 $i$ 或 $j$ 的顶点及它们之间的边，得到导出子图 $G_{ij}$。$G_{ij}$ 的每一个连通分量，称为一条 $(i,j)$-Kempe 链。

引理 3.5（对换不破坏合法性）. 在某一条 $(i,j)$-链 $C$ 上，把所有颜色 $i$ 与 $j$ 互换（链外的顶点保持不动），所得仍是合法染色。

证明. 任取一条边 $uw$，只需验证对换后两端异色。若 $u,w$ 都不在 $C$ 上，二者颜色未变，本来异色，仍异色。若 $u,w$ 都在 $C$ 上，对换只是把 $\{i,j\}$ 两色在 $C$ 内互调，相邻两端依旧取 $\{i,j\}$ 中相异的两色。若恰有一端在 $C$ 内、另一端 $w$ 在 $C$ 外：$w$ 的颜色必不属于 $\{i,j\}$——否则 $w$ 是 $i,j$ 色顶点又与 $u$ 相邻，将落入同一连通分量 $C$，矛盾；于是 $u$ 对换后（仍为 $i$ 或 $j$）与颜色不在 $\{i,j\}$ 中的 $w$ 仍然异色。综上所有边两端异色，染色合法。(证毕)

五色定理

定理 3.6（五色定理，Heawood 1890）. 每个平面图都可用至多五种颜色合法染色。

证明. 反设不成立，取一个最小反例 $G$：顶点数最少的、无法 5-染色的平面图。由推论 3.3，$G$ 有顶点 $v$，$\deg(v) \le 5$。

由 $G$ 的最小性，$G - v$ 可 5-染色；固定它的一个合法 5-染色，下面设法把 $v$ 也染上。

若 $v$ 的邻居（至多 5 个）实际只用到 $\le 4$ 种颜色，则五色中尚有空色可直接给 $v$，得 $G$ 的合法 5-染色，与"$G$ 是反例"矛盾。故必有 $\deg(v) = 5$，且五个邻居恰好用满五色。依平面嵌入把它们绕 $v$ 顺时针记为 $v_1, \dots, v_5$，并设 $v_k$ 的颜色为 $k$。

考察从 $v_1$ 出发的 $(1,3)$-链 $C_{13}$。

情形 (i)：$v_3 \notin C_{13}$。 在 $C_{13}$ 上对换 $1 \leftrightarrow 3$（引理 3.5 保证仍合法）。$v_1$ 变为颜色 3，而 $v_3$ 不在该链上、保持颜色 3。此时 $v$ 的邻居里再没有颜色 1，颜色 1 空出，给 $v$ 即可。矛盾。

情形 (ii)：$v_3 \in C_{13}$。 那么 $C_{13}$ 中有一条从 $v_1$ 到 $v_3$、顶点颜色全在 $\{1,3\}$ 中的路径 $P$。把 $P$ 连同顶点 $v$（经 $v v_1$、$v v_3$ 两条边）首尾接起来，就在平面上围出一条闭曲线 $\gamma$。由 Jordan 曲线定理，$\gamma$ 把平面分成内、外两个区域；而 $v_2$ 与 $v_4$ 在 $v$ 周围正好分处 $v_1, v_3$ 的两侧，故它俩被 $\gamma$ 隔在不同区域。

再看从 $v_2$ 出发的 $(2,4)$-链 $C_{24}$：它的顶点颜色全是 2 或 4，而 $\gamma$ 完全由颜色 1、3 的顶点（加上 $v$）构成——两组颜色不相交。一条全为 $\{2,4\}$ 色的路径若想从 $\gamma$ 内部通到外部，就必须"穿过"$\gamma$；但穿过只能落在 $\gamma$ 的顶点上、或与 $\gamma$ 的边相交，前者不可能（$\gamma$ 上没有 2、4 色顶点），后者被平面性禁止（平面图的边互不交叉）。故 $C_{24}$ 不可能同时含 $v_2$ 与 $v_4$，即 $v_4 \notin C_{24}$。于是在 $C_{24}$ 上对换 $2 \leftrightarrow 4$，$v_2$ 变为颜色 4，颜色 2 空出，给 $v$。矛盾。

两种情形都导致矛盾，最小反例不存在。定理得证。(证毕)

注 3.6.1（平面性是这条证明的命门）. 整个论证的全部重量，都压在情形 (ii) 的一句话上：$(1,3)$-链一旦真的连通了 $v_1$ 与 $v_3$，它在平面上就围出一条 Jordan 闭曲线，把 $v_2$、$v_4$ 强行隔在两侧，于是 $(2,4)$-链再也不可能同时够到它俩——我们因此总能腾出一种颜色。这里"平面性"做了两件不可替代的事：其一，Jordan 曲线定理保证平面上的闭曲线必把平面分成内外两块；其二，平面图的边不交叉，保证异色链无法"绕过"$\gamma$。把同一张图画到环面（甜甜圈面）上，两条性质同时失效——环面上的闭曲线未必分隔曲面，$(2,4)$-链就能从"洞"里绕过去同时连通 $v_2, v_4$，论证当场崩塌。这也正是为什么"四种颜色"在平面与球面上特殊、在环面上要七种（§1）。视频 B19 把这条链对换逐帧演了一遍。

注 3.6.2（为什么恰好到五色为止）. 这条证明之所以干净，是因为当五个邻居用满五色时，"给 $v$ 腾一个颜色"只需要一次成功的链对换，而 Jordan 隔离恰好担保那一次必然成功。可一旦降到四色：邻居用满四色时要腾色，就得让两条链同时让路，而平面性只能隔断"其中一条"，管不住两条之间的相互作用。Kempe 1879 正是没看穿这一点，才误以为同样的把戏能证到四色。下一节给出 Heawood 的精确反击。

把证明走在一张具体的图上

抽象论证看一遍未必有感觉，我们就照定理 3.6 的步骤，在一张能跟着画的小图上把"找顶点 → 删 → 染 → 链对换腾色"走一遍。

例 3.8. 取这样一张平面图（8 个顶点）：中心 $v$，外面一圈五边形 $n_0 n_1 n_2 n_3 n_4$ 与 $v$ 连成轮（$v$ 度为 5），再从 $n_0$ 拖出一条小尾巴 $n_0\text{–}p\text{–}q$。给 $G-v$ 染色：

$$n_0{=}1,\; n_1{=}2,\; n_2{=}3,\; n_3{=}4,\; n_4{=}5,\quad p{=}3,\; q{=}1.$$ 这是合法的，且 $v$ 的五个邻居 $n_0,\dots,n_4$ 恰好用满五色——$v$ 一时无色可填。看从 $n_0$（色 1）出发的 $(1,3)$-链：它顺着 $n_0\to p\to q$（色 $1,3,1$）走，到 $q$ 就走到头了，够不到 $n_2$（同为色 3，却不在这条链上）——正是定理 3.6 的情形 (i)。于是在链 $\{n_0,p,q\}$ 上对换 $1\leftrightarrow 3$，得 $n_0{=}3,\,p{=}1,\,q{=}3$；此刻 $v$ 的五个邻居只用了 $\{2,3,4,5\}$，色 1 空出，令 $v{=}1$。整张图合法 5-染色完成。

下面这段 networkx 代码可直接运行，把上面每一步都复算并校验（图是平面的、每步染色合法、$(1,3)$-链确实够不到 $n_2$、最终染色在全部 12 条边上合法）：

import networkx as nx

# 5-轮 (中心 v + 五边形 n0..n4) + 尾巴 n0-p-q
N = ["n0", "n1", "n2", "n3", "n4"]
G = nx.Graph(
    [("v", n) for n in N]                          # 辐条
    + [(N[i], N[(i + 1) % 5]) for i in range(5)]   # 五边形 C5
    + [("n0", "p"), ("p", "q")]                    # (1,3)-链的尾巴
)
assert nx.check_planarity(G)[0] and G.degree("v") == 5   # 平面、v 度为 5

# G - v 的合法 5-染色；v 的五个邻居用满五色
C = {"n0": 1, "n1": 2, "n2": 3, "n3": 4, "n4": 5, "p": 3, "q": 1}
proper = lambda col, skip=(): all(
    col[a] != col[b] for a, b in G.edges()
    if a not in skip and b not in skip and a in col and b in col)
assert proper(C, skip=("v",))
assert {C[n] for n in N} == {1, 2, 3, 4, 5}              # 邻居用满五色 -> v 卡住

# 从 n0 出发的 (1,3)-Kempe 链 (并查/广搜)
def chain(col, start, i, j):
    seen, stack = {start}, [start]
    while stack:
        x = stack.pop()
        for y in G[x]:
            if y in col and col[y] in (i, j) and y not in seen:
                seen.add(y); stack.append(y)
    return seen

ch = chain(C, "n0", 1, 3)
assert ch == {"n0", "p", "q"} and "n2" not in ch          # 情形 (i): 够不到 n2

# 在链上对换 1<->3, 腾出颜色 1, 染 v
for x in ch:
    C[x] = 3 if C[x] == 1 else (1 if C[x] == 3 else C[x])
assert {C[n] for n in N} == {2, 3, 4, 5}                   # 色 1 已空出
C["v"] = 1
assert proper(C)                                           # 全图 12 条边均合法
print("五色完成:", C)
# -> 五色完成: {'n0': 3, 'n1': 2, 'n2': 3, 'n3': 4, 'n4': 5, 'p': 1, 'q': 3, 'v': 1}

注 3.8.1. 这里落到的是情形 (i)（一次对换即腾出颜色）。情形 (ii)——$(1,3)$-链真把 $v_1,v_3$ 连通——要靠注 3.6.1 的 Jordan 隔离来断 $(2,4)$-链，构造稍大，但腾色的逻辑一致：平面性担保总有一条链可断。

§4 为什么 Kempe 的"四色"会塌

Kempe 1879 的野心不止五色——他想用同一套链法直接证到四色，并且当时所有人都相信他做到了。整整十一年后，Percy Heawood 才指出问题出在哪。这一节把那处错误讲清楚：它不是笔误，而是"链法"在四色这一步上一个本质的漏洞。同一时期 Tait 从另一条路（边染色）出发，也撞在同一堵墙上——我们把两条路一起讲完。

Kempe 的四色论证，与它要命的一步

照搬 §3 的框架：取最小反例，找到度 $\le 5$ 的顶点 $v$，把 $G-v$ 先 4-染色。若 $v$ 的邻居用到的颜色 $\le 3$ 种，直接补；真正的难关是 $\deg(v)=5$、五个邻居却只能用四种颜色——必有一种颜色在邻居里出现两次。

仿照五色的做法，Kempe 想靠链对换腾出一种颜色。但四色下最坏的情形里，一次对换不够：要让中心顶点 $v$ 空出颜色，得同时翻动两条 Kempe 链（比如一条红绿链、一条红黄链）。Kempe 默认这两条链各自为政、互不影响——

这一步就是错的。

命题 4.1（Heawood 1890 的漏洞）. 把两条 Kempe 链同时对换，可能产生一个不合法的染色：即便两条链顶点不相交，也可能有一个绿色顶点与一个黄色顶点恰好相邻；红绿对换把前者变红、红黄对换把后者变红，于是出现两个相邻的红色顶点。

说明（失效机理）. 设中心顶点 $v$（度 5）的五个邻居用满四色（$1$=红、$2$=黄、$3$=绿、$4$=蓝）。Kempe 为腾出红色，需对一条 $(1,3)$-红绿链 $A$ 与一条 $(1,2)$-红黄链 $B$ 各做一次对换。两链作为顶点集合可以不相交，Kempe 据此以为互不干扰；但"不相交"不等于"不相邻"——链 $A$ 上的某个绿点 $g$ 与链 $B$ 上的某个黄点 $y$ 之间完全可能有一条边。对换 $A$（红 $\leftrightarrow$ 绿）把 $g$ 染成红；对换 $B$（红 $\leftrightarrow$ 黄）把 $y$ 染成红；$g, y$ 相邻却同为红色——染色不再合法。Kempe 的"修补"反而制造了新的冲突。$\blacksquare$

注 4.1.1. 对照 §3.6.1：五色证明里只动一条链，Jordan 隔离保证它被干净地隔断；四色要动两条，而平面性只隔得断其中一条，管不住第二条与第一条产生的新相邻关系。漏洞的根，正是注 3.6.2 预告的那一处。视频 B20 把这两条链的对换与最后"绿黄双双变红"的冲突点逐帧定格。

Errera 图：让整套方法当场缠死的反例

命题 4.1 说明"链法可能出错"，但还不够狠——也许换个下手顺序就绕过去了？Errera 图（Alfred Errera 1921，17 个顶点、45 条边的平面图）堵死了这条退路：在它上面，无论怎么按 Kempe 的链法去涂，都会缠死。

我们用 networkx 一手核了 Errera 图的下述事实（邻接表、染色、对换序列均可复算）：

例 4.2（Errera 缠死序列）. 取 Errera 图，记某个度 5 顶点为 $v$。先给 $G-v$ 一个合法 4-染色，使 $v$ 的五个邻居恰好用满四色（红、绿、黄、蓝），于是 $v$ 无色可填。此时：

• 任何单独一次合法的 Kempe 链对换，都无法让 $v$ 的邻居腾出一种颜色（networkx 穷举所有邻居 $\times$ 所有候选颜色的单次对换，无一奏效）；
• 被逼做两次对换时，存在一条红黄链 $A=\{1,15\}$ 与一条红蓝链 $B=\{7\}$，二者顶点不相交，但顶点 $7$ 与顶点 $15$ 之间有边；对换 $A$ 后 $15$ 变红、对换 $B$ 后 $7$ 变红，边 $7\text{–}15$ 两端同为红色——正是命题 4.1 的冲突，在一张具体的图上被精确实现。

这不是某一种涂法的偶然失手，而是 Kempe 的链算法在 Errera 图上的结构性死结：每条出路都通向同一种矛盾。Errera 图因此成了"链法证不动四色"的标准反例。

下面这段 networkx 代码可直接运行，复算例 4.2 的全部论断——Errera 图的邻接、$v=0$ 的五个邻居用满四色、任何单次合法 Kempe 对换都腾不出颜色、以及被逼做两次对换时 $7$ 与 $15$ 双双变红：

import networkx as nx

# Errera 图 (17 顶点 45 边, 平面); 颜色 0=红 1=绿 2=黄 3=蓝
EDGES = [(0,1),(0,7),(0,14),(0,15),(0,16),(1,2),(1,9),(1,14),(1,15),(2,3),(2,8),(2,9),
         (2,10),(2,14),(3,4),(3,9),(3,10),(3,11),(4,5),(4,10),(4,11),(4,12),(5,6),(5,11),
         (5,12),(5,13),(6,7),(6,8),(6,12),(6,13),(6,16),(7,13),(7,15),(7,16),(8,10),(8,12),
         (8,14),(8,16),(9,11),(9,13),(9,15),(10,12),(11,13),(13,15),(14,16)]
G = nx.Graph(EDGES)
assert G.number_of_nodes()==17 and G.number_of_edges()==45 and nx.check_planarity(G)[0]

V = 0; NB = [1,7,14,15,16]                           # 中心度5顶点及其 5 个邻居
C = {1:0,2:1,3:0,4:1,5:0,6:2,7:3,8:0,9:3,10:2,11:2,12:3,13:1,14:3,15:2,16:1}  # G-0 的合法 4 染色
assert all(C[a]!=C[b] for a,b in G.edges() if V not in (a,b))    # G-0 合法
assert {C[n] for n in NB}=={0,1,2,3}                 # 5 邻居用满 4 色 -> 0 无色可填

def comp(col, s, i, j):                               # s 所在的 (i,j)-Kempe 链
    seen, st = {s}, [s]
    while st:
        x = st.pop()
        for y in G[x]:
            if col.get(y) in (i,j) and y not in seen: seen.add(y); st.append(y)
    return seen

def frees(col):                                       # 是否存在“单次合法对换”能在 0 处腾出颜色
    for n in NB:
        for o in range(4):
            if o==col[n]: continue
            ch = comp(col, n, col[n], o)
            sw = {**col, **{x:(o if col[x]==col[n] else col[n] if col[x]==o else col[x]) for x in ch}}
            if all(sw[a]!=sw[b] for a,b in G.edges() if V not in (a,b)) and {sw[m] for m in NB}!={0,1,2,3}:
                return True
    return False
assert not frees(C)                                   # False = 任何单换都救不了 (Errera 现象)

A = comp(C,1,0,2); B = comp(C,7,0,3)                  # 被逼的两次对换: 红黄链 + 红蓝链
assert A=={1,15} and B=={7} and not (A&B) and G.has_edge(7,15)   # 不相交, 但 7-15 相邻
s = dict(C)
for x in A: s[x] = 2 if s[x]==0 else (0 if s[x]==2 else s[x])    # 换 红<->黄
for x in B: s[x] = 3 if s[x]==0 else (0 if s[x]==3 else s[x])    # 换 红<->蓝
assert s[7]==0 and s[15]==0                           # 7、15 双双变红, 边 7-15 红红 -> 非法
print("Errera 缠死: 单换全失效; 双换令 7,15 同为红 -> 矛盾")

另一条路也倒了：Tait 的边染色

几乎同时，物理学家兼数学家 Peter Guthrie Tait 1880 给出了第二条看上去更可行的路。他没有去碰顶点的面染色，而是把问题搬到了边上，并证明了一个非常漂亮的等价。

先要把舞台限定清楚：考虑三正则平面地图——每个顶点恰好伸出 3 条边（地图里三国交界的那种点），且图是无桥的（去掉任一条边仍连通）。

定理 4.3（Tait 1880 的等价）. 一张无桥的三正则平面图能用 4 种颜色合法地面染色，当且仅当它的边能用 3 种颜色染好（每个顶点伸出的 3 条边颜色互不相同）。

这个等价本身是完全正确的，而且构造干净得出乎意料。诀窍是把四种颜色不看成四个名字，而看成 Klein 四元群 $\mathbb{Z}_2\times\mathbb{Z}_2=\{00,01,10,11\}$ 的四个元素（记作 $0,1,2,3$，加法是逐位异或 XOR）。给定一个合法的 4-面染色，令每条边的颜色 = 它两侧两个面的颜色做 XOR：

为什么 XOR 出来的边染色一定合法？绕任一顶点转一圈会遇到 3 个面，它们两两异色——即 Klein 群里三个两两不同的元素（可能含单位元 $0$）；而任取三个两两不同的群元素，它们的两两 XOR 恰好是三个不同的非零元。于是这个顶点的 3 条边正好取齐 3 种颜色，互不相同。下面这段代码在 $K_4$ 上把整套对应复算一遍：

import networkx as nx
# K4 = 最小的无桥三正则平面图; 其平面嵌入有 4 个面
# 面用 Klein 四元群标号 0..3; 外部无界面取单位元 0
face = {"OUT": 0, "ABD": 1, "ACD": 2, "BCD": 3}
edge_faces = {("A","B"): ("OUT","ABD"), ("A","C"): ("OUT","ACD"), ("B","C"): ("OUT","BCD"),
              ("A","D"): ("ABD","ACD"), ("B","D"): ("ABD","BCD"), ("C","D"): ("ACD","BCD")}
edge_col = {e: face[f] ^ face[g] for e,(f,g) in edge_faces.items()}   # 边色 = 两侧面 XOR
assert all(c in (1,2,3) for c in edge_col.values())                  # 非零 -> 恰 3 种边色
for v in "ABCD":                                                     # 每个顶点 3 边取齐 3 色
    assert sorted(edge_col[e] for e in edge_col if v in e) == [1,2,3]
print("4-面染色 --XOR--> 3-边染色:", edge_col)
# -> {('A','B'):1, ('A','C'):2, ('B','C'):3, ('A','D'):3, ('B','D'):2, ('C','D'):1}

问题出在 Tait 接下来的一步。他注意到：只要一张三正则平面图含一条哈密顿圈（一条经过每个顶点恰好一次的闭圈），3-边染色立刻就有——

但"每张三正则（3-连通）平面图都含哈密顿圈"这个假设，是错的——这就是著名的 Tait 猜想。1946 年，W. T. Tutte 给出一张 3-连通、三正则、平面、却不含哈密顿圈的图（46 个顶点），直接推翻了它。注意分寸：Tutte 反例否定的是 Tait 那个哈密顿性假设，并非定理 4.3 那条"四面染色 $\Leftrightarrow$ 三边染色"的等价——等价至今成立，只是它没能像 Tait 期望的那样、靠"总有哈密顿圈"轻易兑现成四色证明。

import networkx as nx
T = nx.tutte_graph()
assert T.number_of_nodes() == 46
assert all(d == 3 for _, d in T.degree())     # 三正则 (cubic)
assert nx.check_planarity(T)[0]               # 平面
assert nx.node_connectivity(T) == 3           # 3-连通
# 不含哈密顿圈是 Tutte 1946 的定理; 46 顶点上暴力枚举哈密顿圈不现实, 此处不重算
print("Tutte 图: 46 顶点, 三正则, 平面, 3-连通 —— Tait 猜想的反例")

两条"用一支笔证出来"的路先后倒下——Kempe 的链、Tait 的边染色——一个念头开始在数学界浮现：也许四色定理，靠人手根本证不动。

§5 机器证明：不可避免集、可约性、放电法

如果不能靠一个精巧的论证一锤定音，那还剩一条笨办法：把"最小反例必然包含的局部图案"全部列出来，再逐一证明每个图案都不可能出现在最小反例里——两头一夹，最小反例无处容身。这正是 Appel–Haken 1976 的框架，也是第一个本质上离不开计算机的重大定理。

可约构型

定义 5.1（构型 / 可约）. 一个构型 (configuration) 是平面图里一小块带边界环 (ring) 的局部子图——可以想成"从地图里挖出来的一块带边框的拼图"。称它可约 (reducible)，是指：若某个最小反例包含这个构型，就能由它导出矛盾——具体到 D-可约（Birkhoff 的判据），是指环上每一种合法 4-染色，都能（必要时配合环外的 Kempe 链对换）延拓成整个"构型 + 内部"的合法 4-染色。

把这两个词画出来就一目了然：

直观地说：可约构型是"啃得动的硬骨头"——一旦最小反例里出现它，就能把它的染色补全，与"最小反例不可染"矛盾。

例 5.2（Birkhoff diamond，最早的 D-可约构型）. Birkhoff 1913 的"钻石"构型：一个 6 顶点的环，里面嵌 4 个内部顶点。环作为一个 6-圈 $C_6$，其合法 4-染色的总数由色多项式给出 $$P(C_6, 4) = (4-1)^6 + (4-1) = 3^6 + 3 = 732. \tag{5.1}$$ 这 732 种环染色中，384 种能直接延拓进内部；其余 348 种在配合 Kempe 链对换后也能延拓；$384 + 348 = 732$——全部 732 种都能延拓，故 Birkhoff diamond 是 D-可约的。

注 5.2.1（这组数字的来历）. 这里的 732、384、348 都是可复现的计算结果，下方代码直接跑得出。尤其要点出：384/348 这个拆分与任何 Kempe 模型无关——它只问一件事："一个环染色能不能不借助 Kempe、直接填进 4 个内部顶点（穷举 $4^4$ 种内部染色）"。正因如此，无论用哪种合法的 labeling 去搭 Birkhoff diamond，跑出来的都是 384/348（这一点经三套独立构造 + 旋转/反射不变性核过）。需要分清："D-可约"这个概念是 Birkhoff 1913 的经典贡献；而 "384/348" 这组具体数字是今天用计算机一跑即得的结论，并非 Birkhoff 原文逐字印出的数。还要老实说明：下方代码里的 Kempe 闭包是一个可复现的演示模型——它如实复现"384 直接 + 348 经闭包全 recover"的计数，但并非完整严格的 Heesch D-可约判据（后者对"哪些链互换能在平面外部同时实现"另有非交叉约束）。对本来就 D-可约的 Birkhoff 菱形，这个演示模型给出的结论与严格判据一致；严格判据本身见 Birkhoff 1913 与 Heesch 的可约性算法。

下面这段 networkx 代码可直接运行，复现全部计数（Birkhoff diamond 的 canonical 邻接经独立三方核定）：

import itertools, networkx as nx

# Birkhoff diamond: 6-环 0..5 + 4 内点 6,7,8,9; 内部菱形 = K4 去掉边 7-9 (留对角线 6-8)
RING   = [(0,1),(1,2),(2,3),(3,4),(4,5),(5,0)]
INNER  = [(6,7),(7,8),(8,9),(9,6),(6,8)]
SPOKES = [(6,5),(6,0),(7,0),(7,1),(7,2),(8,2),(8,3),(9,3),(9,4),(9,5)]   # 内点 -> 环
G = nx.Graph(RING+INNER+SPOKES)
assert G.number_of_nodes()==10 and G.number_of_edges()==21        # 10 顶点 21 边
assert sorted(d for n,d in G.degree() if n in (6,7,8,9))==[5,5,5,5]  # 内点全度 5
assert nx.check_planarity(G)[0]                                    # 平面

CONSTR = INNER + SPOKES                                            # 牵涉内部的边
RING_COLS = [c for c in itertools.product(range(4),repeat=6)
             if all(c[a]!=c[b] for a,b in RING)]
assert len(RING_COLS) == 732                                       # P(C6,4)=3^6+3

def direct(rc):                       # 环染色能否“不用 Kempe、直接”填进 4 内点 (穷举 4^4)
    base = {i: rc[i] for i in range(6)}
    return any(all({**base,6:a,7:b,8:c,9:d}[x] != {**base,6:a,7:b,8:c,9:d}[y]
                   for x,y in CONSTR) for a,b,c,d in itertools.product(range(4),repeat=4))

# 注: 下面的 Kempe 闭包是 D-可约的可复现 *演示* 模型; 它忠实复现"384 直接 + 348 经闭包"
#     的计数, 但不是完整严格的 Heesch D-reducibility 判据(后者对"哪些互换能在平面外部
#     同时实现"另有非交叉约束)。严格判据见 Birkhoff 1913 / Heesch 的 D-reducibility 算法。
def kempe_moves(rc):                  # 外区 i-j Kempe 链 = 换 {i,j} 色环点的一段连续块
    moves = []
    for i,j in itertools.combinations(range(4),2):
        pos = [k for k in range(6) if rc[k] in (i,j)]
        for s in range(len(pos)):
            for L in range(1, len(pos)):
                blk = {pos[(s+t)%len(pos)] for t in range(L)}
                new = [(j if rc[k]==i else i) if k in blk else rc[k] for k in range(6)]
                if all(new[a]!=new[b] for a,b in RING):
                    moves.append(tuple(new))
    return moves

direct_set = {rc for rc in RING_COLS if direct(rc)}
def d_good(rc):                       # rc 经 Kempe 闭包能否到达某个可直接延拓的染色
    seen, st = {rc}, [rc]
    while st:
        x = st.pop()
        if x in direct_set: return True
        for y in kempe_moves(x):
            if y not in seen: seen.add(y); st.append(y)
    return False

D = len(direct_set)
recovered = sum(d_good(rc) for rc in RING_COLS if rc not in direct_set)
print(D, recovered, D + recovered)        # -> 384 348 732  (全 732 D-可约)

不可避免集与放电法

光有"一些可约构型"不够——还得证明它们构成一个不可避免集：任何平面图（从而任何最小反例）都至少含其中之一。这一步靠放电法（discharging）完成。

命题 5.3（电荷总量为正）. 在一个三角剖分的平面图里，给每个顶点 $v$ 赋"电荷" $6 - \deg(v)$，则总电荷恒为 $+12$： $$\sum_{v} \bigl(6 - \deg(v)\bigr) = 6V - 2E = 6V - 2(3V - 6) = 12. \tag{5.2}$$

证明. 由握手定理 $\sum_v \deg(v) = 2E$，且三角剖分取 $(3.2)$ 的等号 $E = 3V-6$，代入即得 $6V - 2E = 6V - (6V-12) = 12$。(证毕)

总电荷 $+12 > 0$ 意味着必有正电荷顶点，即度 $\le 5$ 的顶点（度 $\ge 6$ 者电荷 $\le 0$）。放电法的精髓在于：按一组固定规则把电荷从某些顶点搬到邻居（搬移不改变总量，仍是 $+12$）。规则设计得当时，搬完之后仍带正电的顶点，其周围的局部结构必定落入预先列好的构型集中——于是"度 $\le 5$ 的顶点附近长什么样"被穷尽分类，构型集不可避免得证。

把"不可避免"与"每个构型都可约"合起来：最小反例必含某构型（不可避免），而该构型可约（导出矛盾）。最小反例不存在，四色定理成立。

1976、以及之后的修补

这个框架的两半——列出不可避免集、逐一验证可约——的规模都远超人手：

• Appel–Haken 1976：不可避免集约 1476 个构型（初始约 1834、逐步缩到约 1476），可约性验证耗去约 1200 小时机时。这是历史上第一个本质依赖计算机的重大定理：没有任何人能把那一千多个构型一个个手验完。
• Schmidt 1981：德国学生 Ulrich Schmidt 检查了证明里约四成（这个比例据 Robin Wilson《四色足矣》一书记载）的"不可避免性"部分，发现放电过程中有一处实质性错误。注意分寸：四成是他检查到的范围，不是"四成都错"；错误是一处，不是一片。这处错误（连同后来别人发现的若干处）在 1989 年 Appel–Haken 的书里全部补好。证明是对的，但它的过程并非无懈可击。
• Robertson–Sanders–Seymour–Thomas 1996（论文 1997 年发表）：一个干净得多的新证明，把构型从上千压到 633 个、放电规则从 Appel–Haken 的 487 条减到 32 条。这平息了"它到底对不对"的疑虑——但仍剩一个结：你还得相信那些跑可约性检查的程序本身没写错。
• Gonthier 2005：用证明助手 Coq 把整个证明——不只是结果，而是每一步逻辑——交给机器做了完整的形式化核验。这把"信任一大堆专用程序"降级成了"信任 Coq 那个极小的、被反复审查过的内核"。当年那个引发"这还算证明吗"之争的计算机证明，自己变成了可信度的金标准。

注 5.4. 形式化验证（Coq、以及今天的 Lean）正是四色定理留给当代的遗产：一篇证明只要能翻译成这类语言、被机器逐步核过，对错就有了不依赖人眼通读的判据——错的过不了关。这条线索，正是下一节（§6）面对 AI 时代"看着可信却未必真对"的证明时，最硬的一道防线。

那么——能不能写个程序，把它整个证明出来？答案：能

读到这里，一个很自然的问题是：既然上面那段 Birkhoff 代码已经能"一跑就判出一个构型可不可约"，那把它放大，是不是就能让程序把整个四色定理证完？

是的。而且这正是四色定理最特别的地方——它的证明，本身就是一个程序。 拆开看，这个程序由两个可以分别运行、合起来即完证的部分组成：

1. 可约性 = 上面那段代码的放大版。 §5 的 Birkhoff demo 做的，就是"枚举环的全部合法染色，逐一判定能否延拓"。一个完整证明要做的，是把同一件事在 RSST 的 633 个构型上各跑一遍（每个构型的环更大、内部更复杂，但判定的逻辑同构）。这一步天然是计算机的活——但要分清两种规模：单个构型（像本文那段 Birkhoff demo）今天几秒到几分钟即可判完；而全部 633 个构型的 D-可约性、加上 32 条规则的不可避免性的完整复跑，则是一桩正经计算——1976 年 Appel–Haken 花了约 1200 机时，今天虽快得多，仍需可观的算力与时间（拿另一套独立程序重跑核对更是小时级往上），绝不是几分钟一键秒出。
2. 不可避免性 = 放电规则的程序化检查。 §5 的放电法（命题 5.3 + 图 5.5）需要证明"那 633 个构型构成一个不可避免集"。RSST 把它压成 32 条放电规则，并写成一个可以机器逐条核验的判定过程——也就是说，"这组构型谁都躲不开"这件事，同样是程序跑得出来的。

两半都是程序，合起来就是完整证明。所以"写程序证明四色定理"不是一个比喻，而是字面意义上、四色定理从 1976 起就一直在用的证明方式。

那要不要自己从零写一个上千构型的检查器？——不必，也不该。 现成的、可运行的完整实现早已公开、且被反复独立核对过。最实际的做法是分三层，按你想要的"确信程度"取用：

• 想先有手感（几分钟）：就跑本文 §5 那段 Birkhoff 可约性代码。它是整个证明在单个构型上的忠实切片——把"环染色枚举 + 延拓判定"这件核心动作完整演了一遍。
• 想跑真正的完整证明数据（633 构型 + 32 规则）：直接用 Robertson–Sanders–Seymour–Thomas 公开的程序与数据——四色定理官方页面上挂着 633 个构型的完整清单（unavoidable.pdf）、32 条放电规则的图示，以及当年用来做可约性检查与不可避免性验证的 C 程序和数据文件。Gašper Fijavž 在 Bojan Mohar 指导下还独立写了一套程序（见 RSST 官方页）。不要自己造轮子——你造出来的，无非是它的一个更糙的版本。
• 想要不留任何"程序会不会写错"余地的金标准：用 Georges Gonthier 的 Coq 完整形式化——coq-community/fourcolor。它把证明的每一步逻辑（不只是那些计算结果）都翻译成 Coq、交给证明助手的内核逐步核验通过。信任它，你只需要信任 Coq 那个极小、被全世界反复审查的内核，而不必再去信任任何一段专用的检查代码。

一句话收束这一节：四色定理把"证明"这件事推到了一个新位置——它的正确性，不再靠某个人读懂一篇论文来担保，而靠一段（任何人都能下载、重跑、甚至换语言重写的）程序来担保。这恰恰是下一节要讲的、AI 时代信任问题的正面参照：1976 年的计算机证明虽然"没人读得完"，却可以被任何人重新运行、独立核对；这条"可机器复核"的退路，正是今天我们面对黑箱 AI 论证时，最想要、却最稀缺的东西。

§6 同一个问题，更危险地重演：AI 时代的信任危机

本章底料 = Gauss 深度报告《从四色定理到 Leiden 宣言》（一手核）。以下为博客化改写，所有"活动数据"与未公开项带 caveat。

四色定理留下的问题不是历史，是正在放大重演的当下。

1976 的计算机 vs 2026 的 AI，有一个本质不同——这是整件事最要紧的一刀：

• 1976 的计算机做的是体力活：把人想好的一千多个构型一个个验过去，没提出任何新念头。它的毛病是"算得对，可没人看得完"（不可纵览）。面对这种毛病，答案是 Gonthier 式的机器形式化核验。
• 2026 的 AI 毛病正好反了过来：它能写出读着滴水不漏、却在某个似是而非处藏着错的论证——"看着对，其实未必真对"。而且它真的在创造新数学了。

真创造的活例（2026-05）：一个未公开型号的推理模型推翻了 Erdős 1946 年的单位距离猜想——用数论里的工具攻离散几何，造出谁都没想到的新构造。九位顶尖数学家专门写论文核验（arXiv:2605.20695）。菲尔兹奖得主 Tim Gowers 在配套论文里写下的评价（OpenAI 公告页全文转载，可点开逐字核）："There is no doubt that the solution to the unit-distance problem is a milestone in AI mathematics: if a human had written the paper and submitted it to the Annals of Mathematics, I would have recommended acceptance without any hesitation."（毫无疑问，单位距离问题的解决是人工智能数学的一座里程碑：如果是人写了这篇论文投给《数学年刊》，我会毫不犹豫地建议接收。）但它落地的方式恰好踩中所有人最担心的两点：漏引前人工作 + 方法全黑箱。

对照的反例（2025-10）：OpenAI 一位高管发帖说模型"解决了 10 个未解 Erdős 难题"，被数据库维护者 Thomas Bloom 拆穿是"严重的误传"——AI 只是从已有文献里检索出现成答案。"找到现成的"和"原创解出来的"，原来是一条连续的灰带。

集体回应（2026-06-02）：数学家签署 Leiden 宣言（国际数学联盟背书），列出数学的 5 个核心价值与 AI 带来的 5 个威胁：

诚实标注：① 签名数是实时计数器（发布即上百、一天内将近八百、仍在涨），别当定值。② OpenAI 模型型号未公开，非确认的 GPT-5.x。③ 四色↔AI 的平行是评论者 Gil Kalai 画的，不在 Leiden 宣言原文里——本文以它为论证主轴，但注明出处归属。④ Tao 不在宣言签署人之列。

两条出路：

1. 形式化验证——四色定理自己留下的那条路。一篇证明只要能翻成 Lean 这样的语言、被机器逐步核过，就一定对（错的过不了关）；DeepMind 的 AlphaProof 就是 Gonthier 路线的 AI 版。这里还有一处常被略过的前提：机器核验的是证明本身对不对，并不负责保证"被证的那条陈述正是你想要的那条"——若把定理的陈述翻译歪了，一个机器核过的有效证明仍可能误导。边界：形式化只覆盖已经写成形式语言的部分，且依赖陈述被忠实翻译。
2. 守住人的判断。菲尔兹奖得主 Peter Scholze（莱顿宣言签署人）："The goal of mathematical research is human understanding of mathematics, and so mathematics can only thrive in a community of human mathematicians."（数学研究的目标，是人对数学的理解；所以数学只能在一个由人组成的数学家共同体里繁荣。）

结语

1879 年那张被信了十一年的错证明，和 2026 年这些没人能完全担保的 AI 证明，问的其实是同一个问题。只不过现在，连证明本身，机器可能都替你写好了。

从 1976 到今天，难的从来都不是"算出来"。难的，是判断——到底什么才算"解决了"，以及，我们凭什么相信它。

参考来源

早期历史与人物 - 四色问题早期史（Guthrie 1852、De Morgan→Hamilton 1852-10-23 通信、Cayley 1878–79、Heawood 1890）—— MacTutor: The Four Colour Theorem - Alfred Kempe（1879 证明；1881 因连杆/运动学工作当选皇家学会会员）—— MacTutor: Kempe - Errera 图（Alfred Errera, 1921；17 顶点 45 边）—— Wikipedia: Errera graph - Tait 边染色等价与哈密顿假设（1880）—— Wikipedia: Tait's conjecture - Tutte 非哈密顿三正则平面图（1946；46 顶点）—— Wikipedia: Tutte graph

机器证明 - Birkhoff diamond / D-可约（G. D. Birkhoff, The Reducibility of Maps, Amer. J. Math. 35:115–128, 1913）—— archive.org 全文 - Appel–Haken 1976 + Schmidt 1981 检查 —— Wikipedia: Four color theorem - Robertson–Sanders–Seymour–Thomas 新证明（1996/1997；633 构型 / 32 放电规则；含可运行程序与数据）—— Robin Thomas: The Four Color Theorem - Gonthier 的 Coq 形式化（2005）—— coq-community/fourcolor · Formal Proof—The Four-Color Theorem, AMS Notices 2008 (PDF)

AI 时代（§6） - 单位距离猜想反证的人类核验论文（9 作者）—— arXiv:2605.20695 - Tim Gowers 评价（“milestone in AI mathematics…”）—— OpenAI 公告页 - GPT-5 “解 10 题”误传 + Thomas Bloom 澄清（2025-10）—— TechCrunch - 莱顿宣言（IMU 背书）—— leidendeclaration.ai · 签署名单 - Peter Scholze 背书引文 —— 莱顿宣言官网 - 四色↔AI 平行的出处（Gil Kalai）—— Combinatorics and More, 2026-05-21 - AlphaProof（IMO 2024 银牌级形式证明）—— DeepMind

（出处由 Gauss 史实轮逐条核实、curl-200 live，2026-06-04。）