A Revision of the Proof of the Kepler Conjecture

Thomas C. Hales (), John Harrison (), Sean McLaughlin (), Tobias Nipkow, Steven Obua and Roland Zumkeller
Additional contact information
Thomas C. Hales: University of Pittsburgh, Math Department
John Harrison: Intel Corporation, JF1-13
Sean McLaughlin: Carnegie Mellon University
Tobias Nipkow: Technische Universität München, Department for Informatics
Steven Obua: Technische Universität München, Department for Informatics
Roland Zumkeller: École Polytechnique

Chapter 9 in The Kepler Conjecture, 2011, pp 341-376 from Springer

Abstract: Abstract The Kepler conjecture asserts that no packing of congruent balls in threedimensional 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.

Keywords: Formal proof; Sphere packings; Linear programming; Interval analysis; Higher order logic; Hypermap (search for similar items in EconPapers)
Date: 2011
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-1-4614-1129-1_9

Ordering information: This item can be ordered from
http://www.springer.com/9781461411291

DOI: 10.1007/978-1-4614-1129-1_9

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().