This post continues my series on favorite theorems of the 21st century. For an overview of the categories and my previous selections, see this earlier post.
In the category Between the Centuries—that is, theorems proved in the late 20th century but published in the early 21st century—my favorite result in Geometry and Topology, and indeed across all areas of mathematics, is the proof of Kepler’s conjecture on the densest packing of congruent balls in .
For a formal definition of packing (upper) density and its extension to higher dimensions, see this earlier post. Intuitively, however, the problem is easy to state: how can we arrange non-overlapping congruent balls in three-dimensional space so that they occupy as large a proportion of space as possible?
Two arrangements—called the cubic close packing and the hexagonal close packing—have been known for centuries and both achieve the same density One way to visualize their construction is to begin with balls whose centers lie on a cubic grid, then rearrange each horizontal layer according to the optimal hexagonal packing of circles in the plane. By shifting successive layers and bringing them closer together, one obtains a tightly interlocking three-dimensional structure.
In 1611, Johannes Kepler conjectured that no packing of congruent balls in can exceed this density. In 1831, Gauss proved the conjecture for the special case of lattice packings, where the centers of the balls form a regular lattice. The general case, however, remained stubbornly open.
The conjecture gained further prominence in 1900, when Hilbert included it in his famous list of 23 unsolved problems (as part of the 18th problem). In 1953, László Fejes Tóth reduced the problem to a finite—but astronomically large—collection of cases requiring verification. Building on this strategy and introducing extensive computational methods, Thomas Hales (T. C. Hales 2005) finally completed a proof more than four centuries after Kepler’s original conjecture.
The structure of Hales’s proof is striking. He first showed that any hypothetical counterexample would imply the existence of a finite configuration of spheres satisfying certain geometric constraints. These constraints were then translated into systems of inequalities, which were subsequently relaxed into linear inequalities suitable for analysis via linear programming.
Although the number of resulting systems was finite, it was so vast that verifying them by hand was completely infeasible. Computer solvers were therefore used to show that every such system is inconsistent, ruling out all possible counterexamples.
Because of the unprecedented scale and complexity of the computation, concerns naturally arose about the reliability of the proof. In response, Hales launched the Flyspeck Project, whose goal was to formally verify the entire argument using proof-assistant software, reducing every step back to the axioms of mathematics. This monumental effort was completed in 2015 (Thomas C. Hales et al. 2017), providing essentially complete certainty in the correctness of the proof.
Beyond settling a 400-year-old conjecture, the proof of Kepler’s conjecture stands as a landmark in the use of computers in mathematics—both as exploratory tools and as fully rigorous proof verifiers—reshaping how we think about the nature of mathematical certainty in the 21st century.