MathLabs

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

第 7/9 步：用严格的区间算术验证近千条非线性不等式
上一步下一步
通俗地说

对于那少数无法通过线性化消除的不等式,黑尔斯仍需要在整个区域上(而不仅仅是一点上)给出一个曲线函数的严格界;他没有把该区域切成数百万个小盒子(正确但极其缓慢),而是用微积分通过函数在一个中心点的取值、斜率,再加上一个受控的误差项来界定该函数——就像通过一位徒步者的位置、方向,以及山坡弯曲程度的一个界限,来预测他在山坡上任何地方的海拔高度。

g(y)−r(x)  ≤  g(x)  ≤  g(y)+r(x),r(x)=∣g′(y)∣ w+12 ∣g′′(ξ(x))∣ w2g(y) - r(x) \;\le\; g(x) \;\le\; g(y) + r(x), \qquad r(x) = \lvert g'(y)\rvert\,w + \tfrac12\,\lvert g''(\xi(x))\rvert\,w^{2}
详细分析

剩下的部分是一个由近 10001000 条关于二面角和体积的不等式组成的合取式,它们无法被线性化消去。朴素的区间算术——把定义域细分并在每一小块上界定函数——在形式上是可靠的,但对这些多元不等式来说太慢了。取而代之的是,每条不等式都用一种已验证的二阶泰勒区间扩张来界定:在定义域内固定一点 yy,上面的公式把整个区域上 g(y)g(y)、g′(y)g'(y) 和 g′′g'' 的界,转化为对该区域内任意 xx 处 g(x)g(x) 的一个已验证的包围区间,从而给出一个严格得多、同时依然完全严格的界。这是计算机生成的三个组成部分中计算量最大的一个:论文指出,这三个子问题中最难的一个大约需要 50005000 个CPU小时来验证。

本步骤中的术语
区间算术
一种用有保证的上下界而非单一数值进行计算的方法,使得每一次舍入或近似误差都被追踪,最终得到的界依然是可以证明正确的,而不仅仅是数值上看似合理。