The problem
No packing of congruent spheres in three-dimensional Euclidean space has average density exceeding π/√18 ≈ 74.048%, attained by the face-centred cubic (and hexagonal close-packed) arrangements.
The Kepler Conjecture
historicHistory & significance
From Kepler's 1611 pamphlet on snowflakes, after Hilbert listed it as part of his 18th problem in 1900. Hilbert's programme for the geometry of packings produced Thue's 2D analogue (1910, rigorized 1940s) but 3D resisted all analytic attack. Hales's 1998 proof leaned on computer enumeration, and referees would certify only 99% confidence — so Hales launched Flyspeck, which fully formalized the proof (completed 2014): a machine-checked Kepler beside the human one.
Connected problems
- related Optimal Sphere Packing in Dimensions 8 and 24
- related Fermat's Last Theorem
More in discrete geometry
- same area The Erdős–Ulam Problem
- same area The Tammes Problem
- same area The Kissing Number Problem
References
The resolution (computer-assisted proof)
Proved by Thomas Hales with Samuel Ferguson, 1998: a hybrid of inequality estimates over 5,000 configuration cases, published in Annals after referees reported being 99% certain — unprecedented hedging that pushed Hales toward something new: a complete machine-checked proof. The Flyspeck project finished formalising it in Isabelle/HOL in 2014, 21 computers, 20 gigabytes, no doubt. The precedent for today's Lean-certified AI announcements.
How to check it: Ferguson's thesis settled the pentahedral-prism case; Hales's 1998 Annals paper plus the 2006 discrete-geometry update cover the rest, with linear-programming bounds doing the heavy lifting case by case. Flyspeck (Isabelle/HOL + HOL Light, completed 2014) re-verified every inequality mechanically. Compare the 8- and 24-dimensional packing triumphs elsewhere on this shelf.
Verified by curator — see the API for full claim provenance.