Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hales, T. (2004). Formalizing the Proof of the Kepler Conjecture. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2004. Lecture Notes in Computer Science, vol 3223. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30142-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-30142-4_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23017-5
Online ISBN: 978-3-540-30142-4
eBook Packages: Springer Book Archive