The Flyspeck Project

The project was completed August 10, 2014.

Google is shutting down google code and we are being evicted. This site is no longer maintained. Look for updates of the Flyspeck project on GitHub.

Introduction

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."

Book

The formalization project is based on the book "Dense Sphere Packings: a formal blueprint", published by Cambridge University Press, and (print) or (pdf).

Internal Links

• Flyspeck Wiki
• The Announcement of the Completion of the Project August 10, 2014
• Guide to installing and auditing the Project

External Links

• The official report of the completed project
• Hol-light source code repository
• Dense Sphere Packings book (pdf) T. Hales
• Flyspeck I: Tame Graphs G. Bauer and T. Nipkow
• Flyspeck II: Linear Programs S. Obua
• QED Manifesto
• McLaughlin's revision of the kepler code
• Nonlinear inequality proving R. Zumkeller
• Learning-assisted Automated Reasoning with Flyspeck C. Kaliszyk and J. Urban
• Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations T. Hales and A. Solovyev
• Formal Computations and Methods A. Solovyev
• Formal Proofs for Global Optimization V. Magron

T. Hales acknowledges the support of the NSF through grant 0503447 on the "Formal Foundations of Discrete Geometry" and grant 0804189 on the "Formal Proof of the Kepler Conjecture". He gratefully acknowledges support from the Benter Foundation.

The project has received support from Microsoft Azure Research, the University of Pittsburgh, Radboud Research Facilities, Institute of Math (VAST), and VIASM.