Lessons from the Formal Proof of the Kepler Conjecture

By Professor Thomas Hale, University of Pittsburgh

Wednesday 21st March 2012, 4.00pm

Lecture Theatre 3, Appleton Tower, 11 Crichton Street, Edinburgh

The Kepler Conjecture asserts that no arrangement of congruent balls in Euclidean space can have density greater than the familiar pyramid arrangement that is used to stack cannonballs. Sam Ferguson and I gave a computer-assisted proof of this conjecture in 1998, but a large team of referees was unable to certify the correctness of the proof after years of effort. A group of researchers is now developing a formal proof of Kepler's assertion, by formally certifying every algorithm and every last logical inference. This project is approaching completion, and this talk will discuss some of the lessons learned and will describe recent work by Solovyev on formal proofs of nonlinear inequalities.

Thomas C. Hales is the Mellon Professor of Mathematics at the University of Pittsburgh. He received B.S. and M.S. degrees from Stanford University, a Tripos Part III from Cambridge University, and a Ph.D. from Princeton University in representation theory under R. P. Langlands. He has held postdoctoral and faculty appointments at MSRI, Harvard University, the University of Chicago, the Institute for Advanced Study, and the University of Michigan. In 1998, Hales, with the help of his graduate student Samuel Ferguson, proved Kepler’s 1611 conjecture (and part of Hilbert’s 18th problem) on the most efficient way to stack oranges. Hales’s current project, called Flyspeck, seeks to formalize the proof of the Kepler conjecture in the computer proof assistant “HOL Light.”

This lecture will be followed by a drinks and canape reception in the Informatics Forum, 4th Floor, Mini Forum 2, 10 Crichton Street Edinburgh

Related links

Accessibility menu