400年前から存在する「フルーツを積み重ねるのに最もベストな方法は？」の答えをコンピューターがついに立証

by James Yu

「箱の中に最も効率よく球体を詰め込む方法は、果物屋が店先にオレンジを積み上げるのと同じ方法である」という400年前に提示された問題の証明の正確性が、コンピューターによってついに立証されました。

Proof confirmed of 400-year-old fruit-stacking problem - physics-math - 12 August 2014 - New Scientist
http://www.newscientist.com/article/dn26041-proof-confirmed-of-400yearold-fruitstacking-problem.html

「球体を積み上げるのに最も優れた方法は？」という問題は、惑星の運動に関するケプラーの法則を唱えたヨハネス・ケプラーが1611年に「最も効果的な方法は果物屋がオレンジを積み上げるのと同じ、ピラミッド式の積み上げである」と示したことを発端としているのですが、現在に至るまで証明はされていませんでした。

ケプラー予想と呼ばれるこの問題を証明したのが、ピッツバーグ大学のトマス・ヘールズ博士。ヘールズ博士はその時の感想を「突然10歳くらい若返った気がしました」と語りました。

by Rachel Patterson

といっても、ヘールズ博士によると、ケプラー予想の証明が完成したのは1998年のこと。球体を積み上げる方法は無限にありますが、そのほとんどは数千の方法のバリエーションに過ぎません。そこで、博士は積み上げ方法を数学的に表現できる数千種類に分類して、ソフトウェアを使って調査を行いました。

しかし、証明は300ページに及ぶ膨大な量だったため、12人の評者が4年かけてやっと正誤を確認。2005年に「99％の確率で正しい」ということでAnnals of Mathematics誌で発表されることとなりました。

一方で2003年にヘールズ博士らの研究チームは「フライスペック(小さな染み)」という名前のプロジェクトを開始。99％の正確さでケプラー予想が証明されたわけですが、さらに研究チームは「Isabelle」と「HOL Light」という、小さなエラーをも調べ抜くカーネルを持ったプログラムを使用して証明が正しいということをチェックしました。

by Stéphane PIA

そして2014年8月10日の日曜日に、フライスペックのチームはヘールズ博士の証明をコンピューターで厳密にチェックした結果、証明が正しかったことを発表しました。

このことについて、「技術によって人間が数学的証明の正しさを評価する必要がなくなった」とヘールズ博士は語ります。また研究には参加していないのですが、エディンバラ大学のアラン・バンディ教授も「これは大きな一歩である」とフライスペックの研究を評価しており、今後、多くの数学者が証明の助けとしてコンピューターを使用するようになるだろうと語っています。「世界的な数学者が自動的な定理証明へと手を伸ばしたという社会学的な出来事は、非常に重要な要素です。これからのケーススタディーとなるでしょう」とのこと。

すべてを俯瞰的に見ることは人間にとって困難であるため、プログラムによって数学の証明をチェックできるということは非常に有意義です。ヘールズ教授は「公式の検証が行われている間にやりたいアイデアはたくさんあります。願わくば次のプロジェクトが20年もかからないことを！」と語りました。