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