解法: ケプラー予想の形式的証明:HOL LightとIsabelleによるFlyspeckプロジェクト(2015年)

詰め込みとは、任意の二点の距離が少なくとも $2$ である単位球の中心からなる無限で離散的な集合 $V \subset \mathbb{R}^3$ である。その密度は、大きな容器の中で球が占める割合の極限として定義される。ケプラーの小冊子「六角形の雪片について」(1611年)は、この密度が $\Delta_3 = \pi/\sqrt{18} \approx 0.7405$ を決して超えないと予想した。この値は面心立方格子詰めと、同じ六角形の層から作られる無数の他の詰め込みによって達成される。トーマス・ヘイルズとサミュエル・ファーガソンは1998年に、幾何学的な場合分けと大規模な計算機計算を組み合わせてこの予想を証明したが、査読団を率いたジェフリー・ラガリアスが報告したように、その証明の性質は「人間が信頼性をもってすべての段階を確認することを困難にする」ものであり、2006年に完全な認証なしに出版された。

ヘイルズの対応は、2003年に発表されたFlyspeckプロジェクト(ケプラー予想の形式的証明)であった。これは、伝統的な数学的テキストと計算機計算として実装された部分の両方を含む論証のすべての部分を、HOL LightとIsabelleという証明支援系の中で再構築し、人間の査読者の代わりに、徹底的に精査された小さな論理的カーネルが各推論を検証できるようにするものである。プロジェクトは2014年に完了し、公式の報告はヘイルズと21名の共著者によって2017年に発表された。

この証明の概略の残りのステップは、論文自体の構成に従う:無限の幾何学的問題を有限個の組合せ論的場合に帰着させ(ステップ2–3)、各場合の数値的部分を純粋な算術によって証明できる不等式へと変換し(ステップ4–7)、証明済みの部分を最終的な形式的定理へと組み立てる(ステップ8)。