Skip to Content.
Sympa Menu

coq-club - [Coq-Club] A proof of the Feit Thompson theorem in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A proof of the Feit Thompson theorem in Coq


Chronological Thread 
  • 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.

Top of Page