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

Frequently asked questions

Could there still be a subtle error in the formal proof?

In principle yes, but only in the tiny trusted kernel of the proof assistant itself (a few hundred lines, independently reviewed and even partly self-verified) or in the informal translation of 'the Kepler conjecture' into the formal statement above; every other step, including all case analysis and numerical computation, is checked automatically and cannot silently go wrong.

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 9 of 9: A landmark in machine-checked mathematics

Previous step Next step

In plain words

Once the Kepler conjecture had a proof that a computer, not just a human referee, could check line by line, mathematicians gained a new kind of confidence: the same confidence we have that a calculator's arithmetic is correct. Flyspeck stands alongside a handful of other giant formalisation projects — a machine-verified odd-order theorem, a machine-verified C compiler, a machine-verified operating-system kernel — as proof that century-old open problems can, in principle, be checked all the way down to logical bedrock.

\mathrm{CARD}(V \cap B(0,r)) \le \frac{\pi r^3}{\sqrt{18}} + c\,r^2

Detailed analysis

The formalised main statement says: for every packing $V$ , there is a constant $c$ such that for every radius $r \ge 1$ , the number of ball centres inside a container of radius $r$ satisfies $\mathrm{CARD}(V \cap B(0,r)) \le \pi r^3/\sqrt{18} + c\,r^2$ ; letting $r \to \infty$ recovers Kepler's density bound in its classical form. Because the proof scripts were saved in a replayable format, any reader with an ordinary computer can re-run the entire HOL Light verification of the main statement in about forty minutes, an independent check that requires trusting only the small, published kernel of the proof assistant rather than the thousands of pages of case analysis behind it.

Flyspeck's scale — described by the authors as comparable to the Feit–Thompson odd-order theorem, the CompCert verified C compiler, and the seL4 verified microkernel — helped establish that fully formal verification is a realistic option even for the hardest classical open problems, not just for pieces of software; it also left behind reusable HOL Light libraries for real and complex analysis that later formalisation projects have built on.

Knowledge used in this step

Formal proof with proof assistants (Lean)