Talk:Feit–Thompson theorem

Changes to outline of proof and comparison to CA group proof

A few very minor changes here to the previous text: the trivial character of A needs to be avoided if we are going to call the resulting characters of G exceptional. Also, as previously written, if we take X_1 and X_2 to be irreducible characters of A which are in the same orbit under the action of the normalizer of A, then the result when X_1 - X_2 is induced to G will be zero, not a virtual character of weight two. This is why I re-phrased things in terms of characters of the normalizer, (avoiding characters whose kernels contain A).

Messagetolove 04:41, 19 May 2007 (UTC)

Long papers

"Some of these dwarfed even the Feit–Thompson paper; one was over 1000 pages long." - Just out of curiosity... which? -- Schneelocke 21:41, 24 August 2007 (UTC)

I don't know which article the original editor was talking about, but if one were flexible enough, the two volume "paper" titled "The classification of quasithin groups." by Aschbacher and Smith is 1221 pages long. It is more or less a single long article, and is more or less a necessary part of both the original and the revised proof, though it did not appear until 2004. The math review says "In 1983, Danny Gorenstein announced the completion of the classification of the finite simple groups. All of the major constituent theorems were published by 1983 with one exception. This exception was at last removed and the classification has now been completed with the publication of the two monographs under review." A quick check of mathscinet shows lots of 100 page articles and specialized monographs of a few hundred pages, so while 1000 is a little out of the ordinary, a few hundred is not. JackSchmidt 03:26, 25 August 2007 (UTC)

I remember when I used to think a 300 page proof was long. Boy, those halcyon days of old. Now I know some proofs are so long they don't actually fit within the several books that are claimed to constitute a complete proof :-). --C S (talk) 03:05, 8 May 2008 (UTC)

Comparison with Burnside's theorem

It may be worth mentioning the (much easier) Burnside's theorem for comparison here. Tkuvho (talk) 12:11, 18 March 2010 (UTC)

There is one instance of Burnside's theorem that does not follow directly from the truth of the Feit-Thompson theorem; namely, that groups of order 2^aq^b are solvable for a and b non-negative integers, and q prime (since such groups are of even order for a>0). Of course, if p and q are odd primes, then the fact that any group of order p^aq^b is solvable (for a and b non-negative integers), follows easily from the Feit-Thompson theorem. PST 01:21, 19 March 2010 (UTC)

Shouldn't the article mention this important consequence explicitly?

Namely, that all nonabelian finite simple groups -- aka all noncyclic finite simple groups -- are of even order. Or am I missing something here?Daqu (talk) 23:58, 17 July 2011 (UTC)

Well, that statement is equivalent to the statement that all finite groups of odd order are solvable, and the analysis of the Feit-Thompson paper is concerned with proving that there is no non-Abelian simple group of odd order, so it isn't really necessary. — Preceding unsigned comment added by Messagetolove (talk • contribs) 07:22, 18 July 2011 (UTC)

Well, all true propositions are equivalent to 1 = 1, but logical equivalence is no criterion for whether a statement is "necessary" or advisable in a Wikipedia article. The audience isn't exclusively research mathematicians, as you may know. And even in professional texts, important equivalent statements are usually listed together in a "The following are equivalent" type of theorem. So I find your comment to be beside the point.Daqu (talk) 05:14, 20 July 2011 (UTC)

Well, I don't want to get drawn into a long discussion, and you are certainly entitled to your view about what I said, but in this case, it is much stronger than an abstract logical equivalence between the two statements. The actual paper is concerned with proving that there is no (non-cyclic) finite simple group of odd order with all proper subgroups solvable. If there were a non-Abelian finite simple group of odd order, there would be one of least order, and all its proper subgroups would be solvable, which is excluded by Feit-Thompson. There is nothing to stop someone making that remark somewhere in the text of the main article.Messagetolove (talk) 14:39, 20 July 2011 (UTC)

Apparently your are even averse to short discussions.Daqu (talk) 02:37, 26 July 2011 (UTC)

Coq Proof

I think this is relevant: http://www.msr-inria.inria.fr/events-news/feit-thompson-proved-in-coq — Preceding unsigned comment added by 92.205.47.184 (talk) 13:57, 24 September 2012 (UTC)

• I don't. This is an article on a bit of group theory. I don't think any mathematician would claim that use of a proof checking assistant has anything of significance to do with the theorem. Significant to the Proof-Checker, and worth mentioning on the proof checker's page, but not here. (That the proof works can be checked by hand, it's not that long. Mathematically, the formally checked proof doesn't really add anything, and surely depends on which formalisation of logic one is using?) Relevant to formal logic, or proof-setting, yes, but not to this. (Note that, for instance Ulm's Theorem doesn't mention that it is equivalent to ATR₀ over RCA₀, but that the Reverse mathematics article does.) 129.31.214.162 (talk) 12:21, 25 September 2012 (UTC)

• I think it's worth mentioning. It's a real milestone in formalization. I don't think it's worth mentioning routine formalizations in theorem articles any more, but this one (along with the four-color theorem and a few others) is special because of their difficulty etc.. The Feit-Thompson theorem is not easy to check by hand, since the proof is hundreds of pages long and quite technical. Similarly, reverse mathematics results are significant in some cases, like the Hahn-Banach theorem, and the reversal is mentioned there. As a more extreme example, Goodstein's theorem would barely be interesting if it weren't for its reverse-mathematics aspect. 69.228.171.70 (talk) 04:29, 26 September 2012 (UTC)

• • Sure, which is why it seems relevant for formalization, but not for the theorem. Reverse mathematical results are significant for theorems at times because it gives mathematical information about the theorems. That theorems, axioms, lemmata are logically equivalent is of mathematical significance to theorem. That this result has been proved formally by a computer seems irrelevant to the mathematics. (The Four-Colour theorem is different -- the proof of that was by computer, and not verifiable by hand. Its verification was thus "news-worthy".) This may be partially bias due to the original mention on the article that the theorem had been "certified" by Coq. Still not convinced it's of relevance to this article. 129.31.214.162 (talk) 14:29, 26 September 2012 (UTC)
    • By that argument, the historical background of the theorem should also be omitted, since it doesn't say anything about the mathematical content. But we usually do mention any relevant historical background in articles about theorems. If anything, I see the amount of work that went into the formalization as (among other things) confirming the theorem's significance, since someone saw it as worth all that effort, so it's relevant to the article.

      Anyway, I don't see what the issue really is here. Is formalization somehow a distasteful subject to some algebraists? (I guess I can believe that it might be.) If not, it's just a sentence or two (ok, I was thinking of adding a little more, but I'm not insistent) in the article; it's not like the formalization details are overwhelming everything else. As another example, the ongoing formalization of Hales' proof of the Kepler conjecture is IMHO quite significant, and Hales himself apparently thinks so too, since he's the one leading the effort. The Kepler conjecture article should probably say more about this than it currently does. 69.228.171.70 (talk) 20:36, 26 September 2012 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Feit–Thompson theorem. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20161119094854/http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/ to http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 11:10, 29 September 2017 (UTC)