ケプラー予想のソースを表示

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

1998年に{{仮リンク|トーマス・C・ヘイルズ|en|Thomas Callister Hales}}は{{仮リンク|ラースロー・フェイェシュ＝トート|en|László Fejes Tóth}}が提案した方法<ref name =Tóth>{{cite journal|last1=Fejes Tóth | first1=L. | author1-link=László Fejes Tóth | title=Lagerungen in der Ebene, auf der Kugel und im Raum | publisher=[[Springer-Verlag]] | location=Berlin, New York | series=Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, Band LXV | mr=0057566 | year=1953 }}</ref>に従ってケプラー予想を証明したと発表した。多数のケース一つ一つを複雑なコンピュータシミュレーションでチェックする{{仮リンク|しらみつぶし法|en|proof by exhaustion}}であった。査読者は証明が正しいことを「99%確信している」と評した。よってケプラー予想は[[定理]]として受け入れられる寸前に来ている。2014年、ヘイルズに率いられたフライスペック・プロジェクト（{{Lang-en-short|the Flyspeck project}}）のチームは、定理証明支援ツールである{{仮リンク|Isabell|en| Isabelle (proof assistant)}}および{{仮リンク| HOL Light |en| HOL Light}}を組み合わせて用いることにより、ケプラー予想の形式的証明を完了したと発表した。

==背景==
[[Image:Closepacking.svg|thumb|立方最密充填（左）および六方最密充填（右）。]]
大きな容器を一定サイズの小球で一杯にしたとする。その配置の充填密度は球体積の総和を容器の容積で割ったもので与えられる。容器中の球の数を最大化することが、最大密度の配置を得ること、すなわち球をもっとも密に詰め込むことと等しい。

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

:<math>\frac{\pi}{3\sqrt{2}} = 0.740480489\ldots</math>

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

==発端==
[[Image:Kepler conjecture 2.jpg|thumb|''Strena Seu de Nive Sexangula''（新年の贈り物あるいは六角形の雪について）の図版。ケプラー予想を図解している。]]
ケプラー予想はヨハネス・ケプラーの論文『新年の贈り物あるいは六角形の雪について』<ref>{{cite book| | last1=Kepler | first1=Johannes | title=Strena seu de nive sexangula (The six-cornered snowflake)| url=http://www.thelatinlibrary.com/kepler/strena.html | year=1611|mr=0927925|isbn=978-1-58988-053-5 |laysummary=http://www.keplersdiscovery.com/SixCornered.html}}</ref><ref>ヨハネス・ケプラー （榎本恵美子・訳） 「新年の贈り物あるいは六角形の雪について」 『知の考古学』、第11号、1977年、276-296頁</ref>で初めて述べられた。ここでは、雪の星型の結晶の形状を説明する目的で言及されている。低温で水の粒子が凝縮し、最も密な配置をとるから、というのがその理由である。少し後のデカルトの『気象論』にも類似の言明がある。またイエズス会の宣教師を介して中国にも伝えられ、『[[天経或問]]』を通じて日本にも伝わり、幕末の土井利位『[[雪華図説]]』でも紹介されている<ref>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</ref>。

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

==19世紀==
ケプラー本人は予想を証明できなかったが、[[カール・フリードリヒ・ガウス|ガウス]]は球が規則配置を取る場合についてケプラー予想が正しいことを証明し<ref>{{Cite journal| last1=Gauss | first1=Carl F. | author1-link=Carl Friedrich Gauss | title=Untersuchungen über die Eigenschaften der positiven ternären quadratischen Formen von Ludwig August Seber | url=http://gdz.sub.uni-goettingen.de/dms/load/img/?IDDOC=267233 | year=1831 | journal=Göttingische gelehrte Anzeigen}}</ref>、問題の解明に一歩近づいた。

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

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

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

他方では、あらゆる可能な球配置の最大密度の[[順序集合#上界|上界]]を見つけようという試みがなされていた。イギリスの数学者クロード・アンブローズ・ロジャーズは一つの上界として約78%の値を得た<ref>{{Cite journal| last1=Rogers | first1=C. A. | title=The packing of equal spheres | doi=10.1112/plms/s3-8.4.609  | mr=0102052 | year=1958 | journal=[[Proceedings of the London Mathematical Society]]. Third Series | issn=0024-6115 | volume=8 | issue=4 | pages=609–620}}</ref>。それに続く数学者の努力によりこの値はわずかに引き下げられたが、立方最密充填の約74%には程遠かった。

1990年にウ＝イ・シアン（項武義）はケプラー予想を証明したと発表した。この成果は「[[エンサイクロペディア・ブリタニカ]]」および「[[サイエンス]]」誌で好意的に取り上げられ、シアンは[[アメリカ数学会|AMS]]-MAAジョイントミーティングに招待される栄誉を得た<ref>http://link.springer.com/article/10.1007%2FBF03024356#page-1</ref>。シアンの主張は幾何学的な手法でケプラー予想を証明したというものだった<ref>{{Cite journal | doi=10.1142/S0129167X93000364 | last1=Hsiang | first1=Wu-Yi | title=On the sphere packing problem and the proof of Kepler's conjecture | mr=1245351 | year=1993 | journal=International Journal of Mathematics | issn=0129-167X | volume=4 | issue=5 | pages=739–831}}</ref><ref>{{Cite journal|last1=Hsiang | first1=Wu-Yi | title=Least action principle of crystal formation of dense packing type and Kepler's conjecture | publisher=World Scientific Publishing Co. Inc. | location=River Edge, NJ | series=Nankai Tracts in Mathematics | isbn=978-981-02-4670-9 | mr=1962807 | year=2001 | volume=3}}</ref>。しかしながら、ガボル・フェイェシュ＝トート（ラースローの息子）は論文のレビューで「細部に目を向ければ、重要な言明の多くが容認できるような証明を欠いている」と述べた。ヘイルズはシアンの仕事を詳細に批判し<ref>{{Cite journal | last1=Hales | first1=Thomas C. | title=The status of the Kepler conjecture | doi=10.1007/BF03024356 | mr=1281754 | year=1994 | journal=[[The Mathematical Intelligencer]] | issn=0343-6993 | volume=16 | issue=3 | pages=47–58}}</ref>、シアンはこれに反論した<ref>{{Cite journal | last1=Hsiang | first1=Wu-Yi | title=A rejoinder to T. C. Hales's article: ``The status of the Kepler conjecture''  | doi=10.1007/BF03024716 | mr=1319992 | year=1995 | journal=[[The Mathematical Intelligencer]] | issn=0343-6993 | volume=17 | issue=1 | pages=35–42}}</ref>。現在ではシアンの証明は不完全なものだったと認められている<ref>"Fermat's Last Theorem" by Simon Singh. ISBN 978-0802713315</ref>。

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

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

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

2005年、ヘイルズは100ページの論文で、証明の中でコンピュータを用いない部分を詳述した<ref>{{Cite journal | doi=10.4007/annals.2005.162.1065 | last1=Hales | first1=Thomas C. | title=A proof of the Kepler conjecture | url=http://annals.princeton.edu/annals/2005/162-3/p01.xhtml | mr=2179728 | year=2005 | journal=[[Annals of Mathematics|Annals of Mathematics. Second Series]] | issn=0003-486X | volume=162 | issue=3 | pages=1065–1185}}</ref>。ファーガソンとの共著による2006年の論文および数篇の続報ではコンピュータによる部分を報告した<ref>{{Cite journal | last1=Hales | first1=Thomas C. | last2=Ferguson | first2=Samuel P. | title=A formulation of the Kepler conjecture | doi=10.1007/s00454-005-1211-1 | mr=2229658 | year=2006 | journal=[[Discrete & Computational Geometry]] | issn=0179-5376 | volume=36 | issue=1 | pages=21–69}}</ref>。2009年にヘイルズとファーガソンは離散数学の分野の優れた論文に対して贈られる[[ファルカーソン賞]]を受賞した。

===形式的証明===
2003年1月、ヘイルズはケプラー予想の完全な形式的証明を求める共同プロジェクトを開始した。その目標は、証明の妥当性に一切の疑問を残さないため、HOL LightやIsabelleなどの{{訳語疑問点範囲|{{仮リンク|自動証明検証|en| automated proof checking }}|date=2016年4月}}プログラムにかけられるような形式的証明を構築することであった。プロジェクトは「Flyspeck」と名付けられた。そのうちの3文字、F、P、Kは「Formal Proof of Kepler」（ケプラーの形式的証明）から取ったものである。ヘイルズは完全な形式的証明を構築するのには20年ほどの作業が必要だと見積もっていた。2014年8月10日にプロジェクトの終結が発表された<ref>https://code.google.com/p/flyspeck/wiki/AnnouncingCompletion</ref>。2015年1月、ヘイルズと21人の共同研究者は「ケプラー予想の形式的証明」と題された論文を公開した<ref>http://arxiv.org/pdf/1501.02155.pdf</ref>。

==関連する問題==
;{{仮リンク|トゥエ|en| Axel Thue}}の定理（{{lang-en-short|Thue's theorum}}）:平面に球を詰め込む最密配置は六方格子である。
:2次元版のケプラー予想。証明は初等的である。ヘンクとジーグラーはこの功績を1773年の[[ジョゼフ＝ルイ・ラグランジュ|ラグランジュ]]に帰した<ref>{{Cite journal | last1=Henk | first1=Martin | last2=Ziegler | first2=Guenther | title=La congettura di Keplero|series=La matematica. Problemi e teoremi|volume=2|publisher=Einaudi|location=Torino|year=2008}}</ref>。

;[[ハニカム構造|ハチの巣予想]]（{{lang-en-short|honeycomb conjecture}}）:平面を等しい面積の区画に分けるとき、境界の長さが最小になるのは六方格子[[タイリング]]である。
:証明はヘイルズによる<ref>http://arxiv.org/pdf/math/9906042v2.pdf</ref>。トゥエの定理と関連性がある。

;十二面体予想:等しい大きさの球による球充填から作られる[[ボロノイ図|ボロノイ]]多面体の体積は、内接円半径が1である[[正十二面体]]の体積より小さくなることがない<ref>{{Cite journal | last1=Hales | first1=Thomas C. | last2=MacLaughin | first2=Sean | title=The dodecahedral conjecture | journal=[[Journal of the American Mathematical Society]] | volume=23 | issue=2 | pages=299–344|year=2010 | doi=10.1090/S0894-0347-09-00647-X | arxiv=math.MG/9811079}}</ref>。
:ケプラー予想と関連する問題で、ヘイルズと同様の手法で証明された。マクローリンによる証明<ref>http://de.arxiv.org/pdf/math/9811079.pdf</ref>は1999年の[[:en:Morgan Prize|モーガン賞]]を受賞した。ラースロー・フェイェシュ＝トートが1950年に提示していた予想である。

; ケルヴィン問題 : 3次元において、どのような構造の[[フォーム]]がもっとも効率的（膜面積最小）か？ 100年以上にわたり、この問題の解はいわゆるケルヴィン構造だと予想されてきた。しかし、[[ウィア＝フェラン構造]]の発見<ref>{{citation|last1=Weaire|first1=D.|author1-link=Denis Weaire|last2=Phelan|first2=R.|title=A counter-example to Kelvin's conjecture on minimal surfaces|journal=Phil. Mag. Lett.|volume=69|pages=107–110|year=1994|doi=10.1080/09500839408241577}}</ref>がこの予想を覆した。ケルヴィン予想への反証が発見されたという衝撃は、ヘイルズによるケプラー予想の証明が容易に受け入れられなかった理由の一つであった。

; 高次元における[[球充填]]:最適球充填の問題は1、2、3、8、24次元を除いて未解決である。8次元と24次元における証明は2016年に[[マリナ・ヴィヤゾフスカ]]によって得られた<ref>{{citation|last1=Klarreich|first1=Erica|authorlink1=Erica Klarreich|title=Sphere Packing Solved in Higher Dimensions|url=https://www.quantamagazine.org/20160330-sphere-packing-solved-in-higher-dimensions|magazine=Quanta Magazine|date=March 30, 2016}}</ref>。

;ウラムの充填予想: 球よりも最適充填密度が低くなるような凸立体が存在するかどうかはまだ分かっていない。

==関連項目==
* [[球充填]]
* [[空間充填]]
* [[平面充填]]
* [[接吻数問題]]
* [[ボロノイ図]]
* [[格子 (数学)]]
* [[四色問題]]

==脚注==
{{Reflist}}

==参考文献==
*{{Citation | last1=Aste | first1=Tomaso | last2=Weaire | first2=Denis | title=The pursuit of perfect packing | publisher=IOP Publishing Ltd. | location=Bristol | isbn=978-0-7503-0648-5 | mr=1786410 | year=2000}}
*{{Citation | last1=Hales | first1=Thomas C. | title=Cannonballs and honeycombs | url=http://www.ams.org/notices/200004/ | mr=1745624 | year=2000 | journal=[[Notices of the American Mathematical Society]] | issn=0002-9920 | volume=47 | issue=4 | pages=440–449}} An elementary exposition of the proof of the Kepler conjecture.
*{{Citation | last1=Hales | first1=Thomas C. | last2=Ferguson | first2=Samuel P. | title=The Kepler Conjecture: The Hales-Ferguson Proof | publisher=Springer | location=New York | isbn=978-1-4614-1128-4 | year=2011}}
*{{Citation | last1=Marchal | first1=Christian | title=Study of Kepler's conjecture: the problem of the closest packing | journal=[[Mathematische Zeitschrift]] | volume=267 | pages=737–765|year=2011 | doi=10.1007/s00209-009-0644-2}}
*{{Citation | last1=Szpiro | first1=George G. | title=Kepler's conjecture | publisher=[[John Wiley & Sons]] | location=New York | isbn=978-0-471-08601-7 | mr=2133723 | year=2003}}
*{{Citation | last1=スピーロ| first1=ジョージ・G| title=ケプラー予想| publisher=[[新潮社]] |other=青木 薫（訳）| isbn=4105454013 | year=2005}}
* ジョージ・G.スピーロ, 青木薫(訳)：「ケプラー予想: 四百年の難問が解けるまで」、新潮社 (新潮文庫）、ISBN 978-4102184714（2013年12月24日）。
*ヨハネス・ケプラー （榎本恵美子・訳） 「新年の贈り物あるいは六角形の雪について」 『知の考古学』、第11号、1977年、276-296頁

==外部リンク==
*{{MathWorld | urlname = KeplerConjecture | title = Kepler Conjecture}}
* [http://www.its.caltech.edu/~atomic/snowcrystals/earlyobs/kepler2.gif 『六角の雪片について』表紙（英語）]
* [https://sites.google.com/site/thalespitt/ トーマス・ヘイルズのサイト（英語）]
* [https://code.google.com/p/flyspeck/ フライスペック・プロジェクトのサイト（英語）]
* [http://www.math.pitt.edu/articles/cannonOverview.html ヘイルズの証明の概要（英語）]
* [http://www.americanscientist.org/issues/id.556,y.0,no.,content.true,page.1,css.print/issue.aspx Dana MackenzieによるAmerican Scientist誌の記事（英語）]
* [http://afp.sourceforge.net/entries/Flyspeck-Tame.shtml Flyspeck I: Tame Graphs]:トーマス・C・ヘイルズがケプラー予想の証明の中で定義した平面{{訳語疑問点範囲|馴グラフ|date=2016年4月}}の検証済み目録（英語）

{{Normdaten}}
{{デフォルトソート:けふらあよそう}}
[[Category:離散幾何学]]
[[Category:証明された予想]]
[[Category:ヨハネス・ケプラー]]
[[Category:数学のエポニム]]
[[Category:数学に関する記事]]
[[Category:ヒルベルトの23の問題]]