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

常见问题

为什么可以安全地忽略

y

实际上等于

x^2

这一事实?

线性方程组无解是一个单向的充分条件:如果在去掉约束 $y=x^2$ (这只会扩大可行域)之后仍然无解,那么把这个约束加回去之后当然更不可能有解。反过来,如果某个线性松弛恰好可行,那也并不能排除这个图——它只说明论证需要一个更精细的松弛,这正是下一步的情形划分所提供的。

来源

Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller, 2015

A formal proof of the Kepler conjecture

arXiv:1501.02155v1

许可协议: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

精简版有计算机辅助

第 5/9 步：把每个图所对应的非线性不等式线性化

上一步下一步

通俗地说

几何中的某些量(比如一个角度的平方,或非线性依赖于若干长度的体积)不便于计算机直接推理,因此黑尔斯给每一个麻烦的表达式起一个临时的名字,只记住该表达式必须满足的界限——就好比把“你行进速度的平方”替换成一个新变量“你的动能”,此后只追踪它的取值范围,而不必每次都重新计算平方。

x + x^{2} \le 3,\ x \ge 2 \quad\xrightarrow{\ y \,=\, x^{2}\ }\quad x + y \le 3,\ x \ge 2,\ y \ge 4

详细分析

对每一个驯顺平面图,一个抵触型堆积的几何都会给出一个不等式组——涉及二面角、体积和马尔沙尔胞腔的分数——其中大多数是非线性的。黑尔斯为每个非线性子表达式引入一个新变量,从而把这个不等式组松弛为线性的,正如上面的示例:非线性事实 $x+x^2 \le 3$ 与 $x \ge 2$ 一起,一旦把 $y=x^2$ 当作一个独立变量并用 $y \ge 4$ 约束它,就变成了一个线性方程组。如果得到的线性方程组无解,那么原来的非线性方程组也必定无解,从而把该驯顺图排除在反例之外。

本步骤中的术语

线性规划松弛: 把某些非线性表达式当作新的独立变量处理,从而用一个更宽松的、纯线性的方程组来替代原本困难的方程或不等式组;原方程组的任何解仍然是松弛后方程组的解,因此若松弛后的方程组已经无解,原方程组也必定无解。

本步骤用到的知识

线性规划