Definition
The Kepler conjecture is a statement in three-dimensional geometry asserting that no arrangement of equally sized spheres filling space can achieve a higher average density than that of the face‑centered cubic (FCC) packing (or its equivalent hexagonal close packing). The maximal density is $\pi/\sqrt{18} \approx 0.74048$.
Overview
Proposed by the German astronomer and mathematician Johannes Kepler in 1611, the conjecture addresses the most efficient way to pack congruent spheres in Euclidean three‑dimensional space. For over three centuries it remained an open problem despite numerous partial results and attempts at proof. In 1998, mathematician Thomas C. Hales announced a proof that combined traditional mathematical reasoning with extensive computer verification. After a lengthy peer‑review process, a formal proof was completed in 2014 using the formal proof system HOL Light, confirming the conjecture’s validity.
Etymology / Origin
The conjecture takes its name from Johannes Kepler, who in his treatise Strena seu de Nive Sexangula (1611) discussed the densest possible arrangement of cannonballs, which he conjectured to be the FCC/hexagonal close packing observed in nature (e.g., in the stacking of oranges). The term “conjecture” reflects that Kepler originally offered the statement without proof.
Characteristics
- Mathematical setting: Concerned with packings of equal spheres in $\mathbb{R}^3$ under Euclidean metric.
- Optimal density: Proven to be $\pi/\sqrt{18}$ (≈ 74.048 %).
- Equivalence of packings: The FCC packing and the hexagonal close packing are congruent in density; any other arrangement attaining this density can be transformed into one of these two by a rigid motion.
- Proof methodology: Hales’ proof employed a reduction to a finite (but large) number of configurations, exhaustive computer‑assisted calculations, and later formal verification to eliminate potential gaps.
- Implications: The result influences fields such as discrete geometry, materials science (crystallography), coding theory, and optimization.
Related Topics
- Sphere packing problem – Generalizations to higher dimensions; the densest packings are known in dimensions 1, 2, 3, 8, and 24.
- Face‑centered cubic lattice – One of the two optimal packings described by the conjecture.
- Hexagonal close packing – The other optimal packing, geometrically distinct but density‑equivalent to FCC.
- Thomas Hales – Mathematician who provided the first complete proof.
- Formal proof verification – The use of proof assistants (e.g., HOL Light) to certify mathematical arguments.
- Kepler’s Strena (1611) – The original work in which the conjecture was first articulated.