四色問題 証明の歴史

Pocket

100年以上数学者を悩ませた4色問題の証明の年表。証明が完了したとき、コンピュータを利用したため、正しさの面や方法の面で大きな議論を呼んだ。

世界地図の4色塗り分け
応援ありがとうございます

年表

19世紀半ば:ガスリー、4色問題の着想
1852:ド・モルガン、ハミルトンへの手紙で地図塗り分けにふれる。「学生が4色あればすべての地図はぬれるといってきたが、正しいか」・・・実はこの学生こそガスリーである
1878:アーサー・ケイリー、問題を再び提唱

1880:ケンプ、ケンプ鎖を発想し、4色問題を解決・・・ところが、この証明は間違いであった
1889:ヘイウッド、ケンプの方法に誤りを発見、しかし、ケンプ鎖の方法で5色定理は証明
1897:ヴェルニッケ、不可避集合の概念を提唱
1913:バーコフ、可約配置の研究
1926:レイノルズ、27国までの地図は4色で塗れると証明
1935頃:ヘーシュ、放電法の考案
1967:ハーケン、ヘーシュから方法を学ぶ。コンピュータでの調査を開始
1970:ヘーシュ、8900種類の地図を調べればよいことを示す。これは4色問題の有限化といわれる。
1971:ヨシオ・シマモト、コンピュータを活用し4色問題を解決したと報じられる。・・・これも間違っていた。
1972:アッペル、ハーケンに協力を申し出る。プログラムの高速化。
1976:ハーケン、アッペル、コンピュータを使ってすべてのパターンを調べ、解決。

豆知識

・実際には、ガスリーの兄が着想し、ガスリーに話してきたのがきっかけだったらしい。兄の方はのちに弁護士になった。

・アッペルはもともとポアンカレ予想に取り組んでいたが、完成できなかった。

考察

・コンピュータと証明
この問題の証明が引き起こした議論として、コンピュータにはバグがあるので間違っているかもしれない、ということと、従来の論述形式でないと美しくない、という2点があるが、前者については、繰り返し検証したり、コンピュータの利用法をより洗練させたりして、受け入れられている。 後者は、美意識の問題であり、主観的なものなので、個人差が激しそうである。

・コンピュータを使わない証明は得られるか
いまだに、コンピュータを使わない証明は得られていないが、今後、得られる可能性はあるだろうか。数学者の間では、そのような証明があるならとっくに得られていてもよいはずだ、というのが見解らしい。これを得るためには、不可避集合と可約配置のアプローチ以外の方法を取るか、何かしらのブレークスルーがないと無理なのではないかとも思われる。

・ケプラー予想への間接的な貢献
ケプラー予想は、さらにこの後コンピュータを使って証明された。これに関して、さきに4色問題がコンピュータによって説かれたことで、ケプラー予想の証明に対する抵抗が薄れた点は評価できる点といえる。そういう意味で4色問題は新しい証明法の先駆的な成果であった。