300年以上の歴史を持つ未解決問題であったケプラー予想がついに完全解決したようです.
この記事ではケプラー予想がどのような問題であるかの説明と解決までの歴史をまとめています.
ケプラー予想とは
ケプラー予想とは「3次元空間の中に同じ大きさの球を充填するときに最も密度が大きくなるような並べ方は六方最密充填である」という予想です.
六方最密充填と急に言われてもピンとこないかもしれませんが,別に複雑なものではありません.
次の図のような詰め方です.
つまり,球を3個くっつけて置いて,その上にできたくぼみに球を置いていくという詰め方です.
高校の化学の結晶構造の話で出てくるので覚えている人も多いかもしれません.
六方最密充填は確かに隙間が少ない詰め方のように見えますが,これよりもうまく詰めるのが無理かと言われるとなんとも言えない気分になりませんか.
これは素人だから分からないというようなものでは無く,数学者にとっても非常に難しいものでした.ケプラー予想の内容自体は単純で,数学の知識が無くても理解できます.
しかし,正しいと証明されるには300年以上もかかったのです.
ちなみに,このケプラー予想のケプラーとは,天体の運動に関するケプラーの法則等で知られているあの有名なヨハネス・ケプラーのことです.ケプラーが1611年の論文『六角の雪片について』でこの予想を提示したことに由来しています.
数年前に既に解かれている？
この記事のタイトルに「完全解決」と書きましたが,人によっては「ケプラー予想は何年か前にすでに解かれていたはず」と思う人もいるかもしれません.
実際,「ケプラー予想」とgoogleで検索をかけると次の記事がすぐに出てきます.
400年の難問、「ケプラー予想の証明」やっと100％終わる | ギズモード・ジャパン
これは2014年の記事です.他にも1998年に解決というようなものも見つけられます.これらはどれも嘘を言っているわけでは無く,それぞれ違う事柄を「解決」と表現しているのです.
以下では,この様々な「解決」を整理しながらケプラー予想の歴史を見ていきます.
1998年 第1の解決
1998年に,当時ミシガン大学に在籍していたThomas Halesとその学生であるSamuel Fergusonがケプラー予想の解決を宣言します.これが最初の「解決」です.
ただ,当たり前のことですが本人が「できた」というだけでは本当に解決したかはわかりません.
権威ある雑誌の査読をクリアし,出版されて初めて万人の認めうる解決といえるでしょう.
しかし,このときにはこの「査読」が問題になったのです.何故なら彼らの方法は,六方最密充填よりも密度が高くなるかもしれない充填法を現実的な数まで絞り込み,あとは片っ端から計算機を用いて調べるというものだったからです.「現実的な数」と言いましたが人間の手では到底不可能な量です.
当然論文には膨大な長さのプログラムが記されています.
雑誌の方としては正しいとすれば偉大な結果なわけですから是非掲載したいと思う訳ですが,このプログラム部分の査読は非常に難航し,査読チームが結成され精力的に検討されたようですが,結局は完了しませんでした.
しかし,査読者が読む限りでは「本質的にこのアプローチはすべての場合で上手くいっている」と強く感じさせるものであったようで,査読が完全では無いものの最終的に論文は出版されることとなりました.2006年の事です.
2014年 第2の解決
2003年に上記の論文の執筆者の1人であるThomas Halesは”Flyspeck”なるプロジェクトの開始を宣言します.
このプロジェクトはケプラー予想の証明を計算機で検証可能な形式的証明に書き換えるというものです.計算機による証明検証は非常に信頼性の高いものなので確かにこれが実現すればこの証明の信頼性はグンと上がることになります.
当然,膨大な作業量が必要となる訳ですが,無事にこの作業は完遂され,2014年にプロジェクトの完了が宣言されました.これをもって「解決」と報じている記事が多いようです.
2017年 第3の解決
2017年5月に Cambridge University Pressの”Forum of Mathematics, Pi”にThomas Halesらによる論文“A FORMAL PROOF OF THE KEPLER CONJECTURE“が掲載されています.この雑誌はオープンアクセスなので無料でWeb上から見られます.
この論文は学術誌に掲載するというオフィシャルな形で”Flyspeck”の完了を報告をするのを目的としたもので,特に技術的な詳細が書かれているわけでは無いのですが,形式証明の完了に至るまでの道筋が簡略にまとめられています.そういう意味で本質的には2014年で解決済みともいえるのですが,オフィシャルな発表という意味でこれも「解決」といってよいと思っています.
リンク
A FORMAL PROOF OF THE KEPLER CONJECTURE | Forum of Mathematics, Pi | Cambridge Core
文章中で言及した論文です.文中の査読者のコメントはこの論文のイントロから引用しました.