[TYPES/announce] A proof of the Feit Thompson theorem in Coq

Assia Mahboubi Assia.Mahboubi at inria.fr
Sat Oct 13 18:00:23 EDT 2012

It is our great pleasure to announce that the proof of the Odd Order Theorem
(due to Walter Feit and John G. Thompson) has now been completely
machine-checked using the Coq proof assistant.
This concludes a 6 year effort by the Mathematical Components team lead by
Georges Gonthier (MSR Cambridge) at the Inria Microsoft Research Joint Centre.

For more information, see:


The Mathematical Components Team

More information about the Types-announce mailing list