解法：开普勒猜想的形式化证明:HOL Light与Isabelle中的Flyspeck计划(2015年)
通俗地说
由于只有一族受限的形状可能出现,计算机只需尝试画出所有可能的形状,一旦某个正在构造的形状已经违反驯顺规则就立刻丢弃它,就像通过一试到不合适就立刻剔除的方式来拼拼图。输出结果是一个有限的图形图库,而困难的数学论断是:这个图库是完备的——没有遗漏任何一个。
计算机搜索枚举出满足驯顺条件的所有有限平面图,并剪掉那些不可能变成驯顺图的分支;得到的目录——最初超过 个图,在为形式化而收紧驯顺定义之后精简为 个——被证明是完备的:每一个驯顺平面图都与目录中的某一个同构。这条完备性定理在Isabelle/HOL中被形式化(枚举过程要搜索约 个中间图),随后作为一条手工翻译的假设被导入HOL Light;由于该命题中所有量词的取值范围都是有界的有限结构,这条命题等价于一个命题逻辑的可满足性(SAT)断言,在两种逻辑系统中都能以完全相同的方式证明,这正是把结果在两个证明助手之间搬移的依据。
- 同构的图
- 如果可以给一个图的顶点重新命名,使它看起来与另一个图完全一样——顶点数、边数、连接方式都相同——那么这两个图就是同构的,即便它们在纸面上画法不同。