The Dennes Room

Event Detail

Mon Apr 22, 2019
4 LeConte Hall, 4–5 PM
Alfred Tarski Lectures
Thomas Hales (University of Pittsburgh)
A formal proof of the Kepler conjecture

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.