Proof of the Kepler conjecture
Prueba de la conjetura de Kepler sobre empaquetamiento de esferas
- Date
- 1998 (verificación formal 2014) · confidence high
- Place
- Ann Arbor, Michigan, United States
- Credited to
- Thomas Hales (with Samuel Ferguson); the Flyspeck project (2014)
- People
- 👤 Thomas Callister Hales1958–
- Field
- Knowledge & symbols
What was discovered
No packing of equal spheres exceeds the density of the greengrocer's stacking (pi over the square root of 18), as Kepler conjectured in 1611. The proof, with enormous computation, was formally verified in HOL Light and Isabelle in 2014.
The referees at Annals declared themselves 99 per cent certain, which motivated the formalisation.
What it led to
- formal verification of major proofs
- packings in dimensions 8 and 24 (Viazovska)
Built on
- Four color theorem (computer-assisted proof)1976
- Gauss (lattice packings)
- Fejes Tóth (strategy, 1953)
Made possible
- code design and crystallography