ケプラー予想とは、球充填に関する数学的な予想で、この難問を1998年にトーマス・Ｃ・ヘイルズはコンピュータによるしらみつぶし法で証明した、と発表しました。 10万個ほどの線形計画問題を解いた証明論文は「250ページの手稿と3ギガバイトのプログラム、デ…