ケプラー予想？

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

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

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

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

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

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

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

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

複雑＆高度な数学的証明は毎年何百本となく世に出ています。こんな風に人力ではムリでも自動定理証明機で実証できるとなれば、気が遠くなるような答え合わせの部分はコンピュータに任せてしまって、人間はクリエイティヴな思考に集中できます。これをふまえると今回の発表は、教授以外の人にも朗報ですね。

そうかコンピュータもスゴイが
４００年前に唱えていることも
すごい

コンピュータの仕事をしているてまえ
プログラムにバグはなかったのか？
と考える嫌な奴がここに居ます（笑）

数学で証明できなかった事が
このコンピュータの時代になって証明できるとは

コンピュータの仕事をしていると
最近人工知能の事を知りたくなるのです

今やってる仕事
人工知能が出来れば安く高度なシステムが作れるのに
なんて考えます

地道に作り
できたら発表？
しない安くて高度なシステムを作り
稼ぎたい（笑）

どこでもドアがもし作れたら
どこでもドアを作って販売はしません
旅行代理店を経営し
安く世界旅行をどこでもドアで提供したい（笑）

こんな奴にたいしたものは作れないですきっと
考えが汚い（笑）

タグ：ケプラー予想 数学 証明 コンピュータ バグ