ケプラー予想
大きな容器を一定サイズの小球で一杯にしたとする。その配置の充填密度は球体積の総和を容器の容積で割ったもので与えられる。容器中の球の数を最大化することが、最大密度の配置を得ること、すなわち球をもっとも密に詰め込むことと等しい。
球を無作為に投げ込んでいくと密度は65%前後になることが実験的に確かめられている。これよりも密度を向上させるには、次の手順に沿って注意深く球を詰めていけばよい。まず、球を六方格子状に並べて初めの層を作る。次に、第一層の上でもっとも低い位置に球を並べていって第二層を作る。以下繰り返す。それぞれのステップで新しい層を置く場所には二通りの選択肢が存在するので、この自然な方法から密度が等しい配置は非可算無限個作られる。そのうち立方最密充填および六方最密充填と呼ばれる二つの配置が最もよく知られている。それらの平均密度は次の値を持つ。
π 3 2 = 0.740480489 ... {\displaystyle {\frac {\pi }{3{\sqrt {2}}}}=0.740480489\ldots }
ケプラー予想が主張しているのは、上が可能な密度の最大であり、これ以上の平均密度を持つ球の配置は存在しないということである。
3次元において、どのような構造のフォームがもっとも効率的(膜面積最小)か? 100年以上にわたり、この問題の解はいわゆるケルヴィン構造だと予想されてきた。しかし、ウィア=フェラン構造の発見がこの予想を覆した。ケルヴィン予想への反証が発見されたという衝撃は、ヘイルズによるケプラー予想の証明が容易に受け入れられなかった理由の一つであった。
ケプラー予想(ケプラーよそう、英: Kepler conjecture )とは、17世紀の数学者・天文学者ヨハネス・ケプラーに由来する、三次元ユークリッド空間における球充填に関する数学的な予想である。それによると、等しい大きさの球で空間を充填(パッキング)するとき、平均密度が立方最密充填配置(面心立方)ならびに六方最密充填配置を越えることはない。これらの配置の密度はおよそ74.05%である。
1998年にトーマス・C・ヘイルズ(英語版)はラースロー・フェイェシュ=トート(英語版)が提案した方法に従ってケプラー予想を証明したと発表した。多数のケース一つ一つを複雑なコンピュータシミュレーションでチェックするしらみつぶし法(英語版)であった。査読者は証明が正しいことを「99%確信している」と評した。よってケプラー予想は定理として受け入れられる寸前に来ている。2014年、ヘイルズに率いられたフライスペック・プロジェクト(英: the Flyspeck project)のチームは、定理証明支援ツールであるIsabell(英語版)および HOL Light (英語版)を組み合わせて用いることにより、ケプラー予想の形式的証明を完了したと発表した。