Kepler conjecture

The conjecture that congruent spheres in three-dimensional space cannot be packed more densely than in face-centered cubic or hexagonal close packing. Its optimal density is π/√18.

Sphere packing: The study of arranging non-overlapping spheres to maximize how much space they occupy. The conjecture is the central optimal-density claim for equal spheres in three dimensions.
Johannes Kepler: A German mathematician and astronomer whose work established laws of planetary motion and advanced geometry. He proposed the close-packing bound in 1611 while considering how fruit sellers stack cannonballs.
Convex geometry: The study of convex sets and geometric properties preserved by convexity. The proof’s local estimates rely on geometric bounds for regions surrounding sphere centers.
Flyspeck project: A project that produced a formal proof of the Kepler conjecture using the HOL Light and Isabelle proof assistants. It verified the proof after the original computer-assisted argument raised concerns about checking every case.
Thue's theorem: The theorem that the densest packing of congruent circles in the plane is the hexagonal lattice packing. It is the two-dimensional analogue of the optimal-density question addressed by Kepler.
Packing density: The fraction of space occupied by objects in a packing, measured over a finite region or asymptotically. It gives the quantity the conjecture seeks to bound.
On the Six-Cornered Snowflake: A 1611 essay by Johannes Kepler exploring the geometry and causes of snowflake forms. Kepler presented his sphere-packing conjecture in this work.
Delaunay triangulation: A triangulation of points whose circumscribed spheres contain no other points in their interiors. It partitions space around sphere centers into cells used in the proof’s geometric reductions.
HOL Light: A theorem-proving system based on higher-order logic and a small trusted inference kernel. It was one of the proof assistants used to formalize the conjecture’s proof.
Sphere packing in other dimensions: The study of maximum-density arrangements of non-overlapping spheres in dimensions other than three. The three-dimensional result is one case in a broader family of dimension-dependent packing problems.

Linked from 3 pages

Honeycomb theoremRelated: Hales's work on this packing problem preceded his proof of the honeycomb conjecture.