A team led by Thomas Hales has announced a formal proof of the Kepler conjecture – one of the oldest problems in geometry – which states that no packing of equally sized spheres in 3-dimensional space is more efficient than the face-centred cubic packing (pictured right), or hexagonal close packing.

These packings are both around 74% efficient ($\pi /\sqrt{18}$ to be precise), and consist of layers of spheres arranged in a hexagonal grid; the difference between them is that in hexagonal close packing, every layer sits directly above the one two layers below, whereas the face-centred cubic has three different grid positions when seen from above. Randomly dropping in spheres achieves a density of around 65%, and no other packing has been found to be more efficient than these – conjectured to be optimal by Johannes Kepler in 1611.

The Flyspeck project, headed by Thomas Hales, has been labouring since 1998 (when Hales announced his and Ferguson’s proof of the Kepler conjecture) to construct a formal computer proof of the result. The 1998 proof is by exhaustion (checking all possible cases), and referees have said they are 99% certain of it. The Flyspeck proof is constructed using a combination of the formal proof assistants Isabelle and HOL Light and starts from basic axioms to make sure the statement is thoroughly proved.

The announcement, which was made on 10th August, includes a description of the methods used, as well as links to download the entire code of the project. While previously, this result was proved and definitely true, it’s now definitely definitely true, and greengrocers all over the world, who’ve been packing oranges this way for decades, can now be sure they’re definitely right.

Further Reading

Announcing Completion – FLYSPECK project

Proof confirmed of 400-year old fruit stacking problem at New Scientist

A proof of the Kepler conjecture – Thomas Hales’ original “proof”

Developments in formal proofs by Thomas Hales on the arXiv

Kepler’s Conjecture on Theorem of the Day