自動で四色問題を解くソフト - 四色問題から四色定理、その後

1976年、ヴォルフガング・ハーケンとケネス・アッペルにより初の証明が為された。(*1, *2)

ただし、この証明には様々な批判の声が上がった。数学の証明にコンピュータを用いているということへの懸念もあったようではあるが、本質的には、検証が困難であることが、受け入れられずらかった要因ではないか、と思う。

最終的な証明の全ては「Every Planer Map is Four Colorable」という書籍にまとめられているが(*3)、そのページ数は743ページに上る。1405個の不可避集合に対して、手作業とコンピュータ演算での証明が為されており、実際に検証を試みたロバートソンは、論文中で、「初めに検証を行おうと考えたが、途中で方向転換し独自の証明を試みた」と、記述している。

ハーケンとアッペルの証明方法は、全ての地図を構成する不可避な可約配置に対して証明を行うものであった。当時、フランク・アーレアを含め、複数のチームが同様に、コンピュータを用いて不可避集合を解くアプローチを行っており、ハーケンとアッペルは間違いなくこのレースの勝者である。一方で、後にロバートソンらが発表した分量まで、論文の精査を行っていたら、おそらく、四色定理の証明者は、別の者たちになっていたはずである。そう考えると、苦渋の決断をした部分もあるのではないかと憶測される。

ただ、残念なのは一度証明されたことで、四色問題に対する数学者たちの熱が冷めてしまったことで、後にロバートソンらが発表するまで20年近くも、不可避集合と放電手続きに関しての整頓が行われなかったことである。

プログラムに携わる身としては、不可避集合と放電手続きの整頓は、プログラムの実装量でもあり、とても大切なことなので、これは大変残念なことである。

1996年、ニール・ロバートソンらにより、ハーケンとアッペルのものより、よりシンプルな証明が為された。(*4)

基本的なアプローチの方向性はハーケンとアッペルの証明と同じであるが、従来の放電手続きよりシンプルな放電手続きを考案し、不可避集合の数を1405個から633個に抑えたことが特徴的である。また、証明に用いるプログラムをインターネット上に公開し、家庭用コンピュータを用いて、数時間で証明の検証を可能にしたことも有名である。

2004年、ジョルジュ・ゴンティエが定理証明支援系言語であるCoqを用いて、更にシンプルな証明を行った。(*5) これにより、もはや四色定理に異議を唱えられる可能性はまずなくなったと考えられる。

*1 "EVERY PLANAR MAP IS FOUR COLORABLE 1" BY K. APPEL AND W. HAKEN (BULLETIN OF THE AMERICAN MATHEMATICAL SOCIETY Volume 82, Number 5, September 1976)

*2 "Every planar map is four colorable. Part II: Reducibility" BY K. Appel, W. Haken, and J. Koch (Illinois J. Math. Volume 21, Issue 3 (1977), 491-567.)

*3 CONTEMPORARY MATHEMATICS 98 "Every Planar Map is Four Colorable" by Kenneth Appel and Wolfgang Haken

*4 "A NEW PROOF OF THE FOUR-COLOUR THEOREM" by NEIL ROBERTSON, DANIEL P. SANDERS, PAUL SEYMOUR, AND ROBIN THOMAS (ELECTRONIC RESEARCH ANNOUNCEMENTS OF THE AMERICAN MATHEMATICAL SOCIETY Volume 2, Number 1, August 1996)

*5 "A computer-checked proof of the Four Colour Theorem" by Georges Gonthier (Microsoft Research Cambridge)