Flyspeck

We are pleased to announce the completion of the Flyspeck project, which has constructed a formal proof of the Kepler conjecture. The Kepler conjecture asserts that no packing of congruent balls in Euclidean 3-space has density greater than the face-centered cubic packing. It is the oldest problem in discrete geometry. The proof of the Kepler conjecture was first obtained by Ferguson and Hales in 1998. The proof relies on about 300 pages of text and on a large number of computer calculations.

The formalization project covers both the text portion of the proof and the computer calculations. The blueprint for the project appears in the book "Dense Sphere Packings," published by Cambridge University Press. The formal proof takes the same general approach as the original proof, with modifications in the geometric partition of space that have been suggested by Marchal.

Formal Proof

A formal proof is a mathematical proof that has been checked by computer from the foundational axioms of mathematics and primitive inference rules. A formal proof provides a much higher degree of certification than traditional standards of rigor and peer review by referees.

The formal proof has been constructed in a combination of the Isabelle and HOL Light formal proof assistants.

The Isabelle portion of the formalization, which was carried out by Bauer and Nipkow, classifies all tame graphs. This enumerates the combinatorial structures of potential counterexamples to the Kepler conjecture.

Their classification theorem has been translated directly by hand into a corresponding term import_tame_classification in the HOL Light proof assistant. At a conceptual level, the classification theorem could be formulated as a large SAT problem, and SAT problems pass easily from one proof assistant to another.

The rest of the formalization has been carried out in HOL Light, producing a formal theorem

|- import_tame_classification /\ the_nonlinear_inequalities
==> the_kepler_conjecture

where the_kepler_conjecture is defined as the following term

`(!V. packing V ==> (?c. !r. &1 <= r ==> &(CARD(V INTER ball(vec 0,r))) <= pi * r pow 3 / sqrt(&18) + c * r pow 2))`

In standard mathematical language, this states that for every packing V (which is identified with the set of centers of balls of radius 1), there exists a constant c controlling the error term, such that for every radius r that is at least 1, the number of ball centers inside a spherical container of radius r is at most pi * r^3 / sqrt(18), plus an error term of smaller order. As r tends to infinity, this gives the density bound pi / sqrt(18) = 0.74+, which is the density of the face-centered-cubic packing.

The term the_nonlinear_inequalities is defined as a conjunction of several hundred nonlinear inequalities. The domains of these inequalities have been partitioned to create more than 23,000 inequalities. The verification of all nonlinear inequalities in HOL Light on the Microsoft Azure cloud took approximately 5000 processor-hours. Almost all verifications were made in parallel with 32 cores, hence the real time is about 5000 / 32 = 156.25 hours. Nonlinear inequalities were verified with compiled versions of HOL Light and the verification tool developed in Solovyev's 2012 thesis.

To check that no pieces were overlooked in the distribution of inequalities to various cores, the pieces have been reassembled in a specially modified version of HOL Light that allows the import of theorems from other sessions of HOL light. In that version, we obtain a formal proof of the theorem

|- the_nonlinear_inequalities

Download

The code for the project is available for download from http://afp.sourceforge.net/devel-entries/Flyspeck-Tame.shtml (Isabelle tame graphs) https://code.google.com/p/flyspeck/ (HOL Light Flyspeck project).

There have been many contributors to the project as indicated in the credits below. Many of them will be co-authors of the published account of the formal proof.

Sincerely,

Thomas Hales, Alexey Solovyev, Hoang Le Truong, and the Flyspeck Team August 10, 2014

Credits

• Project Director: Thomas Hales
• Project Managers: Ta Thi Hoai An, Mark Adams
• HOL Light libraries and support: John Harrison,
• Isabelle Tame Graph Classification: Gertrud Bauer, Tobias Nipkow,
• Chief Programmer: Alexey Solovyev,
  • Nonlinear inequalities: Victor Magron, Sean McLaughlin, Roland Zumkeller,
  • Linear Programming: Steven Obua,
  • Microsoft Azure Cloud support: Daron Green, Joe Pleso, Dan Synek, Wenming Ye,
• Chief Formalizer: Hoang Le Truong,
  • Text formalization: Jason Rute, Dang Tat Dat, Nguyen Tat Thang, Nguyen Quang Truong, Tran Nam Trung, Trieu Thi Diep, Vu Khac Ky, Vuong Anh Quyen,
• Student Projects: Catalin Anghel, Matthew Wampler-Doty, Nicholas Volker, Nguyen Duc Tam, Nguyen Duc Thinh, Vu Quang Thanh,
• Proof Automation: Cezary Kaliszyk, Josef Urban,
• Editing: Erin Susick, Laurel Martin, Mary Johnston,
• External Advisors and Design: Freek Wiedijk, Georges Gonthier, Jeremy Avigad, Christian Marchal,
• Institutional Support: NSF, Microsoft Azure Research, William Benter Foundation, University of Pittsburgh, Radboud University, Institute of Math (VAST), VIASM.