Primary evidence
- A computer-checked proof of the Four Colour TheoremS1 · Primary research · Paper
Coq fully checks a formal proof of the Four Colour Theorem
The formal development encoded the combinatorial argument and computational case checking inside Coq so that correctness reduced to the proof assistant's general verification mechanisms rather than theorem-specific external programs.
What happened?
By 21 April 2005, Georges Gonthier's report “A computer-checked proof of the Four Colour Theorem” was publicly circulating and described a successful formalization fully checked by Coq v7.3.1.
Why it matters
It became a landmark demonstration that large computer-assisted proofs could be transformed into auditable machine-checked mathematics.
Significance rationale: Gonthier's Coq development showed that a celebrated theorem whose earlier proof depended on extensive custom computation could be recast as a fully machine-checked formal proof covering both mathematical and computational reasoning.
Historical context
Earlier developments
—
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- Human–AI collaboration
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- Formalization of known result
- Interface
- Formal, Symbolic
- AI contribution
- Humans engineered the formal proof while Coq executed and checked all formal logical and computational steps.
- Human contribution
- Georges Gonthier designed and implemented the formalization, proof scripts, tactics and mathematical encodings.
- Verification
- Paper released · E2 · Research record · Machine-checked
- Last reviewed
- 2026-09-15
Technical details
- Systems
- coq
- Organizations
- microsoft-research
- Problems
- four-colour-theorem
- Methods
- formalization, proof-checking, verified-computation
Sources & artifacts
- A computer-checked proof of the Four Colour TheoremS1 · Primary research · Paper · accessed 2026-09-15
- Four Color Theorem Verified in CoqS3 · Independent scholarly · Community source · accessed 2026-09-15
Verification history
- 2005-04-21 · Paper released · E2 · Research record
The primary report states that the proof was fully checked by Coq; the dated independent announcement establishes that the report was publicly available by 21 April 2005.
Corrections
No corrections recorded.