19/11/29 13:53:37 CoYajOLi.net
>>206
４色問題とかケプラー予想もあったかな（＾＾；
URLﾘﾝｸ(ja.wikipedia.org)
(抜粋)
ケプラー予想（ケプラーよそう、英: Kepler conjecture ）とは、17世紀の数学者・天文学者ヨハネス・ケプラーに由来する、三次元ユークリッド空間における球充填に関する数学的な予想である。
それによると、等しい大きさの球で空間を充填（パッキング）するとき、平均密度が立方最密充填配置（面心立方）ならびに六方最密充填配置を越えることはない。これらの配置の密度はおよそ74.05%である。
1998年にトーマス・C・ヘイルズ（英語版）はラースロー・フェイェシュ＝トート（英語版）が提案した方法[1]に従ってケプラー予想を証明したと発表した。
多数のケース一つ一つを複雑なコンピュータシミュレーションでチェックするしらみつぶし法（英語版）であった。
査読者は証明が正しいことを「99%確信している」と評した。
よってケプラー予想は定理として受け入れられる寸前に来ている。
2014年、ヘイルズに率いられたフライスペック・プロジェクト（英: the Flyspeck project）のチームは、定理証明支援ツールであるIsabell（英語版）およびHOL Light （英語版）を組み合わせて用いることにより、
ケプラー予想の形式的証明を完了したと発表した。