解法: ケプラー予想の形式的証明:HOL LightとIsabelleによるFlyspeckプロジェクト(2015年)
ざっくり言うと
一つの球の近傍にさらにズームインし、近くにある球ごとに点を打ち、二つの隣人が接するか近い場合には線を引く。この略図は、その球の周りの球面上に描かれた小さなグラフであり、平面に広げることができる。ヘイルズは、ある詰め込みが反例に必要とされるほど密であれば、この小さなグラフはごく限られた形のうちの一つにしかなり得ず——決して無秩序に不規則にはならない——ことを示し、これによってコンピューターが場合分けの検証を引き継げるようになる。
詳しい解説
コンパクト性により、ヘイルズは局所環状不等式に対する反例 が「反証的(contravening)」と呼ばれる特別な極値的な形を持つと仮定できる。反証的な についての詳細な幾何学的研究(「主要評価」)により、その近傍にある球の組合せ論的パターンが、頂点の次数と面の大きさに関する厳しい条件からなる短いリストを満たす平面グラフ を常に作ることが示される。このようなグラフを枡状(tame)と呼ぶ。あらゆる反例の可能性は、このようにして一つの具体的な枡状平面グラフに対応付けられ、球の位置に関する解析的な問題が、グラフに関する有限な組合せ論的分類問題に置き換わる。
- 枡状平面グラフ
- 平面グラフ——頂点と辺が平らな面の上で交差せずに描かれたもの——は、各頂点に集まる辺の本数と各面の辺の数に関する短く正確な制限のリストを満たすとき、枡状(tame)と呼ばれる。