解法：开普勒猜想的形式化证明:HOL Light与Isabelle中的Flyspeck计划(2015年)

证明的文字部分——马尔沙尔胞腔分解、胞腔簇不等式,以及归约到驯顺平面图——在HOL Light中被形式化为一条单独的定理,它只需要把非线性不等式和驯顺分类当作黑箱事实使用,正如上面所展示的那样。把这条文字部分的定理,与已验证的非线性不等式(第6步)、已验证的线性规划(第5步)以及从Isabelle导入的驯顺分类(第3步)结合起来,就得到一个完整的形式化证明:$\mathbb{R}^3$ 中单位球的任何堆积都不能超过面心立方堆积的密度 $\pi/\sqrt{18} \approx 0.74$——这正是开普勒猜想。这条主定理可以从保存下来的证明项在一台普通的2 GHz机器上、大约四十分钟内重新跑一遍,任何读者都可以自行做这项独立的验证。