「球はピラミッド型に並べると一番沢山入る」 ← この証明に400年かかるとかアホなの？見てわかるだろ

400年の難問、「ケプラー予想の証明」やっと100％終わる

コペルニクスが提唱した地動説を、天体運行法則で不動のものにした偉人ヨハネス・ケプラー。

そのケプラーが1611年に提唱した「球は、八百屋に山盛りのオレンジみたいにピラミッド型に並べると
一番沢山入る」という説が、400年の歳月を経て、100％正しかったことがコンピュータの力で証明されました。

この立体最密充填の解答は、誰でも直感的になんとなく正しいことがわかります。けれども証明するとなると
超厄介で、世界歴代の天才がいくら頭脳を結集しても証明できなくて、ずっと「定理」ではなく「ケプラー予想」と
呼ばれ続けてきた難題中の難題です（参考）。

証明したのは、米ピッツバーグ大学のトマス・ヘールズ教授です。もともと氏が1998年に発表し、「フェルマーの
最終定理以来の難問が解けた！」と世界中が沸き立ったのですが、なんせ文章で300ページにも及ぶ遠大な証明でして、
間違いチェックがまだ終わっていなかったのです。どびょ～ん。

審査員12人が答え合わせに挑戦するも、4年後には残り1％のところでギブアップ。前例のない労力をつぎ込み
脳みそがショートするまでがんばって99％正しいことまではわかったのですが、もう精も根も尽き果ててしまって、
残り1％がどうしてもクリアできない…。相変わらずケプラー「予想」のままとなりました。

これではいかんと、2003年にはヘールズ教授自らが証明支援ツールで形式的証明を目指す「Flyspeckプロジェクト」を発表、
32コアの並列処理をガンガンやってしらみ潰しに答え合わせをしてきたのであります。

証明支援プログラムとして使ったのは、John Harrisonが開発した「HOL Light」と、HOL後継システムの「Isabelle」です。
いずれも実証が簡単な一連の短い論述をベースにするもので、時間さえ充分に与えてやれば、他の一連の論述
（例えば数学的証明）の正しさがチェックできます。

この「充分に与えてやれば」というのが曲者で、延々この日曜までかかりました。結果はセーフ、ミスはゼロ。
ヘールズ教授は、天晴れて証明が裏付けられた今の心境を「10年若返った気分だよ」とNew Scientistに語っていますよ。

http://www.gizmodo.jp/2014/08/post_15285.html