My favorites | Sign in
Project Logo
                

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

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"









Hosted by Google Code