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

第 6/9 步：用已验证的对偶解证明每个线性规划都不可行

通俗地说

要让一台多疑的机器相信一个线性不等式组无解,只说“我试过但失败了”是不够的——你必须交出一份简短的配方(一组非负权重),把这些不等式组合成一个明显错误的命题,例如 $0 \le -1$ ;核验这份配方只是做数字加法,证明助手完全信任这一点,不同于最初猜出这份配方的外部数值求解器。

\lambda \ge 0, \quad \textstyle\sum_i \lambda_i\,(\text{constraint}_i) \;\Longrightarrow\; 0 \le -\varepsilon \ \ (\varepsilon>0)

详细分析

线性规划的不可行性通过给出其约束的一组非负乘子 $\lambda$ 来验证,这些乘子的加权和会消去所有变量,得到一个明显错误的不等式,例如 $0 \le -\varepsilon$ ——这是一种法卡斯型对偶证书,形式化证明只需做纯粹的算术求和就能核验,而无需重新求解该规划。在约 $18\,762$ 个驯顺图中,大约一半需要把可行域(通过 $x \le a$ 或 $a \le x$ 这类不等式分支)划分成若干子情形,线性松弛才足够紧以致不可行,而像 $\sqrt2$ 或 $\pi$ 这样的无理数系数则被替换为已验证的有理数界。总共生成了 $43\,078$ 个线性规划,每一个都被形式化证明为不可行。

本步骤中的术语

对偶证书(法卡斯证书): 一组非负乘子,每个不等式对应一个,使得这些不等式的加权和坍缩为一个明显错误的命题;它的存在就是原方程组无解的严格证明,并且只需通过简单的算术就能核验,而无需重新求解方程组。

本步骤用到的知识

线性规划

常见错误. 外部求解器GLPK只用来搜索候选的对偶乘子,其浮点输出未必可靠;HOL Light中的形式化证明会从这个猜测出发,重新推导出一个精确算术下正确的对偶证书,并通过可手工核验的求和来检验它,因此任何数值上不可靠的步骤都不会进入证明的内核。