解法: 計算機検証による可約性を伴うAppel–Hakenの放電法証明(1976年)

どの地図にも双対によって平面グラフが対応する:地図の各領域の内部に一つずつ頂点を置き、二つの領域が辺を共有するたびに対応する二頂点を辺で結ぶ。地図が四彩色可能であることは、この双対グラフ $G$ が $\chi(G) \le 4$ を満たすことに等しい。ここで $\chi(G)$ は彩色数、すなわち適切な頂点彩色に必要な最小の色数である。ループは決して生じず(領域は自分自身と隣接しない)、多重辺は一つに潰しても彩色可能性に影響しないため、$G$ は単純平面グラフとしてよい。

定理が成り立たないと仮定し、頂点数が最小の反例 $G$ を選ぶ:自然数の整列性により、反例が一つでも存在すればこのような $G$ が存在する。この極小性が議論全体の原動力である——$G$ の真部分グラフや縮約グラフはすべてより小さく、したがって四彩色可能であり、以降のすべてのステップは「より小さいグラフを彩色してから、取り除いた部分にわたって彩色を修復する」という形でこれを利用する。これはまた、$G$ が疎すぎず硬すぎもしない理由を説明する:$K_5$ は非平面的なので $G$ は単純なクリーク障害にはなり得ず、平面的であることが $G$ に次のステップで調べる低次数の構造を含ませる。

この戦略——極小反例を仮定し、その必ず現れるはずの部分構造がすべて可約であることを示す——は、Kempe の1879年の試み(Heawood が1890年に誤りを指摘)に遡り、Birkhoff、そして Heesch によって発展させられた。Heesch が導入した回避不能集合と可約性の概念を、Appel と Haken が1977年の Illinois Journal of Mathematics の論文で完成に導いた。