解法：开普勒猜想的形式化证明:HOL Light与Isabelle中的Flyspeck计划(2015年)
通俗地说
黑尔斯没有试图一次性思考整个无限空间,而是每次只聚焦一个球,只看它固定距离内最近的邻居。如果他能证明这个小邻域永远不会过于拥挤,并且整个堆积中每一个邻域都遵守同样的局部规则,那么整个无限堆积就被控制住了——就像通过检查每一棵树以及它最近的邻居是否健康,来证明整片果园都是健康的。
详细分析
Hales 将空间划分为 Marchal 胞腔,把密度界归约为满足 的球心的局部环形不等式。不同球心之间的分离条件给出该环形区域至多容纳 个球心的堆积界,而紧致性使所得有限优化问题良定义。因此无限几何问题归约为有限个局部构型。
- 马尔沙尔胞腔
- 分配给每个球心的一块空间区域,使得这些胞腔无缝且不重叠地铺满整个空间,其构造方式让一个球的局部拥挤程度可以用它自己胞腔的体积来衡量。