丸山、証明に失敗する

【 丸山、証明に失敗する 】

この間紹介した「連続体仮説」にしろ「Feit-Thompson定理」にしても、その意味を説明するのは簡単ではないのですが、今回紹介する「ケプラー予想」の意味は分かりやすいものです。

それは、箱におなじ大きさのボールを詰め込もうとした時、どのようにボールを並べたら、一番たくさんボールを詰め込めるかという問題です。ケプラーは、不規則にではなく規則的にボールを並べると一番高密度にボールを詰めこめると考えました。ある意味もっともだと思います。ただ、そのことを証明できませんでした。

紹介がおくれましたが、ケプラーというのは、あの天文学者のケプラーです。彼が、ボールの箱へのパッキング問題を考え予想を立てたのは 1611年のことでした。日本なら徳川幕府ができた頃です。

ただ、それから 300年たっても問題は解けませんでした。ヒルベルトは、1900年に20世紀の数学が解くべき23の未解決問題のリストを公開するのですが、「ケプラー予想」は、その18番目にランクインしています。それでも問題は解けませんでした。

ケプラーから数えれば400年たった 2014年、ヘイルズがこの問題を解決します。

彼は、不規則なボールの配置のパターンを数え上げ(5,000パターンぐらいあるそうです)、その全てのパターン総当たりで、詰め込みの密度の最小値を線形計画法を使って計算します。線形計画法の100,000個のプログラムが必要だったようです。

もちろん、その計算にはコンピュータが使われるのですが、同時に、彼はその計算が正しいことを検証するためのプログラムを開発します。そのプロジェクトを、flyspec Project といいます。それはGitHubで公開されています。

僕は、昨日、flyspec Project をビルドしようとしました。ところがなんとプロジェクトのビルドに失敗してしまいました。僕は、ケプラー予想の証明に失敗したことになります。いつも一発でビルドが通るとは限らないので、もう少し粘ってもよかったのですが、はやばやと諦めました。

というのも、このプロジェクトのビルドに成功したとしても、そのプログラムの実行(すなわち、ケプラー予想の証明)には、5,000個のCPUを使っても、一時間かかるということが分かったからです。とても、僕のくたびれたMac一台で太刀打ちできる計算量ではないのです。

今回、僕が証明に失敗したことは明らかですが、証明を断念したことを含めて、これはこれで面白い経験でした。

【 「証明へのコンピュータの利用 -- ケプラー予想の証明」を公開しました 】

https://youtu.be/OVU7q8ava0I?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg

スライドのpdfは、次からアクセスできます。

https://drive.google.com/file/d/1bYuddwlGnd1nqAUhm1Xks8T8HStLlTaL/view?usp=sharing

このトピックのまとめページは、こちらです。ほぼ毎日更新されると思います。https://www.marulabo.net/docs/math-proof/

セミナーへのお申し込みは、こちらからお願いします。
https://math-proof.peatix.com/


コメント

このブログの人気の投稿

マルレク・ネット「エントロピーと情報理論」公開しました。

初めにことばありき

宇宙の終わりと黒色矮星