400年をかけたケプラー予想の解決は、コンピューターの力も証明した

写真拡大

一見馬鹿げているように思えるかもしれないが、数学者たちは4世紀も苦闘してきた。コンピューターによる証明で、ついにその「予想」が正しいと確認されたのが今年の8月のことだった。

「400年をかけたケプラー予想の解決は、コンピューターの力も証明した」の写真・リンク付きの記事はこちら

球体をうまく積み上げるのに、最も適しているのはどのような“幾何学的図形”なのだろうか?

1611年、ヨハネス・ケプラー(近代天文学の創始者のひとりとされる)は、果物屋で自然発生的に用いられている、オレンジの山のようなピラミッド型だと仮説を立てた。しかし彼は、この直観を証明できなかったため、「球体の最も密度の高い詰め方」について問うケプラー予想が生まれた。現代数学の父、ダフィット・ヒルベルトが1900年に提示した「ヒルベルトの23の問題」の18番目となったほどに重要なものだ。

それからさらに約1世紀が経ち、ペンシルバニア州ピッツバーグ大学のトーマス・ヘイルズはようやく予想を証明した。16世紀末にまでさかのぼる問題──イギリスのウォルター・ローリー卿が山積みした大砲の弾の数を計算するための公式の探求を始め、それから数年後にケプラーが、球体同士の隙間が最小になるように積み重ねるための最良のかたちがどんなものかを解明しようと試みた課題だ。

証明された結果によると、ピラミッド型は74%の効率をもつことが判明した。また、例えば立方体構造よりも22%効率がいい。しかし、これが絶対的に最良の配列なのだろうか?

六角形のグリッドに従って配列した球体をもとにした詰め方も、例えば、約74%の効率に達する。トーマス・ヘイルズは、ケプラー予想を証明するために(もしくは誤りを証明するために)、何年も研究を行った。そしていま、それに成功したというわけだ。

TAG

GeometryMathematicsResearchWIRED IT

16世紀のドイツの天文学者ケプラー。球を敷き詰めたときに、最も密な構造になると予想した。これが「ケプラー予想」だ。image from Wikimedia

このアメリカの数学者、トーマス・ヘイルズは、1998年からこの問題と戦っている。当時彼は、ソフトウェアを用いて何千もの球体の配列(それだけで数学的に可能な無限の組み合わせを代表する)を評価するという、予想に対する最初の挑戦を発表した。

彼の300ページの研究を証明するには、12人の査読者が4年の歳月をかける必要があった。2005年に出された雑誌「Annals of Mathematics」への掲載の後も、査読者たちは「99%正しい」以上は踏み込まなかった。

03年、ヘイルズは自身の証明が完全に検証されるべく、「Flyspeck」プロジェクトを立ち上げた。11年後、「Isabelle」と「HOL Light」の2つのソフトウェア(論理的展開が連続するなか発生しうる誤りを見つけ出す役割が与えられた)が、ポジティヴな結果を出した。ヘイルズの証明に間違いはなく、ケプラー予想は正しかった。そして、果物屋は抜け目なかったという結果だ。

このニュースには、2つの重要な意味がある。1つ目は、ケプラーの仮説の正しさが、コンピューターにおけるよりよいデータの配列をもたらすことができるだろうということだ。データをコード化したりやコミュニケーションをとったりする際に、より高い効率を得られる。

2つ目は、難しい数学の証明の論理的正確さを検証する、ソフトウェアに関するものだ。この成功は、ソフトウェアの応用を拡大し、改良を行って、より使いやすくなるようにするように科学者たちを促すことができるだろう。

ヘイルズは、何年も後でようやく、彼の成功を喜んでいる。「巨大な重荷が突然私の方から取り除かれました。10歳若くなった気がします!」。

TAG

GeometryMathematicsResearchWIRED IT