四色定理

最小反例への帰着。もし定理が偽であれば、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年、1,936個の不可避配置からなる彼らのリスト(後に1997年にRobertson、Sanders、Seymour、Thomasにより633個へ整理された)のすべてが被約であることを、1000時間を優に超える計算機時間を用いて計算機的に検証した。これにより四色定理は、証明が本質的に計算機による検証に依拠した最初の大定理となり、その後独立に再検証され、2005年にはGonthierによってCoq証明支援系の中で一行ずつ形式的に検証された。

結論。すべての不可避配置が被約であるため、最小反例は存在しえない。すなわちどの平面グラフも5色以上を必要とせず、したがって任意の平面グラフ $G$ について $\chi(G) \le 4$ が成り立つ。