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

形式化后的主定理指出:对任意堆积 $V$,存在一个常数 $c$,使得对任意半径 $r \ge 1$,半径为 $r$ 的容器内球心的数目满足 $\mathrm{CARD}(V \cap B(0,r)) \le \pi r^3/\sqrt{18} + c\,r^2$;令 $r \to \infty$ 便得到开普勒经典形式的密度界。由于证明脚本以可重放的格式保存,任何拥有普通计算机的读者都可以在大约四十分钟内重新运行整个主定理的HOL Light验证,这是一种独立的核验,只需要信任证明助手已公开的那个小内核,而不必信任其背后成千上万页的情形分析。

Flyspeck 的规模——作者们将其形容为可与Feit–Thompson奇阶定理、经过验证的C编译器CompCert以及经过验证的微内核seL4相媲美——帮助确立了完全形式化验证即便对于最困难的经典未解难题也是一个现实可行的选择,而不仅仅适用于软件的某些部分;它还留下了可复用的HOL Light实分析与复分析函数库,供后来的形式化项目在此基础上继续构建。