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.

Speaker Details

Alexey Solovyev received his PhD in Mathematics from the University of Pittsburgh in 2012. His dissertation “Formal computations and methods” was advised by Prof. Thomas Hales. Alexey is now working as a postdoctoral researcher at the University of Utah in Prof. Ganesh Gopalakrishnan’s formal verification group. Research interests of Alexey are formal theorem proving, verification of floating-point computations, and computer-aided mathematics.

Alexey Solovyev
University of Utah
    • Portrait of Jeff Running

      Jeff Running