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

Frequently asked questions

Why is it safe to forget that

y

really equals

x^2

Linear infeasibility is a one-way sufficient condition: if there is no solution even after dropping the constraint $y=x^2$ (which only makes the feasible region larger), then certainly there is no solution once that constraint is put back. If a linear relaxation happens to be feasible, that does not clear the graph — it only means the argument needs a finer relaxation, which is exactly what the case-splitting in the next step provides.

Source

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

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Condensed summaryComputer-assisted

Step 5 of 9: Linearise the nonlinear inequalities attached to each graph

Previous step Next step

In plain words

Some quantities in the geometry (like an angle squared, or a volume that depends nonlinearly on several lengths) are awkward for a computer to reason about directly, so Hales gives every troublesome expression its own temporary name and only remembers the bounds that expression must obey — exactly like replacing 'the square of how fast you're going' with a new variable 'your kinetic energy' and just tracking its range instead of recomputing the square every time.

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

Detailed analysis

For each tame plane graph, the geometry of a contravening packing forces a system of inequalities — dihedral angles, volumes, and scores of the Marchal cells — that is mostly nonlinear. Hales relaxes this system to a linear one by introducing a fresh variable for every nonlinear subexpression, as in the toy example above: the nonlinear fact $x+x^2 \le 3$ together with $x \ge 2$ becomes a linear system once $y=x^2$ is treated as an independent variable bounded by $y \ge 4$ . If the resulting linear system is infeasible, the original nonlinear system must be infeasible too, ruling out that tame graph as a counterexample.

Terms in this step

linear programming relaxation: Replacing a hard system of equations or inequalities with a looser, purely linear one obtained by treating some nonlinear expressions as new independent variables; any solution of the original system is still a solution of the relaxed one, so if the relaxed system already has no solution, neither does the original.

Knowledge used in this step

Linear programming