在数学的历史中，最著名同时也是最具争议的定理之一就是“四色定理（Four Color Theorem）”。“任何平面地图，为了使相邻的区域颜色不同，只需要4种颜色就足够了”，这是一个连小学生都能理解的简单主张，然而它的证明却耗费了一个多世纪的岁月，并需要一种动摇数学这门学科根基的“计算机辅助证明”的范式转变。
本文将从1852年朴素的疑问开始，历经天才们的挑战与挫折，直至现代数学借助计算机这一新智慧所达到的高度，从数学、历史与哲学的视角，彻底揭开四色定理的全貌。特别是，我们将深入探讨肯普的伪证明与希伍德反例的几何结构、五色定理的完全证明、放电法的数理、阿佩尔和哈肯的算法、通过Coq的形式化证明细节，以及与NP完全性的关联等深奥的数学话题。
第一章：1852年，弗朗西斯·古德里的朴素疑问与向图论的升华
地图着色问题的提出
故事的开端追溯到1852年，刚刚从英国伦敦大学学院毕业的青年弗朗西斯·古德里（Francis Guthrie）。他在为英国各郡的地图着色时，注意到了一个奇妙的事实：“无论多么复杂的地图，为了让相邻的郡颜色不同，是不是只需要4种颜色就足够了？”
弗朗西斯将这个疑问告诉了当时在伦敦大学学院学习数学的弟弟弗雷德里克·古德里（Frederick Guthrie）。弗雷德里克向他的指导教授、当时代表性的数学家之一奥古斯塔斯·德·摩根（Augustus De Morgan）提出了这个问题。德·摩根立刻被这个问题的趣味性所吸引，并在给朋友威廉·卢云·哈密顿（William Rowan Hamilton）等人的信中分享了这个问题。这就是在数学史上熠熠生辉的“四色问题”诞生的瞬间。
欧拉多面体定理与平面图的对偶性
为了在数学上严密地处理地图着色问题，必须将其形式化为图论问题。将地图上的每个区域（国家或州）视为“顶点（Vertex）”，将相邻的区域用“边（Edge）”连接起来，就可以得到在平面上边不相交的“平面图（Planar Graph）”。这种转换被称为取“对偶图（Dual Graph）”的操作。原地图的边界线对应于图的边，面对应于顶点。
四色问题归结为图的顶点着色问题（Vertex Coloring Problem）：“是否能用4种颜色对任意平面图的顶点进行着色，使得相邻的顶点颜色不同？”
在这里发挥着极其重要作用的，是莱昂哈德·欧拉发现的多面体定理。在连通的平面图中，假设顶点数为 \(V\)，边数为 \(E\)，面数为 \(F\)，则存在以下不变的关系：
\[V - E + F = 2\]结合这一定理与平面图的基本性质，可以推导出关于平面图结构的强大约束。假设图是没有多重边和自环的简单图，并进一步考虑所有面都是三角形的“极大平面图（Maximal Planar Graph）”。因为对任意平面图添加边使其成为极大平面图并不会增加着色数，所以只需要证明极大平面图的四色定理就足够了。
在极大平面图中，每个面恰好被3条边包围。因为1条边恰好是2个面的边界，所以在面的数量与边的数量之间严格成立以下关系：
\[3F = 2E\]将其代入欧拉公式中消去 \(F\)。将 \(F = \frac{2}{3}E\) 代入 \(V - E + F = 2\)：
\[V - E + \frac{2}{3}E = 2 \implies V - \frac{1}{3}E = 2 \implies 3V - E = 6 \implies E = 3V - 6\]在一般的简单平面图中，由于面由3条以上的边包围，所以 \(3F \leq 2E\)，可以推导出以下不等式：
\[E \leq 3V - 6\]这个不等式表明平面图的边密度存在严格的上限。由此，我们来考虑每个顶点的度数（Degree, \(\deg(v)\)）。图中所有顶点的度数之和恰好是边数的2倍（握手引理）。
\[\sum_{v \in V} \deg(v) = 2E\]使用前面的不等式 \(2E \leq 6V - 12\)：
\[\sum_{v \in V} \deg(v) \leq 6V - 12\]两边除以顶点数 \(V\)，可得到顶点的平均度数：
\[\frac{1}{V} \sum_{v \in V} \deg(v) \leq 6 - \frac{12}{V} < 6\]平均度数严格小于6这一事实，在数学上完全证明了“至少有1个顶点，其度数必须小于等于5”。也就是说，在任意简单平面图中，至少存在一个度数为1、2、3、4或5的顶点。这一事实是后文所述“不可避免构形”概念最基础的出发点，也是四色定理证明的绝对核心。
第二章：阿尔弗雷德·肯普的“证明”与11年后的崩溃
肯普链的概念与华丽的“证明”
1879年，英国律师兼数学家阿尔弗雷德·布雷·肯普（Alfred Kempe）终于在《自然》（Nature）杂志及《美国数学杂志》（American Journal of Mathematics）上发表了四色问题的“证明”。他的证明极具独创性，并在其后的11年间被世界数学界公认为正确。
肯普证明的核心，是现在被称为“肯普链（Kempe Chain）”的划时代想法。他使用了数学归纳法。假设四色定理对顶点数为 \(k\) 的所有平面图都成立，他试图证明它对顶点数为 \(k+1\) 的图也成立。
根据前述的欧拉定理，顶点数为 \(k+1\) 的平面图 \(G\) 中一定存在度数小于等于5的顶点 \(v\)。考虑从图 \(G\) 中移除顶点 \(v\) 及其连接的边后的图 \(G'\)。由于 \(G'\) 的顶点数为 \(k\)，根据归纳假设，可以用4种颜色（这里设为红、蓝、绿、黄）进行着色。之后，将 \(v\) 放回并尝试着色。
- 当 \(v\) 的度数小于等于3时: 与 \(v\) 相邻的顶点最多只有3个。因此，4种颜色中至少有1种颜色没有被相邻的顶点使用。将这种未使用的颜色涂在 \(v\) 上，证明即告完成。
- 当 \(v\) 的度数为4时: 假设与 \(v\) 相邻的4个顶点（按顺时针方向记为 \(v_1, v_2, v_3, v_4\)）都涂上了不同的颜色（红、蓝、绿、黄）。在这里，考虑从整个图中只提取涂有“红”和“绿”的顶点，以及连接它们的边所组成的子图。如果 \(v_1\)（红）和 \(v_3\)（绿）在这个红-绿子图中不连通（也就是说，不存在通过红和绿的顶点从 \(v_1\) 到 \(v_3\) 的路径），就可以将包含 \(v_1\) 的连通分支的颜色反转（红变绿，绿变红）。这被称为“肯普链的反转”。反转后，\(v_1\) 变成绿色，周围的颜色减少为蓝、绿、绿、黄3种颜色。这样就可以给 \(v\) 涂上红色。如果 \(v_1\) 和 \(v_3\) 是连通的，由于平面图的拓扑性质（若尔当曲线定理），连接 \(v_1\) 和 \(v_3\) 的红-绿路径会分割 \(v_2\)（蓝）和 \(v_4\)（黄）。因此，\(v_2\) 和 \(v_4\) 绝对无法通过蓝-黄肯普链连接在一起，可以反转包含 \(v_2\) 的蓝-黄连通分支。无论哪种情况，都能将 \(v\) 周围的颜色减少到3种，从而对 \(v\) 进行着色。
- 当 \(v\) 的度数为5时: 考虑 \(v\) 周围的5个顶点 \(v_1, v_2, v_3, v_4, v_5\) 分别被涂上红、蓝、绿、黄、红（因为有5个所以1种颜色会重复）等情况。肯普扩展了度数为4时的论点，主张通过巧妙地组合反转2条不同的肯普链（例如，红-绿链和红-黄链），必定能将 \(v\) 周围的颜色减少到3种以下。他的方法是对“如果一方连通，那么另一方就会被分割”的逻辑进行了双重应用。
这个证明直观而美丽，似乎毫无逻辑漏洞。当时的数学家们深信四色问题至此已被完全解决。
希伍德的反例图：“双重肯普链交叉”的致命缺陷
然而在1890年，当时29岁的数学家珀西·约翰·希伍德（Percy John Heawood）精读了肯普的论文，在关于度数为5的顶点的论证中发现了致命的逻辑跳跃。
肯普在分别反转2条肯普链（例如，蓝-绿链和蓝-黄链）时，暗中假设它们是可以相互独立反转的。但是希伍德从几何学上严密地证明了，当这2条链共享部分顶点时，反转第一条链会改变图的着色状态，进而改变第二条链的连通性。
希伍德构建了一个具体的反例图（即现在所知的“希伍德反例图（Heawood graph）”或其派生，一个由25个顶点组成的极大平面图）。在这个图中，为了减少度数为5的顶点 \(v\) 周围的颜色，如果应用肯普的算法，在反转蓝-绿链的瞬间，原本不连通的蓝-黄链就会变得连通，接着反转蓝-黄链的话，刚才反转的绿色顶点又会恢复成原来的颜色，结果陷入了颜色数不减少的死循环。
肯普的“双重肯普链同时替换”，低估了平面图复杂的交织，没能从大局上维持局部的拓扑分割关系，最终导致了谬误。由于这一发现，肯普关于四色定理的证明彻底崩溃了。
五色定理的数学完全证明
虽然肯普的证明崩溃了，但希伍德不仅仅是破坏了它。他认识到肯普的想法（肯普链）本身极其有用，并利用它严密地证明了“所有平面图必定能用5种颜色涂满”，即《五色定理（Five Color Theorem）》。五色定理的完整证明过程如下。
定理: 任意平面图 \(G\) 都可以用5种颜色进行顶点着色。 证明: 对顶点数 \(n\) 使用数学归纳法。 当 \(n \leq 5\) 时是平凡的。假设对于所有 \(n=k\) 的平面图都可以用5种颜色着色，考虑 \(n=k+1\) 的平面图 \(G\)。 根据由欧拉公式导出的事实，\(G\) 中必定存在度数小于等于5的顶点 \(v\)。 从 \(G\) 中去除 \(v\) 后的图 \(G' = G - \{v\}\) 顶点数为 \(k\)，因此根据归纳假设，可以用5种颜色（颜色1、颜色2、颜色3、颜色4、颜色5）着色。 考虑在保持 \(G'\) 着色的情况下放回 \(v\)。
- 情况1: \(\deg(v) < 5\) 时。 与 \(v\) 相邻的顶点最多4个，所以5种颜色中至少有1种没有被相邻顶点使用。把该颜色涂在 \(v\) 上即可。
- 情况2: \(\deg(v) = 5\) 时。 假设与 \(v\) 相邻的5个顶点 \(v_1, v_2, v_3, v_4, v_5\) （按顺时针方向排列）都被涂上了不同的颜色（依次为颜色1、颜色2、颜色3、颜色4、颜色5）。（如果相同的颜色使用了2次以上，就会剩下至少1种未使用的颜色，可以将其涂在 \(v\) 上）。
在这里，考虑在图 \(G'\) 中仅由涂有颜色1和颜色3的顶点组成的导出子图，并设其中包含 \(v_1\) 的连通分支为 \(C_{13}\)（这就是肯普链）。
- 子情况2a: \(v_3 \notin C_{13}\) 时。 即不存在从 \(v_1\) 到 \(v_3\) 只经过颜色1和颜色3顶点的路径的情况。此时，即使将 \(C_{13}\) 内所有顶点的颜色反转（颜色1 \(\leftrightarrow\) 颜色3），着色的合法性也能保持。反转后，\(v_1\) 变为颜色3，\(v_3\) 也是颜色3，所以 \(v\) 的周围就不再有颜色1。因此可以给 \(v\) 涂上颜色1。
- 子情况2b: \(v_3 \in C_{13}\) 时。 即存在连接 \(v_1\) 和 \(v_3\) 的由颜色1和颜色3顶点组成的路径 \(P_{13}\) 的情况。将这条路径 \(P_{13}\) 与顶点 \(v\) 以及边 \((v, v_1), (v, v_3)\) 结合起来，就会在平面上形成一条闭合曲线（圈）。根据平面图的性质（若尔当曲线定理），这个圈将平面分割成内部和外部。 顶点 \(v_2\) 和 \(v_4\) 位于这个圈的不同侧（一个在内侧，另一个在外侧）。 此时，考虑由涂有颜色2和颜色4的顶点组成的肯普链 \(C_{24}\)。假设 \(v_2\) 和 \(v_4\) 被这条链连通，那么必须存在连接 \(v_2\) 和 \(v_4\) 的路径 \(P_{24}\)。但是，\(P_{24}\) 必须在平面图上不交叉地行进，却无法跨越由 \(P_{13}\) 形成的圈（违背平面图的定义）。 因此，连接 \(v_2\) 和 \(v_4\) 的颜色2和颜色4的路径绝对不存在。也就是说，包含 \(v_2\) 的颜色2-颜色4肯普链 \(C_{24}\) 中不包含 \(v_4\)。 所以，只要将 \(C_{24}\) 内的颜色反转（颜色2 \(\leftrightarrow\) 颜色4），\(v_2\) 就会变为颜色4，\(v\) 的周围就会消除颜色2。最终可以给 \(v\) 涂上颜色2。
综上所述，在任何情况下都可以对 \(v\) 进行着色，通过数学归纳法五色定理被完全证明。\(\blacksquare\)
这个证明极其优美地利用了平面图的拓扑学（若尔当曲线定理），并展示了肯普的“肯普链”概念在应用于单一不交叉的链时是多么强韧。然而，通往“四色”的道路，从这里开始将通过“可约性”和“不可避免集”的全新范式，突入无尽的计算之海。
第三章：放电法（Discharging Method）的数理与不可避免构形的导出
在希伍德之后，数学家们假设存在“无法用四色涂满的最小反例（Minimum Counterexample）”，并开始通过反证法探索它应该具有（或不该具有）怎样的结构。这里变得至关重要的是“可约构形（Reducible Configuration）”和“不可避免集（Unavoidable Set）”这两个强大的概念。
可约性（Reducibility）
可约构形是指，“如果整个图不能用四色涂满（即是最小反例），那么在那个图里绝对不可能存在”的顶点的局部子构形（模式）。 例如，“度数小于等于3的顶点”或“度数为4的顶点”就是可约构形。因为如前所述，只要使用基于肯普链的还原，如果它们存在，问题就能归结（还原）到更小的图，这与它是“最小反例”的假设相矛盾。 1913年，乔治·大卫·伯克霍夫（George David Birkhoff）证明了由特定6个顶点组成的被称为“伯克霍夫钻石”的构形也是可约的。虽然可约构形的发现不断取得进展，但如果不保证它们在图中“必定存在”，就无法完成证明。
放电法（Discharging Method）的数理结构
证明四色定理的最终战略，集中于**“找到一个全部由可约构形组成的不可避免集”**。 不可避免集是指“任何平面图（更准确地说，极大平面图）中，都必定包含该集合中至少一个构形”的构形列表。
为了构建和证明这个不可避免集，一个极其强大的武器是经过海因里希·黑施（Heinrich Heesch）改进的“放电法（Discharging Method）”。放电法是证明图论中结构定理的一种如魔法般的技巧，它类比使用了电磁学中的电荷概念。
放电法的数理过程如下：
- \[ch(v) = 6 - \deg(v)\]
由欧拉公式导出的等式 \(\sum_{v} (6 - \deg(v)) = 12\) 可知，整个图的初始电荷总和严格为 12（正值）。 此时，度数为5的顶点具有 \(+1\) 的电荷，度数为6的顶点具有 \(0\) 的电荷，度数大于等于7的顶点具有负电荷。（因为可以假设最小反例中不存在度数小于等于4的顶点，所以我们将最小度数考虑为5）。
电荷移动规则（Discharging Rules）的定义: 接下来，定义在相邻顶点之间移动电荷的规则。基本想法是“从具有正电荷的顶点（即度数为5的顶点）向具有负电荷的顶点（度数大于等于7的高次顶点）流动（放电）”。 例如，“当度数为5的顶点 \(v\) 与度数为7的顶点 \(u\) 相邻时，从 \(v\) 向 \(u\) 移动 \(\frac{1}{5}\) 的电荷”，像这样精细地设定几十甚至几百条规则。
- \[ \sum_{v \in V} ch'(v) = 12 > 0 \]
（\(ch'(v)\) 是移动后顶点 \(v\) 的电荷） 整体总和为正，意味着**“即使在电荷移动之后，也必定存在至少一个具有正电荷的顶点”**。
此时，基于局部结构（该顶点及其相邻顶点的度数模式），分析各顶点的最终电荷 \(ch'(v)\)。如果能够证明“不具有某种特定构形的顶点，在设定的放电规则下最终电荷必定小于等于零”，那么为了使最终电荷为正，那个“特定的构形”就必定存在于图中的某个地方。 如此一来，将使最终电荷为正的局部构形模式全部穷举列出的列表，就构成了“不可避免集”。
黑施确信，只要使用这种放电法，就一定能构建出由有限个（可能几千个）可约构形组成的不可避免集。但是，判定某个构形是否“可约”的计算量，会相对于边界的长度呈指数级爆发。依靠人类手工计算，检查几千个构形的可约性，即使耗尽寿命也是不可能的。
第四章：1976年，阿佩尔与哈肯的计算机验证算法
D-还原（D-reduction）与C-还原（C-reduction）的定义
20世纪70年代，伊利诺伊大学的肯尼斯·阿佩尔（Kenneth Appel）与沃尔夫冈·哈肯（Wolfgang Haken）着手开展了一项历史性的项目，将黑施的放电法与计算机的计算能力相结合。
他们所致力于的计算量最大的任务，是构形的“可约性判定”。可约性主要有以下2种类型：
- D可约性（D-reducibility / Direct reducibility，直接可约性）: 对于包围构形的环状边界（Ring）的所有可能的4种着色模式，如果它能扩展到构形内部进行涂色，或者通过反转边界颜色的肯普链，可以转换为能够扩展到内部的模式的情况。只要确认了这一点，就能直接断定该构形不包含在最小反例中。
- C可约性（C-reducibility / Contracting reducibility，收缩可约性）: 当存在D可约判定失败的模式时，考虑将该构形的一部分“收缩（将多个顶点合并为一个）”成更小的图，如果该收缩图可以4着色，则能证明原图也可以4着色的方法。
环状边界着色可能性判定算法
交给计算机（IBM 360）的任务是，对庞大数量的构形候选执行D可约性及C可约性的判定算法。
假设某个构形 \(C\) 具有边界环 \(R\)（长度为 \(k\)）。将环上的顶点用4种颜色涂色的组合最多有 \(4^k\) 种，即使考虑对称性，数量也极其庞大。例如当环的长度为 \(k=14\) 时，必须检查多达约20万种边界着色的有效性。 算法按照以下步骤进行：
- 生成边界环 \(R\) 的所有有效的4着色模式集合。
- 尝试构形 \(C\) 内部所有实际用4色涂色的方法，并记录它们与哪些边界模式相一致（是否能在内部扩展）。
- 对于内部无法扩展的边界模式，模拟肯普链的反转。如果通过反转，能够转移到已判明为“内部可扩展”的模式，那么其初始模式也视为“已解决”。
- 重复这种反转转移的搜索，如果所有边界模式都能被解决，就判定该构形 \(C\) 为“D可约”。
随着边界长度变长，计算时间会爆发，因此阿佩尔和哈肯将环长度限制为最大14的构形，并彻底调整了在其中构建不可避免集所需的放电规则。这个调整过程本身，就是人类和计算机之间巨大的连续试错。“人类修正放电规则，计算机输出不可避免集的候选并测试可约性，人类看失败的构形再次修正规则”，这种对话式的过程持续了数年之久。
1200小时的计算与“Q.E.D.”
1976年，他们终于发现了一个由经过精细构建的放电规则所导出的，由 1,936个 构形组成的不可避免集。随后，在伊利诺伊大学的大型计算机上运行了1200多个小时后，计算机确认了这1,936个构形全部是D可约或C可约的。
他们在论文摘要中简短地写道： “Every planar map is four colorable.” “每一个平面地图都是四可着色的。”
伊利诺伊大学数学系的邮戳上印上了一枚充满自豪的印章：“FOUR COLORS SUFFICE（4色足矣）”。这是数学历史上，计算机承担定理证明中核心演绎步骤的首次纪念碑式的事件。
第五章：数学界的剧震与“证明”的哲学
阿佩尔与哈肯的发表，不仅没有给数学界带来纯粹的喜悦，反而引发了深深的困惑和激烈的争论。
人类无法阅读的证明还是数学吗？
在自古希腊延续至今的数学传统中，“证明”意味着人类数学家可以一步一步地追踪逻辑步骤，从心底里理解其正确性并被说服。人们一直相信，证明的过程中蕴含着“为什么这个定理会成立”的深刻洞察以及结构之美。
但是，四色定理的证明却是个异类。论文里只有1,936个构形的列表以及对计算机算法的说明。实际的可约性判定追踪（运行记录）过于庞大，连印在纸上都很困难。不管多么天才的数学家，花尽一生去追踪这些手算过程，并确认没有逻辑缺陷，都是不可能的。
于是出现了一种前所未闻的状况：“为了相信证明是否正确，就必须相信计算机的硬件没有故障，还要相信阿佩尔和哈肯编写的汇编语言程序中没有Bug”。
科学哲学家托马斯·蒂莫斯科（Thomas Tymoczko）批评道，这说明证明是否从纯数学先验（a priori）真理的探索，堕落成了像物理学那样经验科学、实验性的东西呢。“证明”这一行为的定义本身，面临了认识论上的危机。
反驳与通过RSST的简化
面对批评，阿佩尔和哈肯反驳道：“不是只有美丽的证明才是数学。存在着需要庞大分类的本质上复杂的问题，既然超过了人类大脑的极限，借用机器的力量就是必然的进化。”
为了消除这种疑虑，许多数学家挑战了证明的简化与重新验证。1997年，尼尔·罗伯逊（Neil Robertson）、丹尼尔·桑德斯（Daniel P. Sanders）、保罗·西摩（Paul Seymour）、罗宾·托马斯（Robin Thomas）这4人（统称RSST），将放电法改良成了更系统、人类更易验证的形式，发表了新的证明，将不可避免集的大小从1,936个削减到了633个。这是一种经过洗练的算法，计算时间也只需数小时即可完成。
但是，这依然没有改变依赖“计算机计算可约性”的事实。那种完全能让人类直觉所理解的“美丽的纸笔证明”，至今仍未被找到（而且许多图论学者认为，这种证明原理上是不存在的）。
第六章：乔治·贡提耶基于Coq的完全形式化证明
为了在数学上完全消除“程序中可能有Bug”的不安，该怎么做才好呢？其最终答案就是使用“定理证明助手（Proof Assistant）”进行完全形式化（Formalization）。
2005年，法国国家信息与自动化研究所（INRIA）及微软研究院的乔治·贡提耶（Georges Gonthier）与本杰明·维尔纳（Benjamin Werner）一起，使用定理证明助手“Coq”，成功地将四色定理的证明从根本上完全形式化了。
超有限映射（Hypermap）与组合拓扑学形式化
Coq是一个从数学公理出发，遵循极其严密的逻辑规则体系（Calculus of Inductive Constructions: 归纳构造演算），对证明进行描述并机械验证的系统。
贡提耶最大的功绩，在于将平面图这一直观、几何的对象，翻译成了计算机能处理的完全代数、组合结构。为了表达图的顶点、边、面之间的关系，他定义了“超有限映射（Hypermap）”的数据结构。这是将图表达为“飞镖（半边）”的集合，以及其上的置换（排列）群的方法。由此，欧拉公式、若尔当曲线定理等拓扑学定理，被作为群论与有限集的组合逻辑而完全形式化。
证明程序自身的正确性证明
此外，贡提耶抛弃了阿佩尔·哈肯和RSST所使用的“用C语言编写的验证程序”，使用Coq的内部语言（Gallina）实现判定可约性算法本身。然后，他在Coq上数学地证明了**“如果这个判定算法输出 “True”，那么该构形就是真正可约的”这一算法的正确性本身**。
由于这一点，证明的可靠性发生了决定性的改变。再也不必担心“算法的Bug”了。因为，只要Coq核心的逻辑验证内核（几百行极其简单且经受时间考验的代码，使用德布鲁因索引等实现）在正确处理逻辑推理规则，那么贡提耶构建的庞大证明树，就能在数学上被保证是绝对正确的。
这是数学中“证明”的新顶点。从“人类阅读理解的证明（Informal Proof）”，进化到了“机器保证逻辑完整性的形式化证明（Formal Proof）”。四色定理成为了历史上第一个达到这一极限严密性的非平凡大定理。
第七章：平面图4着色问题与NP完全性的悖论
最后，让我们从计算复杂性理论（Computational Complexity Theory）的视角来看四色定理。这里存在着非常有趣的类似悖论的现象。
一般图的着色问题（判定给定图能否用 \(k\) 种颜色涂色的问题），是计算机科学中最著名的“NP完全（NP-complete）”问题之一。特别是“平面图的3着色问题（Planar 3-Colorability）”，已经被证明是NP完全的。也就是说，除非 \(\text{P} = \text{NP}\)，否则被认为不存在能在多项式时间内判定某个平面图能否用3色着色的算法。
那么，“平面图的4着色问题（Planar 4-Colorability）”又如何呢？如果3色是NP完全的，直觉上可能觉得4色也同样困难（NP完全）。
然而令人惊讶的是，平面图4着色问题（判定问题）的计算复杂性是 \(O(1)\)，也就是“常数时间（平凡）”的。 因为四色定理保证了“所有的平面图都能用4种颜色涂色”，所以算法甚至不需要去看输入的图，只需简单地输出“Yes”就能永远100%正确。这是定理强大的存在保证将判定问题的复杂性拉低到极限的一个美丽例子。
不过，这终究只是“能否着色”的判定问题（Decision Problem）。**“实际如何用4种颜色进行着色”的着色算法（Search Problem）**的构建，则是另一回事。 如果将阿佩尔·哈肯或RSST的证明程序作为算法实现，对于给定的 \(N\) 个顶点的平面图，就能获得可以求得实际4色涂色方案的算法。基于RSST证明的算法，被证明能够在最坏计算量 \(O(N^2)\) 的多项式时间内输出4着色。
也就是说，如果想把平面图涂上3种颜色，可能需要花费如同宇宙寿命一样的时间（NP完全），但在加上第4种颜色的瞬间，借助四色定理背后数学结构的恩赐，就存在了快速的（\(O(N^2)\)）算法。这是数学与计算机科学交叉所带来的、极度神秘且迷人的事实。
结论：四色定理留下的遗产
1852年英国青年朴素的地图着色问题，仅仅是作为一个拼图游戏开始的。但是，经过一个多世纪的时间，它开辟了名为图论的广阔而崭新的数学领域，发展了算法理论，最终向人类提出了“计算机能否证明数学”、“数学真理是什么”等根本性的哲学拷问。
四色定理的历史，是人类直觉的极限与机器这种新的逻辑引擎的可能性激烈交汇的历史。现在，像开普勒猜想（2014年，托马斯·黑尔斯的Flyspeck项目）以及法伊特-汤普森定理等其他巨大的难题，也通过使用定理证明助手进行形式化验证而被完全证明。
当我们在不经意间用4种颜色为地图着色时，那里不仅潜藏着欧拉多面体的美学、肯普天才般的挫折、希伍德严密的反证、黑施放电的数理、超级计算机持续闪烁数千小时的计算轨迹，还层层交织着Coq超有限映射的逻辑。四色定理作为展示数学如何超越人类思考框架而不断扩展的绝佳案例，将会被永远传颂下去。