ケプラー予想をわかりやすく解説！〜スイカを一番ぎっしり詰める方法〜

こんにちは、kenjiです！

今日は「ケプラー予想」っていう、ちょっと難しそうな名前の数学の話を、できるだけわかりやすく説明してみたいと思います。

一見、めちゃくちゃマニアックな話なんですが、「スイカを箱にぎっしり詰めるにはどうしたらいいか？」という、わりと身近な問題でもあるんですよね。コンビニの冷蔵庫にも関係があるし、荷物の積み方にも関係ある。

そして、数学の世界では、これがなんと400年以上も証明できなかったという、超・ロマンある話でもあります。

ではいってみましょう！

そもそもケプラーって誰？

まず、「ケプラー予想」の「ケプラー」って誰？という話なんですが。

これは、ヨハネス・ケプラー（Johannes Kepler） というドイツの天文学者・数学者の名前です。

この人、めちゃくちゃすごい人でして。たとえば、惑星の軌道が楕円（だえん）になっているってことを発見したのもこの人。今では当たり前の知識ですが、当時（1600年頃）は地動説すらちゃんと信じられてなかった時代なんですよ。

みたいな位置づけで、ケプラーは「数式で宇宙を語る」っていう先駆者でした。

で、そんな彼が、ある時こう言い出します。

「ケプラー予想」とは、簡単にいうと、こういう話です。

同じ大きさの球（スイカやオレンジ）を箱に詰めるとき、どの並べ方が一番ぎっしり詰められるのか？

っていう問題。

で、ケプラーが1600年代に予想したのが

オレンジを八百屋で並べるみたいに、三角形っぽく積むのが一番効率いいんじゃない？

ってこと。

これを数学っぽくいうと、「最密充填問題（さいみつじゅうてんもんだい）」といって、球を空間に一番密に敷き詰める方法を探す問題なんですね。

ケプラーは、「面心立方構造（FCC）」っていう並べ方（スイカを三角形に積むような感じ）が一番効率がいいと予想しました。

で、これ、みんな「たしかにそれっぽいね〜」とは思ってたんですが、数学的に「絶対にこれが一番だ！」って証明するのがめちゃくちゃ難しかったんです。

じゃあ、実際にそれが証明されたのはいつかというと…

なんと1998年〜2005年ごろです。つまり、400年近くも誰も証明できなかったんですね。やばすぎる。

しかも、証明したのはアメリカの数学者トーマス・ヘイルズ（Thomas Hales） という人。

この人、手計算だけじゃ無理と判断して、コンピューターを使って証明しました。ただ、その証明があまりに複雑すぎて、人間がちゃんとチェックできない！という問題が発生。

そこで、数学の世界でも「じゃあ、コンピューターで証明したのって本当に信用できるの？」という大論争が起きました。

結局、「コンピューターを含めて厳密に検証したよ！」という証明（正式には「形式化証明」といいます）が完了したのは2014年。

つまり、ケプラーの直感が正しかったと証明されるまで、400年以上かかったというわけです。すごいロマン。

「球をどうやって並べるか」なんて、数学オタクだけの話かと思いきや、実は超実用的です。

などなど、実は僕たちの生活の裏にゴリゴリ使われてる理論です。

というわけで、まとめます。

そしてなにより面白いのは、 「八百屋さんが感覚でやってた積み方が、数学的にも最強だった」 という点。

つまり、人間の直感ってすごい。そして、それを証明するのに400年かかることもあるっていうのが、なんともロマンのある話ですよね。

興味を持った方は、ぜひ「トーマス・ヘイルズ」「形式化証明」「Sphere Packing」なんかで調べてみてください。深掘りするとめちゃくちゃ面白いです。

ではでは！

[PR]