Primary evidence
- The Flyspeck Project repositoryS1 · Primary research · Repository
- A formal proof of the Kepler conjectureS1 · Primary research · Paper · 2015-01-09
Flyspeck completes a formal proof of the Kepler conjecture
The completed development formalized both the mathematical text and the large computational components needed for the Kepler-conjecture proof.
What happened?
The Flyspeck project records 10 August 2014 as its completion date after constructing a formal proof of the Kepler conjecture using HOL Light and Isabelle; the official paper was released on 9 January 2015.
Why it matters
Flyspeck became a benchmark for the scale, collaboration and engineering required to make complex research mathematics fully machine-checkable.
Significance rationale: Completion of Flyspeck demonstrated that an exceptionally large research proof combining hundreds of pages of mathematics and extensive computation could be reconstructed as a proof-assistant-checked formal development.
Historical context
Earlier developments
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Human–AI collaboration
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- Formalization of known result
- Interface
- Formal, Symbolic
- AI contribution
- Human formalizers constructed the development while HOL Light and Isabelle executed trusted proof checking and verified computations.
- Human contribution
- Thomas Hales and a large international team formalized the proof, mathematical libraries and computational verification components over more than a decade.
- Verification
- Paper released · E3 · Inspectable artifact · Machine-checked
- Last reviewed
- 2026-09-15
Technical details
- Systems
- flyspeck, hol-light, isabelle
- Organizations
- —
- Problems
- kepler-conjecture
- Methods
- formalization, proof-checking, verified-computation
Sources & artifacts
- The Flyspeck Project repositoryS1 · Primary research · Repository · accessed 2026-09-15
- A formal proof of the Kepler conjectureS1 · Primary research · Paper · accessed 2026-09-15
- Flyspeck formal proof repositoryArtifact · Proof artifact
Verification history
- 2014-08-10 · Claimed · E3 · Inspectable artifact
The public Flyspeck repository records the project completion date and exposes the formal development.
- 2015-01-09 · Paper released · E3 · Inspectable artifact
The official research paper documents the completed formal proof. E3 reflects inspectable artifacts and does not mean Chronicle independently replayed the entire development.
Corrections
No corrections recorded.