# On the proof and equivalence statement of Feit-Thompson

This, I will explain, is not a duplicate of this I think because it has 2 parts and because I have some things to add on to it.

There are 2 questions:

(1) More in-depth explanation of the answer and comments in here, and (2) What is the difference between the original proof of Feit-Thompson and the quite-modern proof of the same theorem here?

Specifically, I do not get (for the first part) why every group of odd order is solvable implies that the only simple groups of odd order are those of prime order. In the comments, what does it mean that "Solvable groups can either be prime cyclic or non-simple because by definition, solvable groups are extension of prime cyclic groups"? I know the precise definition of a solvable group but I do not understand this statement or how it plays part in the proof. If you could provide a detailed answer to (1) that'd be great.

For the second part, what exactly did Gonthier and his colleagues add to the original proof of Feit-Thompson? If it were really just formalizing bunch of 'intuitive' statements and computer-checking things, why did it take so much time, and why is Feit-Thompson's original proof in the mid-1900s still considered valid even if it had significant holes that Gonthier and his colleagues filled in? I am not looking for a generalized answer for this one, or an analogy, but someone who is quite knowlegeable about this theorem's proof.

If there is no answer for part (2), I will take an aswer to only (1) after 1-3 weeks.

• You mean parts? – Mohammad Zuhair Khan Jul 4 '18 at 7:43
• You should proofread more carefully. "the only groups of odd order are those of prime order" is false. – Derek Holt Jul 4 '18 at 7:47
• I would remark also that your two questions are at radically different levels. Question (1) is a straightforward exercise, whereas answering Question (2) would involve some much deeper mathematics. – Derek Holt Jul 4 '18 at 8:39
• Thanks for the input, I made an edit, if you could answer only (1) that'd be great – Cute Brownie Jul 4 '18 at 8:48
• A solvable group has a series of normal subgroups with abelian factor groups, so a solvable simple group must be abelian. So all of its subgroups are normal, from which you quickly deduce firstly that it is cyclic, and secondly that it must be finite of prime order. – Derek Holt Jul 4 '18 at 12:02