四色定理

任何平面地图的区域都可以用至多 $4$ 种颜色进行着色，使得共享边界线（不止孤立交点）的任意两个相邻区域颜色不同。等价地说，每个无自环平面图 $G$ 都是 $4$-顶点可着色的，即其色数满足 $\chi(G) \le 4$。

阿尔弗雷德·肯普1879年著名的证明在被普遍接受十一年后，于1890年被珀西·希伍德指出漏洞（希伍德同时挽救出了 $5$ 色定理）；此后，该问题成为首个必须依赖计算机辅助才得以证明的重大定理。1976年，肯尼思·阿佩尔与沃尔夫冈·哈肯（在约翰·科赫的编程协助下）将希施的放电法与对 $1{,}936$ 个（后缩减至 $1{,}476$ 个）可约构型的计算机穷举检验相结合，耗费了IBM 370计算机逾 $1{,}200$ 小时。由于审稿人无法手工核验计算机的穷举分析，这一证明引发了广泛的哲学争论。1997年，尼尔·罗伯逊、丹尼尔·P·桑德斯、保罗·西摩与罗宾·托马斯发表了简化证明，仅需检验 $633$ 个构型并采用了更清晰的放电规则。最终在2005年，乔治·贡蒂埃（基于与本杰明·韦尔纳的合作工作）在定理证明助手Coq中完成了对罗伯逊-桑德斯-西摩-托马斯证明的完全机器核验形式化，彻底消除了人们对程序漏洞或未核验情形的疑虑。