Overview: The Kepler conjecture asks which periodic arrangement of identical solid spheres fills the largest fraction of three-dimensional Euclidean space. It concerns packing identical spheres so that the gaps between them are minimized and the overall average density is maximized. The conjecture identifies certain close-packed stackings as optimal.

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.

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.