On this page
In 1611 Johannes Kepler wrote a short booklet, *Six-Cornered Snowflake*, guessing that equal balls cannot be packed more tightly than a fruit seller's pyramid. The formal proof paper by Hales and 21 co-authors traces the conjecture to that booklet and calls it "the oldest problem in discrete geometry." Settling it took almost four centuries and a great deal of computer time.
What is the Kepler conjecture?
The Kepler conjecture says that no packing of equal spheres in ordinary three-dimensional space has a higher density than the face-centred cubic packing (Hales et al., Forum of Mathematics, Pi).
The code repository for the 1998 proof puts it more simply: no packing beats "the familiar pyramid-shaped packing used to stack oranges at the market" (kepler98 repository).
Density here means the fraction of space the balls fill. For the orange stack that fraction is π/√18, or about 0.74 (Hales et al., arXiv). So even a perfectly stacked crate of oranges is about 26% air.
Showing one good stacking is easy. Ruling out every possible arrangement, including irregular ones nobody has drawn, is the real problem. The same paper notes that it became part of Hilbert's 18th problem, and that from the 1950s L. Fejes Tóth laid out a proof strategy and suggested that computers might be used.
How did Thomas Hales prove the Kepler conjecture?
Thomas Hales and Sam Ferguson announced a computer-assisted proof in 1998, as Hales recalls in his critical retrospective of the project. The *Annals of Mathematics* received his main paper on 4 September 1998 (Annals of Mathematics) and printed it in 2005, on pages 1065 to 1185 (DOI record).
The idea was to turn a question about infinitely many arrangements into a finite but enormous list of cases, then have a computer check each one. According to the 1998 code repository, the computer side had three main jobs:
proving nonlinear inequalities with interval arithmetic, which works with ranges of numbers so rounding errors cannot sneak in
verifying linear programs
generating every planar graph that satisfies a technical list of properties
The parts done by hand filled a series of eight papers.
Why did checking the proof take until 2014?
The Flyspeck paper quotes the mathematician Jeffrey Lagarias, who described the review process: "The nature of this proof … makes it hard for humans to check every step reliably." In the end the proof was published "without complete certification from the referees."
Hales's answer was to have software check the proof. At the Joint Math Meetings in Baltimore in January 2003 he announced Flyspeck, an expansion of the acronym FPK, for the Formal Proof of the Kepler conjecture. The formal proof was carried out in a combination of two proof assistants, HOL Light and Isabelle (Forum of Mathematics, Pi).
The project "was completed in a large collaborative effort in 2014," Hales writes in the retrospective. The official account appeared in *Forum of Mathematics, Pi* in 2017 (DOI record). The hardest of its three computational subclaims takes about 5000 CPU hours to verify (Hales et al., arXiv).
How do you get 74% for the orange stack?
You can check the number with school geometry. Take the face-centred cubic cell: a cube with a sphere of radius r at each corner and at the centre of each face.
Spheres inside the cube: 8 corners × 1/8 + 6 faces × 1/2 = 4.
Spheres touch along a face diagonal, so the diagonal is 4r and the side is a = 4r/√2 = 2√2 r.
Volume of the spheres: 4 × (4/3)πr³ = (16/3)πr³.
Volume of the cube: (2√2 r)³ = 16√2 r³.
Density: (16/3)π ÷ 16√2 = π/√18 ≈ 0.7405, the value the Flyspeck paper gives.
Now compare a lazy stack, with each orange directly on top of the one below in a square grid. One sphere fills a cube of side 2r, so the density is (4/3)πr³ ÷ 8r³ = π/6 ≈ 0.524. Nudging each layer into the hollows of the one below gains about 22 percentage points. If you have met packing efficiency in chemistry, this is the same 74%; Hales proved that nothing does better.
Layers sitting in hollows are hard to picture from a flat drawing. The Fermi Simulation Lab has interactive simulations for ideas that are easier to see than to read.
What can students learn from Hales's proof?
Three habits worth copying:
Find a good example first, then ask: could anything beat it?
Break an endless question into cases you can list.
Let tools do the repetitive checks, but make sure each check can be re-run. The Flyspeck team encourages readers to verify the main statement themselves, which takes about five hours on a 2 GHz CPU (Hales et al., arXiv).
When your own working goes wrong at one step, the Fermi Problem Library has a step-by-step solver that explains the reasoning rather than printing an answer.
Next time you pass a fruit stall, look at the pyramid: it took 387 years to prove that the seller got it right.
