＼閲覧ありがとうございます！当サイトではリンク広告を利用しています／
難問だったことで有名な「フェルマーの最終定理」よりも未解決の時間が長かった数学の問題として「ケプラー予想」がある。球体を空間に充填するときにはどのような方法が一番効率が良いのかという疑問から発した予想である。
2次元の場合は純粋に論考で証明されたが、3次元の場合は最終的にはコンピュータによって証明が得られた。
1590末：ハリオット、砲弾の効率の良い積み方から最密充填を着想・・・ ウォルター・ローリーから砲弾の積むとき個数を知る数式を作ってくれと頼まれてこの予想をした。 つまり効率よく積んでくれるように頼まれた。というのも、当時砲弾を船で運ぶ時に、効率よく積んだ方が速く多く運べるからである。
1600初頭：ハリオット、ケプラーへの手紙の中でこの予想にふれる。
1611：ケプラー、「6角形の雪について」を出版。ケプラー予想の提起が書物として出る。
1831：ガウス、格子充填における3次元での解決・・・整ったかたちの充填では、面心立方充填が一番効率がよい。
1919：ブリックフェルト、密度が84.3％より高くはならないと証明・・・ここから、上限を下げる試みがつづく。ようは、上の限界値を下げていって、 面心立方充填 の密度と一致すれば証明したことになる、という寸法である。
1938：カーシュナー、2次元でのランダムな充填も含んだ場合の証明・・・2次元平面に円を並べるとき、でたらめな配置を許した場合も、面心立方充填が効率がよい。
1940年代：コンピュータの発展。シンプレックスアルゴリズムの発展・・・制約条件に合うようにグラフを書いていき、それらの制約をすべて満たす範囲での最大値を見つける、という方法。
1958：ロジャーズの証明により、上限が77.98％にまで下がる。
1990：シアン、論考により証明できたと主張・・・これは曖昧な表現で土間化しているところが多く、間違っていた。数学者からも相手にされなかった。
1990代：ヘイルズ、コンピュータで シンプレックスアルゴリズム をつかい証明する方針を考える。
1998：ヘイルズ、ファーガソンとともにコンピュータを使って3次元でのランダムな配置を含めての証明、ケプラー予想の解決
・ケプラーは雪の結晶についての小冊子の中でこの予想にふれている。
・コンピュータによる証明は多少波紋を呼んだが、四色問題「の証明の影響もありそこまでひどくはなかった。
・コンピュータによる証明は従来の「エレガントな証明」にたいして「エレファントな証明」などといわれた。
・コンピュータによる証明
コンピュータによる証明は、4色問題同様ハレーションはあったが、先輩格の4色問題によって、救われた感じはある。また、性能が格段に発展していたのも助けになったといえるだろう。4色問題はしらみつぶしに近い形で証明されたが、ケプラー予想はシンプレックスアルゴリズムによって証明されたという点で多少異なる。
・400年かかった証明
ケプラー予想が証明されたことで、中世くらいから続くような数学の未解決問題はあるいみ失われたといえるかもしれない。フェルマーの最終定理も、ケプラー予想の直前くらいに証明されている。この後の時代は、近代に入ってからの難問が未解決問題として挑戦を受けることになるといえる。
・今後もコンピュータによる証明はでてくるか
幾何学に関する問題のうち、離散数学に関する問題は、コンピュータによって証明されるものもつぎつぎに出てくるかもしれない。4色問題やケプラー予想よりはマイナーであることは間違いない。またコンピュータも進歩しているので、その証明に対する波紋もほぼ怒らないと予想される。