解法: ケプラー予想の形式的証明:HOL LightとIsabelleによるFlyspeckプロジェクト(2015年)
ざっくり言うと
限られた形の族しか起こり得ないため、コンピューターは単に可能なすべての形を描いてみて、枡状の規則をすでに破っている構築途中の形はすぐに捨てればよい——ちょうど、合わないピースを試した瞬間に却下してジグソーパズルを解くようなものである。出力は有限のグラフのギャラリーであり、難しい数学的主張は、このギャラリーが完全である——何一つ欠けていない——ということである。
計算機による探索が、枡状条件を満たすすべての有限平面グラフを列挙し、決して枡状になり得ない枝を刈り込む。得られた一覧——当初は を超えるグラフであったが、形式化のために枡状の定義がより厳密にされた後は に絞り込まれた——は完全であることが証明される。すなわち、あらゆる枡状平面グラフはこの一覧のいずれかと同型である。この完全性定理はIsabelle/HOLの中で形式化され(この列挙は 個程度の中間グラフを探索する)、その後、人手で翻訳された仮定としてHOL Lightに取り込まれた。この命題に現れるすべての量化子は有界な有限構造の上を走るため、この命題は命題論理の充足可能性(SAT)の主張と同値であり、どちらの論理体系でも同じように証明可能である。これが、この結果を二つの証明支援系の間で移すことを正当化する理由である。
- 同型なグラフ
- 二つのグラフが同型であるとは、一方の頂点に別の名前を付け直すことで、紙の上では違う描き方をしていても、頂点・辺・つながり方がすべて他方と全く同じに見えるようにできることをいう。