ケプラー予想

提供: testwiki
2024年12月28日 (土) 13:43時点におけるimported>Gejikeijiによる版 (→発端)
(差分) ← 古い版 | 最新版 (差分) | 新しい版 → (差分)
ナビゲーションに移動 検索に移動

ケプラー予想（ケプラーよそう、テンプレート:Lang-en-short）とは、17世紀の数学者・天文学者ヨハネス・ケプラーに由来する、三次元ユークリッド空間における球充填に関する数学的な予想である。それによると、等しい大きさの球で空間を充填（パッキング）するとき、平均密度が立方最密充填配置（面心立方）ならびに六方最密充填配置を越えることはない。これらの配置の密度はおよそ74.05%である。

1998年にテンプレート:仮リンクはテンプレート:仮リンクが提案した方法[1]に従ってケプラー予想を証明したと発表した。多数のケース一つ一つを複雑なコンピュータシミュレーションでチェックするテンプレート:仮リンクであった。査読者は証明が正しいことを「99%確信している」と評した。よってケプラー予想は定理として受け入れられる寸前に来ている。2014年、ヘイルズに率いられたフライスペック・プロジェクト（テンプレート:Lang-en-short）のチームは、定理証明支援ツールであるテンプレート:仮リンクおよびテンプレート:仮リンクを組み合わせて用いることにより、ケプラー予想の形式的証明を完了したと発表した。

背景

立方最密充填（左）および六方最密充填（右）。

大きな容器を一定サイズの小球で一杯にしたとする。その配置の充填密度は球体積の総和を容器の容積で割ったもので与えられる。容器中の球の数を最大化することが、最大密度の配置を得ること、すなわち球をもっとも密に詰め込むことと等しい。

球を無作為に投げ込んでいくと密度は65%前後になることが実験的に確かめられている。これよりも密度を向上させるには、次の手順に沿って注意深く球を詰めていけばよい。まず、球を六方格子状に並べて初めの層を作る。次に、第一層の上でもっとも低い位置に球を並べていって第二層を作る。以下繰り返す。それぞれのステップで新しい層を置く場所には二通りの選択肢が存在するので、この自然な方法から密度が等しい配置は非可算無限個作られる。そのうち立方最密充填および六方最密充填と呼ばれる二つの配置が最もよく知られている。それらの平均密度は次の値を持つ。

π32=0.740480489…

ケプラー予想が主張しているのは、上が可能な密度の最大であり、これ以上の平均密度を持つ球の配置は存在しないということである。

発端

Strena Seu de Nive Sexangula（新年の贈り物あるいは六角形の雪について）の図版。ケプラー予想を図解している。

ケプラー予想はヨハネス・ケプラーの論文『新年の贈り物あるいは六角形の雪について』[2][3]で初めて述べられた。ここでは、雪の星型の結晶の形状を説明する目的で言及されている。低温で水の粒子が凝縮し、最も密な配置をとるから、というのがその理由である。少し後のデカルトの『気象論』にも類似の言明がある。またイエズス会の宣教師を介して中国にも伝えられ、『天経或問』を通じて日本にも伝わり、幕末の土井利位『雪華図説』でも紹介されている[4]。

ケプラーが球の配置を研究し始めたのは、1606年におけるイギリス人数学者・天文学者、トーマス・ハリオットとの文通がきっかけである。ハリオットは友人で雇い主のウォルター・ローリーから船倉に砲弾を効率的に積み込む方法の問題を与えられていた。ハリオットは1591年に様々な積み上げパターンの研究を出版し、さらに進んで初歩的な原子論を発展させた。

19世紀

ケプラー本人は予想を証明できなかったが、ガウスは球が規則配置を取る場合についてケプラー予想が正しいことを証明し[5]、問題の解明に一歩近づいた。

つまり、ケプラー予想の反証となる充填配置があるとすれば不規則配置でなければいけない。しかし、実現可能な不規則配置をすべてチェックするのは非常に困難で、それこそケプラー予想をここまで証明困難なものにした理由である。

ガウス以降、19世紀の間はケプラー予想の証明に向けた進展はなかった。1900年にダフィット・ヒルベルトが数学における23の未解決問題を提起したとき、ケプラー予想は関連する問題とともに第18問題に挙げられた。

20世紀

解決に向けて次のステップを踏み出したのはラースロー・フェイェシュ＝トートである。彼は、規則・不規則を問わずあらゆる配置の最大密度を求める問題が、有限個の（しかし非常に多数の）計算に還元されることを示した[1]。これはしらみつぶし法による証明が原理的に可能だということである。フェイェシュ＝トートも気づいていたように、十分高性能なコンピュータがあればここからケプラー予想解決への現実的なアプローチが得られる可能性があった。

他方では、あらゆる可能な球配置の最大密度の上界を見つけようという試みがなされていた。イギリスの数学者クロード・アンブローズ・ロジャーズは一つの上界として約78%の値を得た[6]。それに続く数学者の努力によりこの値はわずかに引き下げられたが、立方最密充填の約74%には程遠かった。

1990年にウ＝イ・シアン（項武義）はケプラー予想を証明したと発表した。この成果は「エンサイクロペディア・ブリタニカ」および「サイエンス」誌で好意的に取り上げられ、シアンはAMS-MAAジョイントミーティングに招待される栄誉を得た[7]。シアンの主張は幾何学的な手法でケプラー予想を証明したというものだった[8][9]。しかしながら、ガボル・フェイェシュ＝トート（ラースローの息子）は論文のレビューで「細部に目を向ければ、重要な言明の多くが容認できるような証明を欠いている」と述べた。ヘイルズはシアンの仕事を詳細に批判し[10]、シアンはこれに反論した[11]。現在ではシアンの証明は不完全なものだったと認められている[12]。

ヘイルズの証明

ミシガン大学に在籍していたトマス・ヘイルズは、ラースロー・フェイェシュ＝トートが提案したアプローチ[1]にならい、150個の変数を持つある関数を最小化することによって最大密度配置を見出せると考えた。1992年、大学院生のサミュエル・ファーガソンを助手としたヘイルズは、系統的な線型計画法により、すべての異なる配置の集合に含まれる5000種以上の配置一つ一つについて関数値の下界を求める計画に着手した。すべての配置で関数の下界が立方最密配置の関数値を超えるならば、それがケプラー予想の証明になる。可能なすべてのケースについて下界を求めるには、10万個ほどの線形計画問題を解く必要があった。

1996年に研究プロジェクトを公表するに際して、終結は目前ながら完了まで「1・2年」かかるかもしれない、とヘイルズは述べた。1998年の8月にヘイルズは証明の完了を発表した。この時点で証明は250ページの手稿と3ギガバイトのプログラム、データ、計算結果から構成されていた。

証明の形式が異例だったにもかかわらず、Annals of Mathematics誌の編集者は掲載に同意したが、12人の専門家による査読を条件とした。2003年、四年間の作業を経て、査読者団の筆頭であったガボル・フェイェシュ＝トートは証明が正しいことに「99%の確信を持っている」と報告した。しかし、コンピュータによる計算がすべて正しいと保証することはできなかった。

2005年、ヘイルズは100ページの論文で、証明の中でコンピュータを用いない部分を詳述した[13]。ファーガソンとの共著による2006年の論文および数篇の続報ではコンピュータによる部分を報告した[14]。2009年にヘイルズとファーガソンは離散数学の分野の優れた論文に対して贈られるファルカーソン賞を受賞した。

形式的証明

2003年1月、ヘイルズはケプラー予想の完全な形式的証明を求める共同プロジェクトを開始した。その目標は、証明の妥当性に一切の疑問を残さないため、HOL LightやIsabelleなどのテンプレート:訳語疑問点範囲プログラムにかけられるような形式的証明を構築することであった。プロジェクトは「Flyspeck」と名付けられた。そのうちの3文字、F、P、Kは「Formal Proof of Kepler」（ケプラーの形式的証明）から取ったものである。ヘイルズは完全な形式的証明を構築するのには20年ほどの作業が必要だと見積もっていた。2014年8月10日にプロジェクトの終結が発表された[15]。2015年1月、ヘイルズと21人の共同研究者は「ケプラー予想の形式的証明」と題された論文を公開した[16]。

関連する問題

テンプレート:仮リンクの定理（テンプレート:Lang-en-short）
平面に球を詰め込む最密配置は六方格子である。
2次元版のケプラー予想。証明は初等的である。ヘンクとジーグラーはこの功績を1773年のラグランジュに帰した[17]。
ハチの巣予想（テンプレート:Lang-en-short）
平面を等しい面積の区画に分けるとき、境界の長さが最小になるのは六方格子タイリングである。
証明はヘイルズによる[18]。トゥエの定理と関連性がある。
十二面体予想
等しい大きさの球による球充填から作られるボロノイ多面体の体積は、内接円半径が1である正十二面体の体積より小さくなることがない[19]。
ケプラー予想と関連する問題で、ヘイルズと同様の手法で証明された。マクローリンによる証明[20]は1999年のモーガン賞を受賞した。ラースロー・フェイェシュ＝トートが1950年に提示していた予想である。
ケルヴィン問題
3次元において、どのような構造のフォームがもっとも効率的（膜面積最小）か？ 100年以上にわたり、この問題の解はいわゆるケルヴィン構造だと予想されてきた。しかし、ウィア＝フェラン構造の発見[21]がこの予想を覆した。ケルヴィン予想への反証が発見されたという衝撃は、ヘイルズによるケプラー予想の証明が容易に受け入れられなかった理由の一つであった。
高次元における球充填
最適球充填の問題は1、2、3、8、24次元を除いて未解決である。8次元と24次元における証明は2016年にマリナ・ヴィヤゾフスカによって得られた[22]。
ウラムの充填予想
球よりも最適充填密度が低くなるような凸立体が存在するかどうかはまだ分かっていない。

関連項目

脚注

テンプレート:Reflist

参考文献

外部リンク

テンプレート:Normdaten

  1. ↑ 1.0 1.1 1.2 テンプレート:Cite journal
  2. ↑ テンプレート:Cite book
  3. ↑ ヨハネス・ケプラー （榎本恵美子・訳） 「新年の贈り物あるいは六角形の雪について」 『知の考古学』、第11号、1977年、276-296頁
  4. ↑ Sabine Kink (2022) The Explanations of Snow in the Taixi shuifa 泰西水法 (Hydromethods of the Great West, 1612) and Their Reception beyond the Ming–Qing Transition, Monumenta Serica, 70:1, 165-207, DOI: 10.1080/02549948.2022.2061159, p.186
  5. ↑ テンプレート:Cite journal
  6. ↑ テンプレート:Cite journal
  7. ↑ http://link.springer.com/article/10.1007%2FBF03024356#page-1
  8. ↑ テンプレート:Cite journal
  9. ↑ テンプレート:Cite journal
  10. ↑ テンプレート:Cite journal
  11. ↑ テンプレート:Cite journal
  12. ↑ "Fermat's Last Theorem" by Simon Singh. ISBN 978-0802713315
  13. ↑ テンプレート:Cite journal
  14. ↑ テンプレート:Cite journal
  15. ↑ https://code.google.com/p/flyspeck/wiki/AnnouncingCompletion
  16. ↑ http://arxiv.org/pdf/1501.02155.pdf
  17. ↑ テンプレート:Cite journal
  18. ↑ http://arxiv.org/pdf/math/9906042v2.pdf
  19. ↑ テンプレート:Cite journal
  20. ↑ http://de.arxiv.org/pdf/math/9811079.pdf
  21. ↑ テンプレート:Citation
  22. ↑ テンプレート:Citation
「https://ja.wiki.beta.math.wmflabs.org/w/index.php?title=ケプラー予想&oldid=2861」から取得