ケプラー予想（ヒルベルトの第18問題）の証明で大変だったこと

　ケプラー予想とは、球充填に関する数学的な予想で、この難問を1998年にトーマス・Ｃ・ヘイルズはコンピュータによるしらみつぶし法で証明した、と発表しました。
　10万個ほどの線形計画問題を解いた証明論文は「250ページの手稿と3ギガバイトのプログラム、データ、計算結果」（ウィキペディアによる）によって構成され、12人の査読者が4年にわたって精査したあげく、2003年に「99％は正しい気がする」と判断しました。
　それに頭に来たヘイルズは、完全な形式的証明（証明図）を作成するためにさらにコンピュータを使う「フライスペック計画」を立ち上げ、20年かかるかも、と言われていた計画は2014年の夏に一応終了しました。
　しらみつぶし法というのはかつては数学者による禁断の呪法でしたが、21世紀は「それを構築するコンピュータのプログラムが間違っていなければ問題ない」ということになったようであります。