20 September 2012 - Mathematical Components

The formalization of the Odd Order theorem has been completed September 20th 2012

“This is really the End”.

After a six year effort, members of the Mathematical Components team have completed an axiom-free formalization of the proof of the Odd Order theorem (due to Walter Feit and John Griggs Thompson), using the Coq proof assistant.

Read the announcement on the Microsoft Research website.

Read the announcement on the Inria Microsoft Research Joint Centre website.

Read “A Machine-Checked Proof of the Odd Order Theorem“,  our paper in the proceedings of the ITP 2013 conference.

Back to the Mathematical Components project pages.


This team work was led by Georges Gonthier, MSR Cambridge (UK). The other contributors are:


The whole Coq development contains in total:

  • Lines of code :                 ~170 000
  • Number of definitions :   ~4200
  • Number of theorems :     ~15 000

The part of the development which corresponds to the verification of the two books Local Analysis for the Odd Order Theorem, H. Bender and G. Glauberman (Cambridge University Press) and Character Theory for The Odd Order Theorem, T. Peterfalvi (Cambridge University Press) contains in total:

  • Lines of code :                 ~47 000  (~30%)
  • Number of definitions :   ~200       (~5%)
  • Number of theorems :     ~1300    (~10%)


Browse the progress chart (all the lights are green now).

Explore the final theory graph (scroll right and down or unzoom, the graph is big).

Download the current version of the Coq development.