Welcome to the Flyspeck project, which gives a formal proof of the Kepler conjecture in the HOL Light proof assistant. The Kepler conjecture asserts that no packing of congruent balls in Euclidean 3-space has density greater than that of the familiar cannonball arrangement.
The project was completed August 10, 2014.
The purpose of the flyspeck project was to produce a formal proof of the Kepler Conjecture. The name flyspeck comes from matching the pattern /f.*p.*k/ against an English dictionary. FPK in turn is an acronym for "The Formal Proof of Kepler."
See a step by step installation guide.
There is an installation guide for the project and other Wiki pages.
The formalization project is based on the book Dense Sphere Packings, which is available from Cambridge University Press.
This project is distributed under the MIT Licence.
This project was supported by NSF through grant 0503447 on the "Formal Foundations of Discrete Geometry" and grant 0804189 on the "Formal Proof of the Kepler Conjecture", the Benter Foundation, Microsoft Azure Research, the University of Pittsburgh, Radboud Research Facilities, Institute of Math (VAST), and VIASM.
The main proof scripts are in the subdirectory
text_formalization.
The primary files used to build the project are in
text_formalization/build.
See especially text_formalization/build/ocamlinit_hol_light.ml
The directory structure for the flyspeck project is as follows.
azure
Files related to the formal verification of nonlinear inequalities.
These inequalities were first formally verified by a computation on the Microsoft Azure Cloud.
formal_graph
Files related to the formal verification of the classification of tame graphs in
the Isabelle proof assistant. Most of these files are a backup of files are part of the
Isabelle Archive of Formal Proofs
afp.sf.net (afp.sourceforge.net/entries/Flyspeck-Tame.shtml).
That archive should be used to download
the code for the formal verification of the classification of tame graphs.
The files here are solely to aid in
the translation of the statement of the theorem into HOL Light.
formal_ineqs
Files related to the formal verification of nonlinear inequalities.
formal_lp
Files related to the formal verification on linear programs.
informal_code
Code used for the informal computer programs used in the proof of the Kepler conjecture.
These files are not required for the flyspeck project.
jHOLLight
Code for the java front end that is used for Solovyev's SSReflect mode for HOL Light.
kepler_tex
Latex source files for the book "Dense Sphere Packings"
legacy
This directory contains dead code that is no longer of any use. Ignore this directory.
text_formalization
This is the main directory of the project. It contains the files for the formalization of the
text part of the flyspeck project, as described in the book "Dense Sphere Packings"
See the README file in that directory
for more instructions on loading and auditing the project.
text_formalization/build directory contains files related to building the project.
usr
These files are not part of the flyspeck project.
It mostly contains an assortment of latex files for articles written by Hales.