Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Formal Proof of the Kepler Conjecture: a critical retrospective

Thomas Hales

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.

The Formal Proof of the Kepler Conjecture: a critical retrospective

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.
Paper Structure (15 sections, 1 theorem, 3 equations)

This paper contains 15 sections, 1 theorem, 3 equations.

Table of Contents

  1. Introduction
  2. Statement
  3. Proof Sketch
  4. partitioning space
  5. outline
  6. revision
  7. Formalization
  8. libraries
  9. international collaboration
  10. alignment between informal and formal
  11. search
  12. Verifying the computer-assisted proof
  13. tame graphs
  14. linear programs
  15. nonlinear inequalities

Key Result

Lemma 4.3.1

[OUIJTWY] If $y\in [-1,1]$, then

Theorems & Definitions (1)

  • Lemma 4.3.1