math-comp/odd-order

The formal proof of the Odd Order Theorem

stars

204

commits

Rocq Prover

primary language

Aug 20, 2026

updated

coq

feit-thompson-theorem

mathcomp

odd-order-theorem

ssreflect

Browse cluster: Formal Mathematics in Rocq/Coq →

README

$CI$

A formal proof of the Odd Order Theorem

The repository contains a formal verification of the Odd Order Theorem (Feit - Thompson, 1963), a landmark result of finite group theory.

The formal proof is based on the Mathematical Components library for the Coq proof assistant.

Installation

If you already have OPAM installed (a fresh or up to date version of opam 2 is required):

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-odd-order

Contributors

77 commits

37 commits

30 commits

17 commits

Similar repos

math-comp/fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

249

shared topics

math-comp/finmap

Finite sets, finite maps, multisets and generic sets

shared topics

coq-community/fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

249

shared topics

math-comp/math-comp

Mathematical Components

696

shared topics

math-comp/analysis

Mathematical Components compliant Analysis Library

247

shared topics

coq-community/gaia

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

shared topics

math-comp/hierarchy-builder

High level commands to declare a hierarchy based on packed classes

104

shared topics

coq-community/coqeal

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

shared topics

Languages

Rocq Prover

99.8%

math-comp/odd-order

The formal proof of the Odd Order Theorem

stars

204

commits

Rocq Prover

primary language

Aug 20, 2026

updated

coq

feit-thompson-theorem

mathcomp

odd-order-theorem

ssreflect

Browse cluster: Formal Mathematics in Rocq/Coq →

README

$CI$

A formal proof of the Odd Order Theorem

The repository contains a formal verification of the Odd Order Theorem (Feit - Thompson, 1963), a landmark result of finite group theory.

The formal proof is based on the Mathematical Components library for the Coq proof assistant.

Installation

If you already have OPAM installed (a fresh or up to date version of opam 2 is required):

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-odd-order

Similar repos

math-comp/fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

249

shared topics

math-comp/finmap

Finite sets, finite maps, multisets and generic sets

shared topics

coq-community/fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

249

shared topics

math-comp/math-comp

Mathematical Components

696

shared topics

math-comp/analysis

Mathematical Components compliant Analysis Library

247

shared topics

coq-community/gaia

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

shared topics

math-comp/hierarchy-builder

High level commands to declare a hierarchy based on packed classes

104

shared topics

coq-community/coqeal

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

shared topics

Contributors

77 commits

37 commits

30 commits

17 commits

Languages

Rocq Prover

99.8%