A revision of the proof of the Kepler conjecture

Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland Zumkeller

Research output: Contribution to journalArticlepeer-review

68 Scopus citations

Abstract

The Kepler conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space has density greater than that of the face-centered cubic packing. The original proof, announced in 1998 and published in 2006, is long and complex. The process of revision and review did not end with the publication of the proof. This article summarizes the current status of a long-term initiative to reorganize the original proof into a more transparent form and to provide a greater level of certification of the correctness of the computer code and other details of the proof. A final part of this article lists errata in the original proof of the Kepler conjecture.

Original languageEnglish
Pages (from-to)1-34
Number of pages34
JournalDiscrete and Computational Geometry
Volume44
Issue number1
DOIs
StatePublished - Jul 2010

Keywords

  • Formal proof
  • Higher order logic
  • Hypermap
  • Interval analysis
  • Linear programming
  • Sphere packings

Fingerprint

Dive into the research topics of 'A revision of the proof of the Kepler conjecture'. Together they form a unique fingerprint.

Cite this