四色定理

任意の平面地図の領域は、境界線（孤立点だけでなく線分や曲線）を共有するどの2つの領域も同じ色にならないように、高々 $4$ 色で塗り分けることができる。言い換えれば、自己ループを持たないすべての平面グラフ $G$ は $4$ 頂点彩色可能であり、その彩色数は $\chi(G) \le 4$ を満たす。

アルフレッド・ケンプによる1879年の有名な証明が11年間にわたり正しいと信じられた後、1890年にパーシー・ヒーウッドがその誤りを指摘して（同時に $5$ 色定理を救い出して）以来、この問題はコンピュータの本質的な支援によって証明された最初の大定理となった。1976年、ケネス・アッペルとヴォルフガング・ハーケン（ジョン・コッホがプログラミングを支援）は、ヒーシュの放電法と $1{,}936$ 個（後に $1{,}476$ 個に削減）の可約配置に対する網羅的なコンピュータ検証を組み合わせ、IBM 370で $1{,}200$ 時間以上の計算を行って証明を完成させた。人間の査読者がコンピュータによる場合分けを手作業で追いきれなかったため、この証明は数学的証明をめぐる哲学的議論を巻き起こした。1997年にはニール・ロバートソン、ダニエル・P・サンダース、ポール・シーモア、ロビン・トーマスが配置数を $633$ 個に減らし放電規則を整理した簡略化証明を発表した。そして2005年、ジョルジュ・ゴンティエ（バンジャマン・ヴェルナーとの共同研究を基盤として）が証明支援系Coqの上でロバートソン・サンダース・シーモア・トーマス証明の完全な機械検証付き形式化を成し遂げ、プログラムのバグや未検証ケースに関する疑念を完全に払拭した。