The familiar arrangement used for stacking cannonballs and oranges β hexagonal close-packing β is the densest possible way to pack identical spheres in space, achieving about 74.05% density and no more. Conjectured by Johannes Kepler in 1611, it resisted proof for nearly 400 years until Thomas Hales completed an extraordinary computer-assisted proof in 1998, which then took a dedicated international team another 15 years to fully, formally verify.
Walk into any grocery store and look at how oranges are stacked in a pyramid display: each layer nestles into the gaps of the layer beneath it. Grocers have arranged fruit this way for centuries because it's obviously space-efficient β but proving, with full mathematical rigour, that this really is the absolute best possible way to pack spheres turned out to be one of the hardest problems in the history of geometry.
The difficulty isn't in showing that this particular stacking arrangement achieves 74.05% density β that part is straightforward. The genuinely hard part is ruling out every conceivable alternative arrangement, including bizarre and highly irregular ones that no grocer would ever think to try, and proving that literally none of them could possibly do better. With infinitely many conceivable sphere arrangements to consider, this required an entirely different kind of proof strategy than ordinary geometric reasoning could provide.
Thomas Hales, building on earlier work by LΓ‘szlΓ³ Fejes TΓ³th, completed a proof in 1998 that reduced the infinite space of possible arrangements down to a finite (but still enormous) number of specific cases, each of which then had to be checked individually by computer. The proof was so long and computationally intensive that the reviewing mathematical journal could only state they were "99% certain" of its correctness after four years of review β an unprecedented and controversial situation in the history of mathematical publishing.
The packing density of a sphere arrangement is the fraction of total space occupied by the spheres themselves (as opposed to empty gaps between them), in the limit of an arrangement extending infinitely in all directions. Kepler's conjecture states the maximum possible density for identical spheres is exactly Ο/β18 β 0.7405, or about 74.05%.
There are actually two distinct arrangements achieving this identical maximum density: face-centred cubic packing (the familiar cannonball-stacking arrangement) and hexagonal close packing (a related but subtly different layering pattern). Both achieve exactly the same density, and in fact infinitely many further variations combining elements of both patterns also achieve this same maximum β meaning the "optimal" arrangement is very far from unique.
Hales's approach (building substantially on foundational ideas from LΓ‘szlΓ³ Fejes TΓ³th, who first suggested in 1953 that the problem might be reducible to a finite, computer-checkable calculation) assigns each possible sphere arrangement a "score" based on a specific local geometric analysis, and shows that the maximum possible score corresponds exactly to the density claimed by Kepler's conjecture. This reduces an inherently infinite geometric problem to checking roughly 5,000 distinct configurations of spheres, each requiring extensive computer-verified linear programming calculations β a combination of human mathematical insight (setting up the precise reduction and scoring system) and brute computational force (checking each resulting individual case) characteristic of several other major 20th and 21st century mathematical results (compare the Four Colour Theorem entry).
Intuitively, no matter how spheres are arranged, unavoidable "wasted" empty space always remains between them, since spheres are curved and cannot tile space perfectly without leaving any gaps (unlike, say, cubes, which perfectly fill 100% of space with zero wasted gaps). Kepler's conjecture pins down the exact, unavoidable minimum amount of such wasted space for identical spheres specifically.
Hales submitted his proof to the prestigious journal Annals of Mathematics in 1998. After four years of careful review by a panel of twelve expert referees, the journal's editors took the unusual step of publishing the paper in 2005 with an accompanying note stating the reviewers were "99% certain" of the proof's correctness, but could not fully verify every one of the extensive computer calculations involved within a reasonable review timeframe. This unprecedented situation β a major result published with an explicit caveat about incomplete verification β highlighted a growing tension in mathematics between the increasing reliance on computer-assisted proof techniques and the traditional expectation that a human peer reviewer can, in principle, fully verify every step.
Motivated directly by this uncertainty, Hales launched the Flyspeck project ("Formal Proof of Kepler") in 2003 β an ambitious, multi-year international collaborative effort to produce a complete, machine-checked formal verification of every single step of the proof, using formal proof assistant software (specifically HOL Light and Isabelle) that mechanically checks each logical inference against foundational axioms, leaving no room whatsoever for human oversight error or computational bugs to go undetected. The project was declared fully complete in 2014, providing the first-ever complete, machine-verified certainty that Kepler's conjecture is indeed true β 403 years after Kepler first proposed it, and 16 years after Hales's original (highly convincing but not 100% formally verified) proof.
The analogous sphere-packing problem in other dimensions has proven even more varied in difficulty. The 1-dimensional and 2-dimensional cases were solved comparatively easily using classical methods. Remarkably, the 8-dimensional case was solved by Maryna Viazovska in 2016 using an elegant and unexpected technique involving modular forms, and the 24-dimensional case (connected to an exceptionally symmetric structure called the Leech lattice) was solved shortly afterward by Viazovska together with several collaborators, also in 2016. Viazovska was awarded the Fields Medal in 2022 for this work. The general n-dimensional sphere-packing problem, for most dimensions other than these specific solved cases (1, 2, 3, 8, and 24), remains completely open.
Sphere-packing problems are directly and deeply connected to the design of error-correcting codes in information theory and digital communications: an efficient code for transmitting data reliably over a noisy channel corresponds mathematically to an efficient sphere-packing arrangement in a suitably high-dimensional space, where each valid codeword acts as the centre of a sphere designed to be as densely and efficiently packed as possible while still remaining reliably distinguishable from its neighbours despite transmission noise.