The Flyspeck ProjectIntroductionThe 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 LinksFlyspeck 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 DocumentsThe pdf files are under continual revision. For the absolutely latest version, the raw tex files can be downloaded from the repository.
External LinksHol-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 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"