“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.
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:
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.