解法: ケプラー予想の形式的証明:HOL LightとIsabelleによるFlyspeckプロジェクト(2015年)
ざっくり言うと
最後の一手は帳簿合わせである:伝統的な数学的論証は、「もし枡状グラフの一覧が完全であり、これらの不等式がすべて成り立つならば、ケプラー予想が従う」という一つの定理として形式化されている。したがって、別々に検証された三つの計算機による結果を差し込むこと——設計図がすでに検証された機械に最後の三つの部品を組み込むようなもの——によって証明が完成する。
詳しい解説
証明のテキスト部分——マルシャル胞体分割、胞体クラスター不等式、そして枡状平面グラフへの帰着——は、非線形不等式と枡状分類をブラックボックスの事実としてのみ必要とする、上に示した形のただ一つの定理としてHOL Light内で形式化されている。このテキスト部分の定理を、検証済みの非線形不等式(ステップ6)、検証済みの線形計画(ステップ5)、そしてIsabelleから取り込まれた枡状分類(ステップ3)と組み合わせると、 内の単位球のいかなる詰め込みも面心立方格子詰めの密度 を超えられないという、完全な形式的証明——すなわちケプラー予想——が得られる。この主定理は、保存された証明項から、ごく普通の2GHzマシン上でおよそ四十分で再実行でき、読者は誰でもこの独立した検証を自分で行うことができる。