Subject: Ssreflect Users Discussion List
List archive
- From: Assia Mahboubi <>
- To: , , , "" <>,
- Subject: A proof of the Feit Thompson theorem in Coq
- Date: Sat, 13 Oct 2012 08:39:32 -0400
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:
http://www.msr-inria.inria.fr/Projects/math-components/feit-thompson
The Mathematical Components Team
- A proof of the Feit Thompson theorem in Coq, Assia Mahboubi, 10/13/2012
Archive powered by MHonArc 2.6.18.