四色定理
任何平面地图都可用四种颜色着色使相邻区域不同色；1976 年 Appel–Haken 用计算机辅助证明。
详细描述
1852 年，英国大学生弗朗西斯·格思里（Francis Guthrie）在为英格兰各县地图着色时注意到：似乎只需四种颜色，就能保证任意两个拥有公共边界的相邻区域颜色不同。他向弟弟弗雷德里克提起此事，后者又转告其老师、数学家德·摩根（Augustus De Morgan）。这就是四色定理（Four Color Theorem）：对任何画在平面或球面上的地图，只要区域连通且”相邻”指共享一段（而非一个点）公共边界，则至多四种颜色即可完成合法着色。等价地，把区域变为顶点、相邻关系变为边，得到其平面对偶图，问题化为”每个平面图都可四点顶点着色”。
求解过程
在长达一个多世纪里，四色问题吸引了一代又一代数学家：
- 肯普（A. Kempe, 1879） 给出首个”证明”，引入肯普链思想，但 1890 年被希伍德（P. Heawood）指出漏洞；希伍德借此证明了较弱的五色定理。
- 希施（H. Heesch） 在 20 世纪 60 年代提出”放电法”（discharging）与”可约性”检验，把证明转化为寻找一个”不可避免且可约”的构型有限集合。
- 阿佩尔与哈肯（Kenneth Appel, Wolfgang Haken, 1976） 在伊利诺伊大学，借助研究生约翰·科赫（John Koch）的算法，把问题归约为 1936 个可约构型；他们用计算机完成约 1200 小时的构型可约性验证，于 1976 年 7 月宣布证明。完整论文 1977 年发表于《伊利诺伊数学期刊》，最终列表含 1482 个构型。这是史上第一个重大计算机辅助证明，曾引发”机器证明是否算证明”的持续争论。
意义
四色定理的计算机辅助证明具有里程碑意义：它第一次表明，大规模机械计算可以成为严肃数学证明的合法组成部分。这一范式此后催生了证明助手与形式化验证（如开普勒猜想的 Flyspeck 工程），从根本上拓宽了”可被接受的数学论证”的边界。