知识/定理
黑尔斯团队（2017）完成开普勒猜想的机器形式化验证（Flyspeck 项目）——计算机证明获终极核验。
公式
球最密堆积密度 $\le\frac{\pi}{\sqrt{18}}$；Flyspeck：HOL Light 中核验全部证明。
证明思路
把 Hales 1998 的计算机辅助证明改写为定理证明器可核验的「形式证明」。
应用/例子
形式化验证的「登月工程」；证明可信度的新标准。
意义/影响
「计算机证明可信吗」问题的里程碑回答——可形式化即可信。
DOXA · 数学编年史 · 知识详情
2017 ｜ 黑尔斯团队 ｜ 离散·组合 ｜ 突破
黑尔斯团队（2017）完成开普勒猜想的机器形式化验证（Flyspeck 项目）——计算机证明获终极核验。
球最密堆积密度 $\le\frac{\pi}{\sqrt{18}}$；Flyspeck：HOL Light 中核验全部证明。
把 Hales 1998 的计算机辅助证明改写为定理证明器可核验的「形式证明」。
形式化验证的「登月工程」；证明可信度的新标准。
「计算机证明可信吗」问题的里程碑回答——可形式化即可信。