四色定理

归约为最小反例。若定理不成立,取一个需要5种或更多颜色、顶点数尽可能少的平面图。在保持平面性的前提下增加边只会使所需颜色数增多不会减少,因此这个最小反例可以假设是一个极大平面图(三角剖分),其中每个面(包括外部面)恰好由3条边围成。

放电法准备。给每个顶点 $v$ 分配初始电荷 $6 - \deg(v)$。结合 $V - E + F = 2$ 以及 $2E = \sum_v \deg(v)$ 和 $3F \le 2E$(每个面至少有3条边),所有顶点上的电荷总和恰好等于 $12$,因而严格为正。放电法随后按照一套固定规则在相邻顶点间局部转移电荷,而不改变这个总和;分析放电后正电荷必然残留在何处,可以证明图中某处必定出现某个低度顶点及其特定邻域模式。这有限多种模式称为不可避配置,因为每个平面三角剖分中至少会出现其中一种。

可约性。称一个配置是可约的,是指每当它出现在假设的最小反例中时,通过删去或收缩该配置所得较小图的任何4着色,总能重新扩展为整个图的4着色,这与最小性矛盾。Appel和Haken于1976年用计算机验证了他们列出的1936个不可避配置(后于1997年被Robertson、Sanders、Seymour和Thomas精简为633个)全部都是可约的,共耗费一千多个小时的计算机时间。这使四色定理成为第一个证明本质上依赖机器计算的重大定理,此后又被独立重新验证,并于2005年由Gonthier在Coq证明助手中逐行进行了形式化核验。

结论。由于每个不可避配置都是可约的,最小反例不可能存在:没有平面图需要5种或更多颜色,因此对任意平面图 $G$ 都有 $\chi(G) \le 4$。