Feit thomson proved 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.

---

From Laurent Théry
Date: Thursday 20 September 2012, 20:24
Re: [Coqfinitgroup-commits] r4105 – trunk
Hi,

Just for fun

Feit Thompson statement in Coq:

Theorem Feit_Thompson (gT : finGroupType) (G : {group gT}) : odd #|G| -> solvable G.

How is it proved?

You can see only green lights there:

http://ssr2.msr-inria.inria.fr/~jenkins/current/progress.html

and the final theory graph at:

http://ssr2.msr-inria.inria.fr/~jenkins/current/index.html

How big it is:

Number of lines ~ 170 000
Number of definitions ~15 000
Number of theorems ~ 4 200
Fun ~ enormous!

– Laurent

 

---

!!! A BIG BRAVO to Georges and the Mathematical Components project !!!

---

From Georges Gonthier 
Date: 20 September 2012, 18:16
À : Alexey Solovyev , Andrea Asperti , Assia Mahboubi , 
Cyril Cohen , Enrico Tassi , Guillaume Cano , 
Jeremy Avigad , Laurence.Rideau@sophia.inria.fr, Laurent.Thery@sophia.inria.fr, 
Maxime.Denes@inria.fr, roconnor@theorem.ca, Sean McLaughlin , 
Yves Bertot , Francois Garillot
RE: [Coqfinitgroup-commits] r4105 - trunk

  Bonjour à tous,
juste un petit message pour attirer votre attention sur ce dernier ajout, qui amène notre
grand projet à son terme. Un grand merci à tous pour avoir contribué, de près ou de loin,
à cette aventure.
  Vous avez quelque chose à fêter ce soir!
Georges

-----Original Message-----
From: coqfinitgroup-commits-bounces@lists.gforge.inria.fr [mailto:coqfinitgroup-commits-bounces@lists.gforge.inria.fr] On Behalf Of gonthier@users.gforge.inria.fr
Sent: 20 September 2012 16:46
To: coqfinitgroup-commits@lists.gforge.inria.fr
Subject: [Coqfinitgroup-commits] r4105 - trunk

Author: gonthier
Date: 2012-09-20 17:46:05 +0200 (Thu, 20 Sep 2012) New Revision: 4105

Log:
This is really the End.

Modified:
  trunk/PFsection11.v
Modified: trunk/PFsection11.v
===================================================================
--- trunk/PFsection11.v	2012-09-20 15:24:20 UTC (rev 4104)
+++ trunk/PFsection11.v	2012-09-20 15:46:05 UTC (rev 4105)
@@ -1662,14 +1662,14 @@
  rewrite subr_eq0 /= -natrM eqr_nat  [(_ * a)%N]mulnC.
  by rewrite mulnA divnK // [(q * _)%N]mulnC.
have: '[tau (mu_ 0 - zeta), tau psi] = 0.
+  have psiIZ: psi \in 'Z[irr M, HU^#]. 
+    rewrite zchar_split // rpredB.
+    - rewrite cfun_onD1 psi1 rpredB //.
+        by apply:   seqInd_on mujISC.
+      by apply/rpredZ/(seqInd_on _ lambIS2).
+    - by rewrite rpred_sum // => i _; apply: irr_vchar.
+    by rewrite scale_zchar ?mem_zchar ?Cint_Cnat // mem_irr.
  rewrite Dade_isometry ?muCF //; last first.
-    have psiIZ: psi \in 'Z[irr M, HU^#]. 
-      rewrite zchar_split // rpredB.
-      - rewrite cfun_onD1 psi1 rpredB //.
-        - by apply:   seqInd_on mujISC.
-        by apply/rpredZ/(seqInd_on _ lambIS2).
-      by rewrite rpred_sum // => i _; apply: irr_vchar.
-  by rewrite scale_zchar ?mem_zchar ?Cint_Cnat // mem_irr.
    have-> : 'A0(M) = HU^#  : class_support  (cyclicTIset defW) M.
      by rewrite -defA (FTtypeP_supp0_def _ MtypeP).
    by apply: cfun_onS (zchar_on psiIZ); rewrite subsetUl.
@@ -1683,7 +1683,7 @@
    have Tmu0: mu_ 0 \in seqIndT HU M.
      by rewrite -[mu_ 0]cfInd_prTIres mem_seqIndT.
    rewrite (seqInd_ortho _ Tmu0 (seqInd_subT lambIS2)) // /lamb.
-    apply: contraTneq (mem_irr ib) => <-; apply: prTIred_not_irr.
+    by apply: contraTneq (mem_irr ib) => <-; apply: prTIred_not_irr.
  by rewrite mulr0 oppr0.
pose chi : 'CF(G) := tau (mu_ 0 - zeta) - \sum_j eta_ 0 j.
have chiE: tau (mu_ 0 - zeta) = \sum_j eta_ 0 j + chi.
@@ -1700,15 +1700,22 @@
rewrite big1 ?addr0=> [|i NZi]; last first.
  by rewrite cfdot_cycTIiso [0 == _]eq_sym (negPf NZi).
rewrite big1 ?addr0=> [|i NZi]; last first.
-rewrite cfdot_sumr big1 // => ì1 NZi1.
+rewrite cfdot_sumr big1 // => i1 NZi1.
  by rewrite cfdot_cycTIiso  (negPf NZi) andbF.
rewrite cfdotC cfdot_sumr big1 ?mulr0 ?subr0=> [|i _]; last first.
  apply: (coherent_ortho_cycTIiso _ _ CoWtau2); rewrite ?mem_irr //.
rewrite conjC0 mulr0 subr0 mulr1.
rewrite cfdot_sumr big1 ?mulr0 ?addr0 => [|i _]; last first.
  by rewrite (orthoPl oChi) ?map_f ?mem_irr.
-rewrite sub0r conjC_nat rmorph_sign.
-move/eqP; rewrite subr_eq0=> cfdot_chi_tau.
+rewrite sub0r conjC_nat rmorph_sign => /(canRL (subrK _))/(congr1 Num.norm).
+case/esym/eqP/idPn; rewrite add0r normrM normr_sign normr_nat.
+rewrite Cnat_mul_eq1 ?rpred_nat ?Cnat_norm_Cint //; last first.
+  rewrite Cint_cfdot_vchar //.
+    rewrite rpredB ?rpred_sum // => [|j1 _]; last exact: cycTIiso_vchar.
+    rewrite Dade_vchar // zchar_split muCF // rpredB ?irr_vchar //.
+    by rewrite char_vchar // prTIred_char.
+  by have [[_ ->//]] := CoWtau2; apply: mem_zchar.
+rewrite pnatr_eq1 -eqn_mul ?indexg_gt0 // mul1n gtn_eqF //.
have ltqu: (q < u)%N.
  have [solU [_ _ _ defC]] := (solvableS sUHU sol_HU, Mtype34_facts).
  have frobUW1 := Ptype_compl_Frobenius maxM MtypeP Mtypen5.
@@ -1727,7 +1734,7 @@
have ltap: (a < p)%N.
  rewrite -(prednK (prime_gt0 pr_p)) ltnS dvdn_leq //.
  by rewrite -(subnKC (prime_gt1 pr_p)).
-admit.
+exact: ltn_trans ltap (ltn_trans pLq ltqu).
Qed.

End Eleven.

_______________________________________________
Coqfinitgroup-commits mailing list
Coqfinitgroup-commits@lists.gforge.inria.fr

http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/coqfinitgroup-commits