Formalizing the Proof of the Kepler Conjecture

The Kepler Conjecture states that the densest packing of spheres in three dimensions is the familiar cannonball arrangement. Although this statement has been regarded as obvious by chemists, a rigorous mathematical proof of this fact was not obtained until 1998. The mathematical proof of the Kepler Conjecture runs 300 pages, and relies on extensive computer calculations. The refereeing process involved more than 12 referees over a five year period. This talk will describe the top-level structure of the proof of this theorem. The proof involves methods of linear and non-linear optimization, and arguments from graph theory and discrete geometry. In view of the complexity of the proof and the difficulties that were encountered in refereeing the proof, it seems desirable to have a formal proof of this theorem. This talk will give details about what would be involved in giving a formal proof of this result.