14/09/07 08:06:19.55
>>275 つづき
どうもです スレ主です。
>A fully formal proof, checked with the Coq proof assistant, was announced in September 2012 by Georges Gonthier and fellow researchers at Microsoft Research and INRIA.[1]
URLﾘﾝｸ(hal.inria.fr)
A Machine-Checked Proof of the Odd Order Theorem
Abstract.
This paper reports on a six-year collaborative effort that culminated in a complete formalization of a proof of the Feit-Thompson Odd Order Theorem in the Coq proof assistant.
The formalized proof is constructive, and relies on nothing but the axioms and rules of the foundational framework implemented by Coq .
To support the formalization, we developed a comprehensive set of reusable libraries of formalized mathematics, including results in finite group theory, linear algebra, Galois theory, and the theories of the real and complex algebraic numbers.
URLﾘﾝｸ(www.msr-inria.fr)
20 September 2012 - Mathematical Components
Feit thomson proved in coq
Feit-Thompson theorem has been totally checked in Coq Thursday 20 September 2012, 18:16.
We received following mail from Georges Gonthier (see below).
It concludes the proof in Coq of the Feit-Thompson theorem.
This theorem, also named the Odd Order Theorem, is the first main result in the classification of finite groups.
This work was achieved by the team formed by addressees of Georges’ mail, team strongly led by Georges Gonthier.
It is the end of a 6-year long research effort (almost fulltime work) started in May 2006. After the Four Color theorem, this is the second impressive mathematical theorem totally proved in the Coq proof assistant.
More info can be found in this mail by Laurent Théry.
See also the dedicated page here.
URLﾘﾝｸ(www.msr-inria.fr)