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
- Formalizing the Text This is a proposal about how to formalize the written text of the proof.
- IMO-demo A demo on using HOL Light, including Harrison's IMO problem video.
- Browse flyspeck Browse the subversion repository
- View flyspeck Google code view of repository.
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
- 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
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"
