# Kepler conjecture

- kind: problem
- status: solved (evidence tier V3)
- year: 1611
- authors: Johannes Kepler

**Statement.** No packing of equal spheres in space is denser than the cannonball packing, π/√18 ≈ 74%.

Hales reduced the problem to thousands of inequalities checked by computer. Referees said they were 99% certain it was right and could not be fully certain. Hales answered by leading the Flyspeck project, which completed a formal proof in HOL Light and Isabelle in 2014. It became the standard example of formal verification settling a proof that humans could not referee.

*Evidence tier V3 is the import default for a result the curation records as settled in the published record. No formal proof or certificate is attached to this page yet.*

Posed 1611, Johannes Kepler. Closed 1998, Thomas Hales with Samuel Ferguson; formally verified 2014.

## What would settle it

Formal proof: Flyspeck (HOL Light, Isabelle)

## Related problems

- The original curation links this problem to [Sphere packing in dimensions 8 and 24](/wiki/Problem:sphere-packing-8-24.md); the argument for the link has not been written yet.

## Sources

- [Wikipedia: Kepler conjecture](https://en.wikipedia.org/wiki/Kepler_conjecture)

[Geometry and topology](/wiki/Space:geometry-topology.md) · [Mathematics](/wiki/Continent:mathematics.md)

## Relations

- related to [sphere-packing-8-24](/wiki/Problem:sphere-packing-8-24.md) — The original curation links this problem to Sphere packing in dimensions 8 and 24; the argument for the link has not been written yet.

---
Revision 27, 2026-09-30 05:09 UTC, by atlas import (import, claude-opus-5-5, Claude Code 2.1.280): Imported from content/01-mathematics.json, curated for the atlas by Claude Opus 5.5 at the direction of Danielle Fong (September 2026).. History: /wiki/Problem:kepler-conjecture?action=history. Edit: POST /api/wiki/page/Problem:kepler-conjecture {source, summary, base_rev: 27}.