## 四色定理是啥？ > **一句话**：在一张平面地图上，不管疆域怎么七扭八歪，只要相邻的两个国家（共享边，而不是只在点上接触）必须涂成不同颜色，**4 种颜色就始终够用，再多的颜色其实是浪费。** --- ## 1 ▪ 最直观的小实验 1. 画几个轮廓怪异的省份，让它们两两接壤。 2. 拿 4 支彩笔（红、绿、蓝、黄），从随便一个省开始上色： - 给它红色； - 相邻省不能再用红，于是挑绿； - 继续往外涂。如果卡住，把涂错的改成其它没用过的颜色。 3. 不管地图多复杂，最后一定能在 4 种色以内完成。 --- ## 2 ▪ 正式陈述（平面图版本） - 把平面地图看成“顶点=国家、边=共同边界”的**平面图** G； - **四色定理**：对任何平面图 G，存在一个顶点着色函数 c:V(G)→{1,2,3,4}c:V(G)\to\{1,2,3,4\}，使得相邻顶点颜色不同。 - 换言之：平面图的**色数 χ(G) ≤ 4**。 --- ## 3 ▪ 为什么它这么有名？ |维度|亮点| |---|---| |**朴素**|小学生也听得懂题意，却困扰数学家一百多年。| |**历史戏剧性**|1852 年提出（Francis Guthrie），1879 年 Kempe 给出“证明”，11 年后被 Heawood 找出漏洞；此后各路尝试屡战屡败。| |**首个计算机证明**|1976 年 Appel & Haken 用 IBM 370 机，列举 1 483 个“不可约配置”，借助 1 200 小时计算检验，首度完成严格验证 → 计算机辅助证明时代的开端。| |**引发争议**|“机器算过就是证明？” 数学界围绕可验证性、可读性讨论多年，催生了可形式化证明、交互式定理证明器的发展。| > 1997 年 Robertson、Sanders、Seymour、Thomas 进一步把不可约集合缩到 633 个，并用 现代验证器重跑；2017 年 Coq 系统给出完全形式化证明。 --- ## 4 ▪ 证明思路（极简口味） 1. **不可约配置** - 如果存在五色以上才涂完的最小“坏图”，那么这个坏图里有一种小结构叫“不可约配置”。 2. **可缩减性** - 通过“缩顶”“展顶”等操作，把含该配置的图化简为更小图；若小图四色可涂，则原图也可涂 → 矛盾。 3. **穷举 + 计算机检查** - 列出所有可能的不可约配置集合，证明它们**可缩减**。若平面图中任何一个必含于集合，则不存在坏图。 4. **结果** - Appel–Haken 找到 1 483 个，计算机验证全部可缩减 → 四色定理成立。 --- ## 5 ▪ 应用场景与旁枝 |场景|说明| |---|---| |**电子布线/频谱分配**|PCB导线层、蜂窝基站频率避免冲突，可转为平面图着色问题。| |**考试排课、资源调度**|某些无交叉约束模型可投影为平面图 → 四色足够。| |**趣味艺术**|设计四色地图拼图，或“最难四色涂色游戏”。| |**数学延伸**|变体：“平面图加限制”→三色定理，非平面图→需要更多颜色；拓扑图面着色 (哈特伍德公式)。| --- ## 6 ▪ 常见误解 |误解|事实| |---|---| |“任意地图都恰好需要 4 色”|有些地图 2 色就够（国际象棋格），4 色是 **上界**。| |“四面交汇也算相邻”|只在一个点接触 ≠ 相邻；必须共享 **边界线段**。| |“四色定理=哈定猜想”|哈定猜想谈的是球面均匀点集的色数，概念不同。| |“证明就是把所有地图枚举完”|实际只枚举**不可约的局部结构**，再用可缩减性推全局，不计无穷多图。| --- ### 小结 - **四色定理**：任何平面地图只需 4 种颜色就能让相邻国双色不同。 - **困扰 124 年**，终被“计算机辅助证明”攻克。 - **启示**： 1. 和谐美学：复杂的相邻关系，极简的 4 色足矣； 2. 证明范式变革：当人工推理遇到极大穷举，计算机可成“定理伙伴”。