从1852年的偶然的发现，到1976年计算机的首次介入，再到21世纪的形式化验证。这里是全网最详尽、最易懂的四色定理科普基地。
四色定理指出：在平面上划分成若干连通区域的地图，如果相邻的区域（有公共边界线段，而非仅有一个公共点）必须涂上不同的颜色，那么只需四种颜色就足以完成着色。
注意“相邻”的定义。例如，美国的列文沃思县与犹他州仅在四角点接触，它们不算相邻，可以同色。又如，法国的下莱茵省和上莱茵省被河流分开，若河流不算陆地边界，则它们相邻；若算，则需仔细界定。通常数学模型中将边界视为线，点接触不算相邻。
想象一张世界地图。你可以用红色、蓝色、绿色、黄色四种颜色，给所有国家涂色，使得任何两个接壤的国家颜色都不一样。无论地图多复杂，这个结论都成立。
英国大学生弗朗西斯·古德里（Francis Guthrie）在绘制英国地图时发现，似乎只需四种颜色就能区分相邻郡县。他的弟弟威廉将问题请教导师奥古斯塔斯·德·摩根（Augustus De Morgan）。
凯莱（Arthur Cayley）在伦敦数学学会正式提出该问题，标志着四色定理成为数学界著名的未解难题之一。
希伍德（Heawood）证明了五色定理，即任何地图只需五种颜色。这暂时平息了部分讨论，但四色是否足够仍是谜。
美国伊利诺伊大学的阿佩尔（Kenneth Appel）和哈肯（Wolfgang Haken）利用电子计算机，经过1200小时的运算，证明了四色定理的正确性。这是数学史上第一个依赖计算机的证明。
罗伯逊（Robinson）、桑德斯（Sanders）、西摩（Seymour）和托马斯（Thomas）提出了更高效的算法，将验证时间缩短至数小时。
乔治·贡蒂尔（Georges Gonthier）使用Coq证明助手完成了四色定理的形式化验证，彻底消除了人们对计算机程序可能出错的疑虑。
四色定理的证明首先将地图转化为平面图（Planar Graph）。地图中的每个区域视为一个顶点（Vertex），如果两个区域相邻，则在它们对应的顶点之间连一条边（Edge）。这样，着色问题就转化为：给平面图的顶点着色，使得相邻顶点颜色不同，且颜色数最少。
在这个模型中，四色定理等价于：任何平面图的色数不超过4。图论工具的使用，使得数学家可以从拓扑和组合的角度研究这个问题，而不是局限于几何形状。
| 地图元素 | 图论对应 | 说明 |
|---|---|---|
| 国家/省份 | 顶点 (Vertex) | 着色的基本单位 |
| 公共边界 | 边 (Edge) | 连接相邻顶点 |
| 颜色 | 标签 (Label) | 相邻顶点标签不同 |
证明的核心思想之一是找到一个不可避免集。所谓不可避免集，是指任何平面图（假设存在反例，即需要5种颜色的最小反例图）必须包含该集合中的至少一个构形（Configuraton）。
阿佩尔和哈肯构建了一个包含1936个构形的不可避免集（后来简化为1476个）。这意味着，任何需要5种颜色的地图，必然包含这1936种局部结构之一。
仅仅找到构形是不够的，还需要证明这些构形是可约的。如果一个构形是可约的，意味着如果包含该构形的图是4-着色的，那么去掉该构形后的子图也是4-着色的，并且这种着色可以扩展回原图。
如果存在一个反例（最小反例），它必须包含不可避免集中的构形，但这些构形又是可约的，这就产生了矛盾：如果子图可4-着色，原图也可4-着色，那么原图就不是最小反例。因此，不存在需要5种颜色的地图。
这个过程极其繁琐，需要计算机逐一验证1936个构形的可约性，这是人类手工无法完成的。
在讨论四色定理时，网友们经常提到一些有趣的变体和误区：
在移动通信中，基站之间如果频率相同会产生干扰。可以将基站视为图的顶点，如果两个基站距离太近则连边。四色定理保证了在理想平面情况下，只需4种频率组即可避免干扰（实际中因地形复杂，可能需要更多）。
数独本质上是拉丁方，与图着色有异曲同工之妙。许多填色游戏（如俄罗斯方块变种、地图编辑器）都隐含了图着色的约束条件。理解四色定理有助于设计更复杂的谜题算法。
在编译器设计中，需要将变量分配到有限的CPU寄存器中。如果两个变量同时活跃，则不能分配同一寄存器。这可以转化为图着色问题。虽然图着色是NP完全的，但四色定理及其推广为启发式算法提供了理论边界。
在GIS软件中，自动地图着色是一个经典问题。虽然四色定理保证4色足够，但为了美观和区分度，软件通常允许用户自定义颜色数量，并使用贪心算法或回溯算法进行着色。
争议主要源于证明过程依赖计算机穷举，而非传统的人类可验证的数学推导。部分数学家认为这不符合数学证明的‘优雅’标准，因为人类无法手动检查成千上万次的逻辑判断。但主流数学界已接受其正确性，因为它可以通过形式化验证工具（如Coq）进行复核。
如果五根柱子围成一圈，每根都与左右两根相邻，则需要3种颜色（A红, B蓝, C红, D蓝, E绿）。如果是一排直线排列，则只需2种颜色。关键在于“相邻”的定义和拓扑结构。
四色定理本质上是针对平面图的。由于球面可以映射到平面（球极投影），因此四色定理同样适用于球面地图，如地球仪上的国家分布。任何球面地图都可以转化为平面地图，反之亦然。
地图着色问题是图论的起源之一，它推动了组合数学、拓扑学和计算机科学的发展。它不仅是一个有趣的数学谜题，更是解决现实世界中资源分配、冲突避免等问题的基础模型。
对于某些简单地图（如只有两个相邻区域），2种颜色就足够了。但四色定理保证的是“最坏情况”下的上限。也就是说，无论地图多复杂，4色永远够用，但有时3色或2色也够用。