The Flyspeck Project
Announcement: There will be a summer workshop on the Flyspeck Project in Hanoi Vietnam during the months of June and July 2009. There will be intensive short courses on Objective CAML, the foundations of HOL, and the proof of the Kepler Conjecture. The workshop is supported by the National Science Foundation. Please contact Thomas Hales if you are interested in participating.
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
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"
