Worked solution: Flyspeck: a formal proof of the Kepler conjecture in HOL Light and Isabelle (2015)

Step 7 of 9: Verify nearly a thousand nonlinear inequalities by rigorous interval arithmetic

In plain words

For the handful of inequalities that can't be linearised away, Hales still needs a rigorous bound on a curved function over a whole region, not just at one point; rather than chopping the region into millions of tiny boxes (correct but painfully slow), he uses calculus to bound the function by its value and slope at one central point plus a controlled error term — like predicting a hiker's elevation everywhere on a hillside from their position, direction, and a bound on how curvy the hillside can be.

g(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}

Detailed analysis

The remaining ingredient is a single conjunction of nearly $1000$ nonlinear inequalities about dihedral angles and volumes that cannot be linearised away. Naïve interval arithmetic — subdividing the domain and bounding the function on each piece — is formally sound but far too slow for these multivariate inequalities. Instead each inequality is bounded using a verified second-order Taylor interval extension: fixing a point $y$ inside the domain, the formula above turns bounds on $g(y)$ , $g'(y)$ , and $g''$ over the whole box into a certified enclosure of $g(x)$ for every $x$ in the box, giving a much tighter and still fully rigorous bound. This is the most computationally expensive of the three computer-generated ingredients: the article reports that the hardest of the three subclaims takes on the order of $5000$ CPU-hours to verify.

Terms in this step

interval arithmetic: A way of computing with guaranteed lower and upper bounds instead of single numbers, so that every rounding or approximation error is tracked and the final bound is still provably correct, never just numerically plausible.