The Flyspeck Project: A Formal Proof of the Kepler Conjecture

In 1611, Johannes Kepler asserted that the maximum density of a sphere packing in a three dimensional space is achieved by the familiar cannonball arrangement. This results (known as the Kepler conjecture) was proved in 1998 by Thomas Hales and Samuel Ferguson. An important part of the proof of the Kepler conjecture is computer code which cannot be completely verified by a standard peer review process. To eliminate any uncertainties about the correctness of the proof, Hales launched the Flyspeck project in the beginning of 2003. The aim of this project is a complete formal verification of the Kepler conjecture. In my talk, I will give a high level overview of the proof of the Kepler conjecture and present my contributions to the Flyspeck project. I will emphasize formal verification of the computer code part of the proof and my work on developing automatic tools and techniques for a rigorous verification of nonlinear inequalities.