Kepler conjecture (densest packing of equal spheres in three dimensions)

Statement and density

Informally, the conjecture asserts that no arrangement of congruent spheres in 3D can exceed the density achieved by the familiar face-centered cubic (FCC) or the equivalent hexagonal close packing (HCP) arrangements. Both of those packings have the same highest known packing fraction, approximately 74.05% of space occupied by spheres.

History and proof

Johannes Kepler proposed the idea in 1611 while discussing the arrangement of cannonballs and the structure of snowflakes. The problem remained open for centuries and became a central question in mathematics and crystallography. In 1998 Thomas Hales announced a proof that combined traditional reasoning with extensive computer-assisted case analysis. Because of the scale and complexity of the computations, the proof was initially checked by referees over several years.

Formal verification and methods

To remove lingering doubts about the computer work, the Flyspeck project later formalized and fully verified Hales's result using proof assistant software; that project reported completion in the early 2010s. The overall approach reduced the infinite packing problem to a finite but large number of local configurations and then used careful estimates and computation to rule out any denser packing.

Applications and related problems

Beyond pure interest, the Kepler conjecture connects to materials science, crystallography and the study of dense particulate arrangements. It also sits alongside other sphere-packing questions in higher dimensions, where the maximal density and optimal arrangements can differ dramatically and have links to coding theory and information transmission.

Notable facts

• Both FCC and HCP achieve the conjectured maximal density; they are distinct arrangements with the same packing fraction.
• The problem led to advances in rigorous computer-assisted proof techniques and formal verification.
• For more background and historical pointers see Kepler's original statement and contemporary summaries of the result.