証明

ポアンカレ予想 (1904年)からペレルマン証明(2003年)まで99年。番組にも取り上げられるほどでしたが、ケプラー予想「最密球充填は、面心立方最密もしく六方最密かその組み合わせである。」(1611年)からヘイルズ証明(1998年)まで387年かかったのに、あまり話題にもなりませんでした。
証明が4色問題と同じで、多数の有限パターンをコンピュータでしらみつぶしに調べたというものらしい。
学生のときに、4色問題の証明は証明かという議論を聞いていたことがありました。ある人曰く、数学の証明に求められるものは美しさであり、あれは証明ではない。ある人曰く、命題の証明は命題が成り立つことの確認作業であり、あれは証明である。
私見では、コンピュータによる確認は証明じゃないですね。コンピュータは、（デジタル情報をアナログ素子で実現していることによるSN比の問題やDRAMを通過するα粒子の問題など）決定的動作をする機械ではないです。確率的に振る舞う機械。そういう機械で確認したのなら、確認した結果も確率的で、それは証明とは呼ばない。
ただ、パターンが有限であることが証明されてしまうと、きっと証明を求める人は興味を失ってしまうのでしょうね。