四色定理
FOUR COLOR THEOREM // 计算机证明第一案
> 给任何平面地图着色，四种颜色永远够——相邻区域不同色。这个连小学生都能听懂的问题，从 1852 年提出到 1976 年证明花了 124 年，而且证明方式掀翻了数学的地板：让计算机检查了 1936 个构形，人类无法用手复核——史上第一个重大的计算机辅助证明。此前的插曲同样经典：1879 年 Kempe 的"证明"被学界信了 11 年，1890 年被 Heawood 找出漏洞——但错误证明里的 Kempe 链方法活了下来，正是最终证明的核心工具。四色定理的故事是三条线的交织：一个天真的问题、一个错误的方法、一次信任的迁移——从信任数学家，到信任程序，再到 2005 年信任定理证明器。
Principle — 原理与来源
猜想诞生（1852）：伦敦大学学院学生 Francis Guthrie 给英格兰各郡地图着色时发现四色似乎永远够，通过哥哥 Frederick 转告数学家 Augustus De Morgan——猜想由此进入数学界（De Morgan 写信给哈密顿求助，哈密顿回信毫无兴趣）。此后 124 年里它难倒所有尝试者。
错证与救出（1879/1890）：律师出身的数学家 Kempe 1879 年发表论文"证明"四色猜想，被学界接受了 11 年（他因此当选皇家学会院士）。1890 年 Heawood 发现五邻国情形的处理有致命漏洞——但 Kempe 论文并非废纸：Heawood 用同样的方法立刻证出五色定理（手工可查的经典证明：欧拉公式 → 存在度 ≤5 顶点 → 归纳 + Kempe 链换色），且"Kempe 链"与"可归约构形"概念正是 86 年后最终证明的骨架。错误的方法论遗产比正确的结论更长寿。
计算机证明（1976）：伊利诺伊大学的 Appel 与 Haken 沿 Kempe-Heawood 框架，证明存在一个"不可免集"（任何平面图必含其中构形之一）并逐一验证 1936 个构形全部可归约——验证由计算机完成，机时以百小时计。1976 年 7 月结果公布，"四色够用"终成定理。哲学炸弹随之引爆：一个人类无法逐步复核的证明，还算数学证明吗？《纽约时报》报道时数学界分裂成两派——Imre Lakatos 一脉质疑"实验式数学"消解了证明的先验性；支持者则说：数学从没规定过验证必须用铅笔。
证明的进化（1996/2005）：1996 年 Robertson、Sanders、Seymour、Thomas 把不可免集缩到 633 个构形并附赠二次时间四着色算法；2005 年微软研究院的 Gonthier 与 Werner 用 Coq 定理证明器完成完全形式化验证——从"信那两位教授的程序"升级为"信一个被广泛审查的小内核"。"四色定理是真的"如今有了机器背书，但"人类能不能理解它为什么是真的"仍是开放问题。
Apply — 用在哪里
Simulate — 地图着色实验室 × 曲面拓扑沙盘
Personal Takeaways — 个人启示 · 03
表述的难度不等于求解的难度
四色、哥德巴赫、考拉兹——问题说得越像常识，越要警惕它的真实成本。接需求同理："就加个小功能"的表述复杂度与实现复杂度毫无关系，先估求解结构，再谈排期。
错误的证明可以留下正确的工具
Kempe 错了 11 年，但他发明的链式换法活到了最终证明里。复盘失败的方案时，别只问"哪里错了"，要问"哪个部件值得拆下来重用"——错误方案的零件库常常比正确结论更值钱。
信任可以外包，但要层层降级
四色定理的信任链一路下沉：信任数学家 → 信任教授写的程序 → 信任 Coq 的小内核。AI 时代同理：LLM 生成的代码不该被直接信任，该被更小的验证器信任——把"谁背书"设计进系统，比祈祷不出错可靠。