100年以上数学者を悩ませた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色問題は新しい証明法の先駆的な成果であった。
