# Kepler Conjecture

**Type:** Theorem  
**Domain:** Named Results / Geometry  
**Proposed:** 1611, Johannes Kepler  
**Proved:** 1998 (Hales, computer-assisted); 2014 (Flyspeck, fully formally verified)  
**Codex URL:** /mathematics/named-results/kepler-conjecture/  
**Entry status:** Live — v1.0 (2026-05-27)

## Summary
Cannonball/orange stacking is the densest possible sphere packing: π/√18 ≈ 74.05%.

## Two optimal arrangements
Face-centred cubic and hexagonal close packing both achieve the maximum density.

## Hales's proof strategy (1998)
Reduces infinite arrangement space to ~5,000 configurations, each checked via computer-assisted linear programming. Built on Fejes Tóth's 1953 reduction idea.

## The controversial peer review
Annals of Mathematics (2005): published with note stating reviewers "99% certain" — could not fully verify all computer calculations.

## Flyspeck project (2003–2014)
Complete machine-checked formal verification using HOL Light and Isabelle proof assistants. Completed 2014 — 403 years after Kepler's conjecture.

## Higher dimensions
Dimension 8 (Viazovska, 2016) and dimension 24 (Viazovska + collaborators, 2016) solved using modular forms. Viazovska won 2022 Fields Medal. General n-dimensional case remains open.

## Sources
### Tier 1
- Hales, T.C. (2005). A proof of the Kepler conjecture. *Annals of Mathematics*.
- Hales, T. et al. (2017). A formal proof of the Kepler conjecture. *Forum of Mathematics, Pi*.
### Tier 2
- Viazovska, M. (2017). *Annals of Mathematics*.

---
*Mathematics Codex entry v1.0 — added 2026-05-27 — thecodex.expert/mathematics/*