Tarski Lecture: A formal proof of the Kepler conjecture
Lecture | April 22 | 4-5 p.m. | 4 LeConte Hall
Thomas Hales, University of Pittsburgh
The Kepler Conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space can have density greater than that of the face-centered cubic packing. This talk will describe the history and proof of the conjecture, including early attempts to reduce the problem to a finite calculation, controversy surrounding claimed proofs, the announcement of a proof by Sam Ferguson and me more than 20 years ago, and finally a formal proof of the Kepler conjecture in the HOL Light proof assistant in 2014.