Primary evidence
- A formal proof of the Kepler conjectureS1 · Primary research · Paper · 2015-01-09
Flyspeck launches a long-term formal proof of the Kepler conjecture
The project aimed to formalize both the written mathematical argument and the computer calculations underlying Hales's proof, eventually using HOL Light and Isabelle.
What happened?
Thomas Hales announced the Flyspeck project at the January 15–18, 2003 Joint Mathematics Meetings in Baltimore with the goal of producing a fully formal proof of the Kepler conjecture; because the exact announcement day is not preserved in the cited record, the canonical date uses the meeting opening day.
Why it matters
Flyspeck became a defining large-scale demonstration that proof assistants could audit extremely complex research mathematics end to end.
Significance rationale: Flyspeck turned the verification of a major, computer-intensive mathematical proof into a long-running collaborative formalization project spanning proof text, computation and reusable proof-assistant infrastructure.
Historical context
Earlier developments
—
Later developments
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Claimed
- Evidence level
- E2 · Research record
- AI role
- Human–AI collaboration
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Formalization of known result
- Interface
- Formal, Symbolic
- AI contribution
- Humans led the formalization while proof assistants executed trusted inference, proof checking and large verified computations.
- Human contribution
- Hales and an international collaboration organized the formalization, decomposed the original proof and implemented the formal libraries and verification pipeline.
- Verification
- Claimed · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- flyspeck, hol-light, isabelle
- Organizations
- —
- Problems
- kepler-conjecture
- Methods
- formalization, proof-checking, verified-computation
Sources & artifacts
- A formal proof of the Kepler conjectureS1 · Primary research · Paper · accessed 2026-09-15
- Joint Mathematics Meetings Baltimore 2003 programS2 · Official institutional · Official announcement · accessed 2026-09-15
Verification history
- 2003-01-15 · Claimed · E2 · Research record
The official published Flyspeck account states that Hales announced the project at the January 2003 Joint Mathematics Meetings; the AMS archive fixes the meeting to January 15–18.
Corrections
No corrections recorded.