解法：开普勒猜想的形式化证明:HOL Light与Isabelle中的Flyspeck计划(2015年)
通俗地说
再进一步放大到某个球的邻域,给每个附近的球画一个点,只要两个邻居相接触或靠得很近就连一条线;这幅草图就是画在该球周围球面上的一个小图,可以展平到平面上。黑尔斯证明,如果一个堆积密集到足以构成反例所需的程度,这个小图只能呈现极少数受限形状中的一种——绝不会杂乱无章——这正是让计算机能够接手情形检验的原因。
详细分析
紧致性使得黑尔斯可以假设局部环形不等式的一个反例 具有一种特殊的极值形式,称为'抵触型'(contravening)。对抵触型 的细致几何研究('主估计')表明,其邻近球的组合模式总能构成一个平面图 ,满足关于顶点度数和面大小的一小组严格组合条件;满足这些条件的图称为驯顺图(tame)。于是每一个可能的反例都被标记上一个具体的驯顺平面图,把一个关于球位置的分析问题变成了一个关于图的有限组合分类问题。
- 驯顺平面图
- 平面图——顶点与边在平面上不相交地画出——如果满足一小组关于每个顶点相接边数与每个面边数的精确限制,就称为驯顺图。