Primary evidence
- A Machine-Checked Proof of the Odd Order TheoremS1 · Primary research · Paper · 2013-07-22
Coq completes a machine-checked formal proof of the Odd Order Theorem
The project formalized the theorem together with a substantial mathematical library spanning group theory, linear algebra, Galois theory and real/complex algebraic numbers.
What happened?
The ITP 2013 paper reports a complete constructive formalization of the Feit–Thompson Odd Order Theorem in Coq, relying only on the axioms and rules of Coq's foundational framework.
Why it matters
It raised the demonstrated scale and depth of machine-checked research mathematics and strengthened the library infrastructure later available to automation and AI systems.
Significance rationale: The six-year Coq formalization of the Feit–Thompson Odd Order Theorem demonstrated that proof assistants could sustain a deep research-level argument while simultaneously building reusable libraries across finite group theory, algebra and number systems.
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
- Human authors constructed the formal proof while Coq checked every formal inference under its foundational rules.
- Human contribution
- The collaboration formalized the mathematics, engineered reusable libraries and developed proof methodology and tooling needed for the large project.
- Verification
- Paper released · E2 · Research record · Machine-checked
- Last reviewed
- 2026-09-15
Technical details
- Systems
- coq
- Organizations
- microsoft-research, inria
- Problems
- odd-order-theorem
- Methods
- formalization, proof-checking, mathematical-library
Sources & artifacts
- A Machine-Checked Proof of the Odd Order TheoremS1 · Primary research · Paper · accessed 2026-09-15
Verification history
- 2013-07-22 · Paper released · E2 · Research record
The peer-reviewed ITP paper documents the complete Coq formalization; machine checking reflects Coq verification and does not mean Chronicle independently replayed the full development.
Corrections
No corrections recorded.