[Hol-info] Flyspeck Project completion

[Mark A. <ma...@pr...>]

For those to whom the news has not already reached, Tom Hales'
Flyspeck Project is now complete!  This establishes a formal proof of
Hales' 1998 Kepler Conjecture proof, and is a landmark in the
formalisation of mathematics.  The formal proof was mainly done in HOL
Light, but with one part (the classification of tame hypermaps) done
in Isabelle/HOL.  It involves hundreds of thousands of lines of proof
script, resulting in billions of primitive inferences.  I include
below Hales' original announcement from 5 weeks ago.

Mark.


-----------------------------------------


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.

----

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.

This 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 conjection 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

----

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.