The Flyspeck Project

Introduction

The purpose of the flyspeck project is 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."

Internal Links

• Flyspeck Wiki
• What's left in the text part of the formalization. It is nearly complete!

PDF Documents

The pdf files are under continual revision. For the absolutely latest version, the raw tex files can be downloaded from the repository.

External Links

• Hol-light source code repository
• Flyspeck Google Group
• 2009 Hanoi workshop
• code for 1998 proof
• McLaughlin's revision of the kepler code
• Flyspeck I: Tame Graphs G. Bauer and T. Nipkow
• Flyspeck II: Linear Programs S. Obua
• QED Manifesto
• Nonlinear inequality proving R. Zumkeller

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.