coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Assia Mahboubi <Assia.Mahboubi AT inria.fr>
- To: coq-club AT inria.fr, projects-mkm-ig AT lists.jacobs-university.de, types-announce AT lists.seas.upenn.edu, "ssreflect AT msr-inria.inria.fr" <ssreflect AT msr-inria.inria.fr>, Map AT fourier.ujf-grenoble.fr
- Subject: [Coq-Club] 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
- [Coq-Club] A proof of the Feit Thompson theorem in Coq, Assia Mahboubi, 10/13/2012
Archive powered by MHonArc 2.6.18.