Loading article…
17世紀の数学者であり天文学者でもあるヨハネス・ケプラーにちなんで名付けられたケプラー予想は、 3次元ユークリッド空間における球体の充填に関する数学的定理である。この予想によれば、空間を埋め尽くす同サイズの球体の配置で、立方最密充填（面心立方格子）と六方最密充填の配置よりも平均密度が高いものは存在しない。これらの配置の密度は約74.05%である。
1998 年、アメリカの数学者トーマス・ヘイルズは、フェイェス・トート (1953)が提案したアプローチに従って、ケプラー予想の証明を得たと発表した。ヘイルズの証明は、複雑なコンピュータ計算を用いて多数の個々のケースをチェックする、網羅的証明である。査読者は、ヘイルズの証明の正しさについて「99% 確信している」と述べ、ケプラー予想は定理として受け入れられた。2014 年、ヘイルズが率いる Flyspeck プロジェクトチームは、IsabelleとHOL Light証明支援システムを組み合わせて、ケプラー予想の正式な証明が完成したと発表した。2017 年、正式な証明は、学術誌Forum of Mathematics, Piに受理された。[ 1 ]
同じ大きさの小さな球体を大きな容器に詰め込むことを想像してみてください。例えば、同じ大きさのビー玉を1ガロンの陶器製の容器に入れるとします。この配置の「密度」は、すべてのビー玉の総体積を容器の体積で割った値に等しくなります。容器に入れるビー玉の数を最大にするには、容器の側面と底の間にビー玉を積み重ねて、可能な限り密度の高い配置を作り、ビー玉ができるだけ密に詰まるようにする必要があります。
実験によると、ビー玉をランダムに落とし、密に並べようと努力しなくても、密度は約65%になります。[ 2 ]しかし、ビー玉を次のように注意深く並べると、より高い密度が得られます。
各ステップで次の層を配置する方法は少なくとも 2 つあるため、この計画外の球体の積み重ね方法によって、数えきれないほど多くの等密度の充填構造が作られます。これらのうち最もよく知られているのは、立方最密充填と六方最密充填です。これらの配置はそれぞれ平均密度が
ケプラー予想によれば、これが最善の配置であり、これより高い平均密度を持つビー玉の配置は他に存在しない。手順 1～3と同じ手順に従う驚くほど多くの異なる配置が可能であるにもかかわらず、手順に従うか否かにかかわらず、同じ容器にこれ以上のビー玉を詰め込むことは不可能である。
この予想は、ヨハネス・ケプラーが1611年に論文「六角形の雪片について」の中で初めて述べたものです。彼は1606年にイギリスの数学者で天文学者のトーマス・ハリオットと文通を始めたことがきっかけで、球体の配置の研究を始めました。ハリオットはウォルター・ローリー卿の友人であり助手でもあり、ローリー卿はハリオットに積み重ねた砲弾の数え方の公式を見つけるよう依頼しました。この依頼がきっかけで、ローリー卿の数学者の知人は砲弾を積み重ねる最良の方法は何かという疑問を抱くようになりました。[ 3 ]ハリオットは1591年に様々な積み重ねパターンの研究を発表し、その後、原子論の初期バージョンを開発しました。
ケプラーは予想の証明を持っていなかったが、次の段階はカール・フリードリヒ・ガウス（1831年）によって踏み出され、球が規則的な格子状に配置されなければならない場合、ケプラー予想が正しいことが証明された。
これは、ケプラー予想を否定するような充填配置は、必ず不規則なものでなければならないことを意味していた。しかし、考えられるすべての不規則な配置を排除することは非常に難しく、これがケプラー予想の証明を困難にしていた理由である。実際、十分に小さな体積であれば、立方最密充填配置よりも密度の高い不規則な配置が存在するが、これらの配置をより大きな体積に拡張しようとすると、必ず密度が低下することが現在では知られている。
ガウス以降、19世紀にはケプラー予想の証明に向けた進展は見られなかった。1900年、ダフィット・ヒルベルトはこれを数学における未解決問題23問のリストに含めた。これはヒルベルトの第18問題の一部である。
解決策への次の一歩を踏み出したのは、ラースロー・フェイェシュ・トートであった。フェイェシュ・トート（1953）は、あらゆる配置（規則的配置と不規則的配置）の最大密度を決定する問題は、有限（ただし非常に多い）数の計算に還元できることを示した。これは、原理的には網羅的証明が可能であることを意味していた。フェイェシュ・トートが認識していたように、十分高速なコンピュータがあれば、この理論的な結果を問題解決のための実践的なアプローチに変えることができる。
一方、球体のあらゆる配置における最大密度の上限値を求める試みが行われた。イギリスの数学者クロード・アンブローズ・ロジャース（ロジャース（1958）参照）は約78%という上限値を確立し、その後他の数学者による努力によってこの値はわずかに減少したが、それでも約74%の立方最密充填密度よりはるかに大きかった。
1990年、呉毅祥はケプラー予想を証明したと主張した。その証明はブリタニカ百科事典とサイエンス誌で称賛され、祥はAMS-MAA合同会議でも表彰された。[ 4 ]呉毅祥（1993年、2001年） は幾何学的方法を用いてケプラー予想を証明したと主張した。しかし、ガーボル・フェイェシュ・トート（ラースロー・フェイェシュ・トートの息子）は論文のレビューで「詳細に関しては、多くの重要な主張には受け入れられる証明がないというのが私の意見だ」と述べた。 ヘイルズ（1994年）は祥の研究を詳細に批判し、祥（1995年）はそれに答えた。現在のコンセンサスは、祥の証明は不完全であるというものである。[ 5 ]
ラースロー・フェイェシュ・トートが提案したアプローチ[ 6 ]に従い、当時ミシガン大学に在籍していたトーマス・ヘイルズは、150個の変数を持つ関数を最小化することで、すべての配置の最大密度を見つけることができると判断した。1992年、大学院生のサミュエル・ファーガソンの協力を得て、彼は線形計画法を体系的に適用し、5,000種類を超える球体の配置のそれぞれについて、この関数の値の下限を見つける研究プログラムに着手した。これらの配置のそれぞれについて、立方最密充填配置の関数の値よりも大きい下限（関数の値）が見つかれば、ケプラー予想が証明されることになる。すべてのケースの下限を見つけるには、約10万個の線形計画問題を解く必要があった。
1996年にプロジェクトの進捗状況を発表した際、ヘイルズは完成が間近に迫っているものの、完了には「1、2年」かかるかもしれないと述べた。1998年8月、ヘイルズは証明が完了したと発表した。その時点で、証明は250ページに及ぶメモと、3ギガバイトのコンピュータプログラム、データ、結果から構成されていた。
証明の異例な性質にもかかわらず、『Annals of Mathematics』の編集者は、12人の査読者による審査で承認されることを条件に、その論文を掲載することに同意した。2003年、4年間の作業を経て、査読者委員会の委員長であるガーボル・フェイェシュ・トートは、委員会は証明の正しさについて「99%の確信」を持っているが、すべてのコンピュータ計算の正しさを証明することはできないと報告した。2005年、『Annals』は、ヘイルズの証明の非コンピュータ部分を詳細に記述した100ページの論文を掲載した（Hales (2005)）。Hales & Ferguson (2006)およびその後のいくつかの論文は、計算部分を記述した。ヘイルズとファーガソンは、 2009年の離散数学分野における優れた論文に対して、フルカーソン賞を受賞した。
2003 年 1 月、ヘイルズはケプラー予想の完全な形式的証明を作成する共同プロジェクトの開始を発表した。その目的は、HOL LightやIsabelleなどの自動証明チェックソフトウェアで検証できる形式的証明を作成することで、証明の妥当性に関する残りの不確実性をすべて取り除くことだった。このプロジェクトはFlyspeckと呼ばれ、これは Formal Proof of Kepler の頭文字である FPK の拡張である。2007 年にこのプロジェクトが開始されたとき、ヘイルズは完全な形式的証明を作成するには約 20 年かかると見積もった。[ 7 ]ヘイルズは 2012 年に形式的証明の「設計図」を公開した。[ 8 ]プロジェクトの完了は 2014 年 8 月 10 日に発表された。[ 9 ] 2015 年 1 月、ヘイルズと 21 人の共同研究者は、 arXivに「ケプラー予想の形式的証明」というタイトルの論文を投稿し、予想を証明したと主張した。[ 10 ] 2017年に、正式な証明が学術誌Forum of Mathematicsに受理された。[ 1 ]
{{citation}}ISBN /日付の不一致（ヘルプ）{{citation}}ISBN /日付の不一致（ヘルプ）