四色定理 ── コンピュータが証明の一部を担った日

四色定理は、平面上のどんな地図も、境界線を共有する隣どうしが同じ色にならないように4色で塗り分けられる、という定理である。1852年に問いとして現れ、120年以上解かれなかったこの問題を、1976年にイリノイ大学の Kenneth Appel と Wolfgang Haken が証明した。MacTutor（セント・アンドルーズ大学の数学史アーカイブ）は、2人が1976年6月21日に、コンピュータの助けを借りて四色予想を証明したと発表したと記録している。

この証明が歴史に残るのは、結論そのものよりも証明の形のためである。中心部分は、約1,500個の「配置」を計算機で一つずつ確かめる作業で、人の手では全体を検算できなかった。「人が読み通せない証明を証明と呼べるのか」という問いはこのとき大きな論争になり、半世紀後に AI が証明を書き始めた時代にも持ち越されている。

1852年の問いと、外れた証明

MacTutor によれば、問いの出発点は1852年の Francis Guthrie である。弟の Frederick がこの問いを Augustus De Morgan に尋ね、De Morgan は尋ねられたその日、1852年10月23日に William Rowan Hamilton へ手紙を書いている。

Kempe の証明は10年以上正しいと受け取られていた。MacTutor は、Heawood が1890年の論文の目的を「構成的というより破壊的」だと書き、広く認められていた証明の欠陥を示すと宣言したことを紹介している。四色問題は、もっともらしい証明が後から崩れる問題として知られるようになった。

Appel と Haken の証明 ── 不可避集合と可約性

証明の骨格は、Kempe 以来の2つの考え方を組み合わせたものである。どんな地図にも必ず現れる「配置」の集まり（不可避集合）をつくり、その集合のどの配置も、より小さい地図の塗り分けに帰着できる（可約である）ことを示せば、反例は存在し得ない。

難しさは集合の大きさにあった。MacTutor が引く1976年の告知論文によれば、必要な配置は約1,500個で、その大半はそれまで発表されていなかった。可約性の検証には約1,200時間の計算時間がかかった。

イリノイ大学の記事によると、Haken は1949年に Heinrich Heesch の講義を聞いてこの問題に関心を持ち、1960年代に取り組んだが、突破には強力なコンピュータが要ると考えた。そこでプログラミングに通じた同僚の Appel と組んだ。Haken は後に、自分たちは「最後の20%」をやっただけで、問題に取り組んだ5世代目にあたると語っている。

イリノイ大学数学科は、証明をたたえて郵便料金計器の印字に「Four Colors Suffice（4色で足りる）」の文字を入れた。この記事の画像は、1976年9月30日付のその印字である。

「計算機は証明の一部になれるか」という論争

同じ記事で Haken は、発表が熱狂と軽蔑の両方で迎えられたと振り返っている。1981年にニューヨークの大学でドキュメンタリーを撮影した際、ある数学教授は学生が2人と話すことさえ許さなかったという。Haken は、ある人に、計算機がどうして数学の証明の一部になれるのか、計算機は物理的な装置だ、と言われたことを語り、その指摘はもっともだったとも認めている。

哲学の側からは、Thomas Tymoczko が1979年に Journal of Philosophy に論文を書き、証明は人間の数学者が見渡せる（通覧できる）ものでなければならないという基準を持ち出して、Appel–Haken の証明は演繹の代わりに実験を置いたものだと論じた。論争は、個別の定理の正否を超えて「証明とは何か」という問いに及んだ。

Georgia 工科大学の Robin Thomas のページは、Appel–Haken の証明に残った懸念を2つ挙げている。計算機を使う部分は手で検証できないこと、そして手で確かめられるはずの部分も極めて複雑で退屈なこと、である。

別証明と形式検証 ── 疑いを機械で消す

この懸念に答えたのが1997年の別証明である。Neil Robertson、Daniel Sanders、Paul Seymour、Robin Thomas は、633個の配置と32個の放電規則（Appel–Haken は300個以上）で証明を組み直し、Journal of Combinatorial Theory Series B に発表した。計算機は依然として必要だったが、規模は大きく縮んだ。

さらに2005年、Georges Gonthier と Benjamin Werner は、定理証明支援系 Coq を使って証明全体を形式的に検証した。計算機の出力を人が信じるのではなく、論理の規則に従っているかを別のプログラムに一歩ずつ検査させるという発想である。同じ流れは、ケプラー予想の Flyspeck 計画（2014年）で、査読者が確信しきれなかった証明を形式検証で決着させるところまで進んだ。

誰に何が変わったか

変わったのは数学者の仕事の前提である。MacTutor は、当初の懸念はあったものの独立した検証によってやがて誰もが定理の証明を認めたと総括している。それと引き換えに、査読の方法、検算の分担、そして「確実さ」をどこに置くかが問い直された。

この問いは、AI が国際数学オリンピックの問題を解き始めた2024年以降に、別の形で戻ってくる。証明支援系 Lean で機械検証された AI の証明は、Coq による四色定理の検証の延長線上にある。一方で、人が読み通せない証明をどう扱うかは、エルデシュ問題と AI（2026年）をめぐる議論でも再び中心になった。計算機と数学の関係は AI と数学の年表 にまとめている。