Stack cannonballs, pour spheres into a box, and watch order beat disorder
In 1611 Johannes Kepler had a patron to thank and no money for a present, so he wrote him a pamphlet instead. Strena Seu de Nive Sexangula — “On the Six-Cornered Snowflake” — is twenty pages on why snow falls in sixes, and it wanders through pomegranate seeds, honeycomb and the way a gunner stacks cannonballs. Somewhere in that wandering Kepler states, flatly and without argument, that the grocer’s stack “will be the tightest possible, so that in no other arrangement could more pellets be stuffed into the same container.” The arrangement fills π/√18 ≈ 74.05% of space.
Every physicist, every crystallographer and every greengrocer agreed. Nobody could prove it. Gauss removed the regular half of the problem in 1831; Hilbert put the rest on his famous list in 1900; and it stood as one of the longest-lived open questions in mathematics until Thomas Hales settled it in 1998 with an argument so dependent on machine calculation that its referees, after four years of work, could say only that they were “99% certain”. This lesson builds the stack, tries to beat it, and follows what it cost to prove that nothing does.
Start with a flat layer and put the next layer in the hollows. That is the entire construction, and it is the one every market stall and every artillery park has used for as long as there have been round things to stack. A square base of n × n gives layers of n², (n−1)², … , 1 — the square pyramidal numbers. A triangular base gives layers of triangular numbers instead. The two look like different objects and are not: they are the same lattice resting on a cube face and on a cube corner. Turn either one and the close-packed triangular layers are there, running diagonally through the pile.
Try it: Press Build it and watch the layers fall in, then switch the base from square to triangular. The sphere counts change completely — 91 against 84 for a base of six — while the arrangement of any sphere and its neighbours does not change at all. Orbit until you are looking down a sloping face of the square pyramid: that face is a triangular layer.
Lay down a close-packed layer and call it A. The second layer drops into hollows — call it B. Now look carefully at the third. Half the hollows in layer B sit directly above the spheres of A; the other half sit above the hollows of A that nobody used. Both are hollows, both hold the layer just as tightly, and choosing between them costs nothing. Take the first and you get …ABAB…, hexagonal close packing. Take the second and you get …ABCABC…, face-centred cubic. The choice comes back at every layer, forever.
Try it: Build a stack by hand, one layer at a time, then flip a coin for every layer instead. The density readout never moves off 74.05% and every interior sphere still touches twelve others, whatever you chose. Turn on the unit cell to see the cube hiding inside ABCABC — its body diagonal is exactly three layers tall — and the hexagonal prism inside ABAB.
This is the first sign of how hard the theorem is going to be. The densest packing in three dimensions is not unique: a stack nine layers tall already admits 256 different sequences, and an infinite stack admits a free binary choice at every layer — uncountably many arrangements, all tied for first place, none of them distinguished by density. A proof cannot work by finding the winner and showing it is better than the rest, because there is no winner. It has to rule out an unimaginable space of competitors while letting a continuum of ties through.
Everything so far was placed deliberately. Pour spheres into a box instead and let gravity and friction do the arranging, and the result is nothing like a crystal: the pile jams at roughly 64%, a figure called random close packing, with each sphere touching about six others rather than twelve. Pour more gently and arches survive to hold it near 55%. Shake the box and the arches collapse, spheres drop into hollows, and the density climbs — slowly, grudgingly, and only as far as crystalline patches manage to nucleate.
Try it: Pour until the box is full, note the density, then hold Shake the box and watch the trace climb off the cyan line toward the amber one. Contacts per sphere is the honest tell: disorder settles near 6, order approaches 12. Ten percentage points of space separate the pile you get by accident from the one Kepler described.
It is worth seeing the alternatives laid out, because the numbers are closer together than the pictures suggest. Stacking spheres on a plain grid — simple cubic — fills π/6 ≈ 52.36% and wastes nearly half of space. Slipping one extra sphere into the middle of each cube gives body-centred cubic at π√3/8 ≈ 68.02%, which is what iron does at room temperature. Close packing, in either of its forms, reaches π/√18 ≈ 74.05%, and no arrangement of equal spheres anywhere in three-dimensional space reaches higher.
The same layers stacked ABCABC, which hides a cube: a sphere at every corner and one at the centre of every face. The cannonball pyramid is this lattice resting on a cube face.
Found in: Copper, silver, gold, aluminium, lead — and the grocer’s oranges
The interesting number is the gap. Between what you get by accident — a poured, shaken pile at roughly 64% — and what you get by design lies about ten percentage points of space, and it is bought entirely by putting every sphere in a hollow instead of on a shoulder. Nothing sits above the dashed line, in this table or anywhere else: that is the content of the theorem.
Try it: Click through the rows and rotate each cell. Count contacts as you go — 6, then 8, then 12 — and notice that the coordination number, not the picture, is what tracks the density. The two rows without a unit cell are the measured ones: random packings have no formula, only an experiment and a number everybody agrees on.
The route to a proof was mapped in 1953, when László Fejes Tóth showed that the whole infinite question could be reduced to a minimisation over finitely many configurations of a sphere and its neighbours — and remarked that a computer might one day be able to run it. Forty-five years later Thomas Hales, with his student Samuel Ferguson, ran it: thousands of cases, roughly a hundred thousand linear programs, about three gigabytes of output, and a written argument past 250 pages. The machine was not an aid to the proof. It was a load-bearing part of it.
Hales’ response to the referees was to remove human checking altogether. The Flyspeck project, begun in 2003, restates the entire proof inside the proof assistants HOL Light and Isabelle, where every step is verified mechanically from the axioms. The last obligation closed on 10 August 2014.
Formalising the proof meant rebuilding the geometry, the case analysis and every numerical bound in a language a machine can check without trusting anyone’s judgement — including Hales’. It took eleven years and thousands of processor-hours, and the formal proof was published in 2017. The Kepler conjecture became a theorem in the strictest sense available: no step in it is taken on anybody’s authority.
Flyspeck did not only settle a question about oranges. It was the first demonstration at scale that a proof too large for any person to hold in mind can still be made trustworthy — by handing the checking to a machine that cannot be impressed, bored, or persuaded. That idea, and the machines that have since started to find proofs rather than merely check them, is where this module ends.
Try it: Scrub the year from 1611 forward and watch the status band change colour twice in four centuries. The amber stretch is 387 years of everyone being sure and nobody knowing; the violet stretch is sixteen years of a published proof that no human could check; the green begins the day a machine finished checking it.
The referees’ verdict — 99% certain, unable to verify — is the most honest sentence in the story, and Hales took it as a job description rather than an insult. The Flyspeck project spent eleven years restating every line of the argument inside proof assistants that check each step against the axioms, and closed the last obligation on 10 August 2014. What had been a claim about oranges backed by a mountain of computation became a theorem in the strictest sense the discipline has.
See also: The Packing Problem, where the same question is asked and answered about circles on a page; Kissing Numbers, for the local version of this argument around a single sphere; and The Machine Age, where machines stop checking proofs and start finding them.