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
historicReferences
History & 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.
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.