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

堆积是由单位球球心组成的一个无限离散集合 $V \subset \mathbb{R}^3$,其中任意两点的距离都至少为 $2$;它的密度是球在一个大容器中所占比例的极限。开普勒的小册子《论六角雪花》(1611年)猜想这一密度永远不会超过 $\Delta_3 = \pi/\sqrt{18} \approx 0.7405$,该值由面心立方堆积以及由同样的六边形层构造出的无数其他堆积所达到。托马斯·黑尔斯与塞缪尔·弗格森于1998年通过几何情形分析结合大量计算机计算证明了这一猜想,但正如主持审稿小组的杰弗里·拉加里亚斯所说,这个证明的性质“使人类难以可靠地核对每一步”,它在2006年发表时并未获得完全的核实。

黑尔斯的应对之策,即2003年公布的Flyspeck计划(开普勒猜想的形式化证明):在HOL Light与Isabelle两个证明助手内部,重新构造论证的每一部分——既包括传统的数学文字部分,也包括以计算机计算形式实现的部分——使得一个经过严格审查的小型逻辑内核来检验每一步推理,而不是依赖人工审稿人。该计划于2014年完成,黑尔斯与二十一位合著者于2017年发表了官方报告。

本证明梗概接下来的步骤遵循论文自身的框架:把无限的几何问题归约为有限多个组合情形(第2–3步),把每个情形的数值部分转化为可用纯粹算术核实的不等式(第4–7步),最后把已核实的各部分组装成最终的形式化定理(第8步)。