Kepler Conjecture
The densest packing of equal spheres is the familiar cannonball stacking arrangement.
In 1611 Kepler conjectured that no arrangement of equal spheres in three-dimensional space can exceed the density π/(3√2) ≈ 0.7405, achieved by the face-centered cubic (FCC) and hexagonal close-packed (HCP) lattices. Thomas Hales and Samuel Ferguson confirmed this in 1998 with an intricate computer-assisted proof, which the Annals of Mathematics published in 2005 after years of refereeing. The result was placed beyond doubt when the Flyspeck project, using the HOL Light and Isabelle proof assistants, completed a full formal verification published in Forum of Mathematics, Pi in 2017.
Formula
The densest packing of unit spheres in R³ has this density, achieved by both FCC and HCP arrangements.
The face-centered cubic lattice is generated by these three basis vectors; each sphere touches 12 neighbors (kissing number).
The density of a sphere packing is the fraction of space covered, taken as a limit over growing regions.
Summary
In 1611 Kepler conjectured that no arrangement of equal spheres in three-dimensional space can exceed the density π/(3√2) ≈ 0.7405, achieved by the face-centered cubic (FCC) and hexagonal close-packed (HCP) lattices. Thomas Hales and Samuel Ferguson confirmed this in 1998 with an intricate computer-assisted proof, which the Annals of Mathematics published in 2005 after years of refereeing. The result was placed beyond doubt when the Flyspeck project, using the HOL Light and Isabelle proof assistants, completed a full formal verification published in Forum of Mathematics, Pi in 2017.
