REVIEW 2 cited by
The Formal Proof of the Kepler Conjecture: a critical retrospective
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original 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. In 1998, Sam Ferguson and I announced a computer-assisted proof of this conjecture. Long delays in the refereeing process sparked a project to give a formal proof of the Kepler conjecture, which was completed in a large collaborative effort in 2014. This article gives a critical reappraisal of that project.
Forward citations
Cited by 2 Pith papers
-
FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature $-$ Toward the Formalization of the Classification of Finite Simple Groups
AI-assisted workflow built a machine-checked Lean theory covering Feit-Thompson, Glauberman Z*, Brauer-Suzuki, and Bender-Suzuki from distributed literature.
-
Complementary bodies in sphere packing
The gaps in cubic close packing of equal spheres are exactly tiled by two named spherically truncated polyhedra, and their volumes and surface areas are derived explicitly.
Discussion (0). Continue with ORCID to comment.