Kepler conjecture

Remarks

Johannes Kepler stated the claim in 1611. Gauss proved it for lattice packings in 1831. Thomas Hales announced a proof in 1998, completed with Samuel Ferguson. It reduces the problem to the minimization of a function over finitely many local configurations, and checks these by computer with linear programming bounds. The Flyspeck project, led by Hales, completed a formal proof checked by the proof assistants HOL Light and Isabelle in 2014. The bound is attained by infinitely many packings. Any stacking of hexagonal layers, each layer resting in the hollows of the one below, has density $\pi/\sqrt{18}$. The face-centred cubic and the hexagonal close packings are two of them.

Going deeper

For a student

The Kepler conjecture is the three-dimensional case of the sphere packing problem; the two-dimensional case is Thue's theorem. Unlike in the plane, the densest local cluster of balls around one ball does not extend to a packing of space, so local arguments alone fail. Hales's proof uses a carefully chosen partition of space into cells around the balls and a weighted volume score that handles this. The other dimensions where the answer is known are $8$ and $24$, by the work of Viazovska and her coauthors.