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

残る要素は、二面角と体積に関する、線形化できないほぼ $1000$ 個の不等式からなる一つの論理積である。素朴な区間演算——定義域を細分し、各断片上で関数を評価する方法——は形式的には健全だが、これらの多変数不等式に対しては遅すぎる。その代わりに、それぞれの不等式は検証済みの二次テイラー区間拡張を用いて評価される。定義域内の一点 $y$ を固定すると、上記の式は、その箱全体における $g(y)$、$g'(y)$、$g''$ の限界を、箱の中のすべての $x$ に対する $g(x)$ の検証済みの包含域へと変換し、はるかに精密でありながら完全に厳密な限界を与える。これは計算機が生成する三つの要素のうち最も計算量の大きいものであり、論文によれば三つの部分問題のうち最も難しいものの検証には $5000$ CPU時間程度を要するという。