解法: ケプラー予想の形式的証明:HOL LightとIsabelleによるFlyspeckプロジェクト(2015年)
ざっくり言うと
幾何学に現れるいくつかの量(角度の二乗や、複数の長さに非線形に依存する体積など)は、コンピューターが直接扱うには扱いにくいため、ヘイルズは厄介な式それぞれに一時的な名前を与え、その式が満たすべき限界だけを記憶する——ちょうど「今どれだけ速く動いているかの二乗」を新しい変数「あなたの運動エネルギー」に置き換えて、毎回二乗を計算し直す代わりにその範囲だけを追跡するのと同じである。
詳しい解説
それぞれの枡状平面グラフについて、反証的な詰め込みの幾何学は、二面角、体積、マルシャル胞体のスコアに関する不等式系——その大半は非線形である——を要求する。ヘイルズはそれぞれの非線形な部分式に新しい変数を導入することで、この系を線形なものへと緩和する。上の例で言えば、非線形な事実 と は、 を独立な変数とみなし で制約すれば線形な系になる。得られた線形系が実行不可能であれば、元の非線形系も実行不可能でなければならず、その枡状グラフは反例の候補から除外される。
- 線形計画緩和
- いくつかの非線形な式を新しい独立変数として扱うことによって得られる、より緩く純粋に線形な系で、難しい方程式や不等式の系を置き換えること。元の系のどんな解も緩和された系の解でもあるので、緩和された系がすでに解を持たなければ、元の系も解を持たない。