I didn’t say anything about my own talk at the Prospects in Mathematics meeting. But soon afterwards I was re-reading Lee Smolin’s 2006 book *The Trouble with Physics*, and it resonated with some of the things I said.

My topic was the Classification of Finite Simple Groups, and its impact on research in many parts of mathematics and computer science.

I began with one of my favourite examples. In 1872, Jordan showed that a transitive permutation group on a finite set of size *n* > 1 contains a *derangement* (an element with no fixed points). The proof is a simple counting argument which I have discussed here. In 1981, Fein, Kantor and Schacher added the innocent-looking postscript that the derangement can be chosen to have prime power order; but the proof of this requires the Classification of Finite Simple Groups.

In outline, easy reductions show that we may assume that the group is simple and the stabiliser of a point is a maximal subgroup; so we have to show that, if *G* is a simple group and *H* a maximal subgroup of *G*, then there is a conjugacy class of elements of prime power order disjoint from *H*. This has to be done by taking the simple groups one family at a time (or one group at a time, for the sporadic groups).

The subtext of my talk was: the proof of CFSG is very long, and is the work of many hands; it is certain that the published proof contains mistakes. (The proportion of mathematics papers which are error-free is surprisingly small, especially when possible errors in cited works are taken into account.) So can we trust it, and if not, should we be using it? Mathematicians have always had as a guiding principle that we should take nobody’s word for anything, but check it ourselves; CFSG makes that principle almost impossible to follow.

I told the students that, when they arrived at university from school, they were probably told that school mathematics is not “real” mathematics, and that now they would see the real thing, with an emphasis on proofs and building on secure foundations. Now that they are about to embark on a PhD, they have to be told something similar. In a university mathematics course, they are given the statement of a famous theorem, say Cauchy’s, with an elegant proof polished by generations of mathematicians. Now they are entering territory where proofs don’t exist; they will have to build proofs themselves, and sometimes they might make mistakes.

Smolin, in his book, has some hard words to say about the sociology of string theory (a subject in which he himself has worked). He was asked to write a survey paper about quantum gravity, and wanted to include the result that string theory is a “finite theory”. If this seems a little odd, string theory (like quantum electrodynamics) is a perturbative theory, where the answer to a calculation has to be found by summing infinitely many terms. (I remember my feeling of shock when I learned this from Mike Green quite a long time ago.) In the case of QED, it is well established that the sum converges, and according to Smolin, string theorists accept that the same is true for string theory. But when he went looking for a proof of this, he found that everyone referred to a paper of Stanley Mandelstam which showed only that the first approximation was finite. It seems that the assertion that finiteness had been proved was never checked by the people who quoted it; according to Smolin, the ethos of the field was to believe that such a statement must be true.

I do believe that finite group theory avoided this horror. First, it was never “the only game in town”, monopolising grants and postdoc appointments the way that string theory did. Second, everyone knew that the proof was not complete; many people hoped it could be completed (as it eventually was – the delay was partly caused by the fact that it was a big job, and experts were reluctant to commit themselves to it), but anyone who used it noted that it was being used. There were many such papers based on the assumption of CFSG, and had it proved to be false, revising them all would have been a huge job; but at least we had a good idea where to look.

However, it is true that the proof of CFSG is so long that it is unreasonable to expect a mathematician who uses it to have read and checked the proof. This is especially true for the many uses of the theorem outside group theory (in the theory of other algebraic structures such as semigroups and loops, in number theory, in computational complexity, and so on). This is probably the biggest change in a subject which has always taken the statement “Take nobody’s word for it” as a guiding principle. (In the paper of Fein, Kantor and Schacher, the assertion about derangements of prime power order is really a lemma in the proof of the theorem that the relative Brauer group of a finite extension of a global field is infinite – whatever that means!)

What about the mistakes, which undoubtedly occur in the published proof?

We have to hope that mathematicians will continue to recognise the importance of CFSG, and will continue to apply it, and even (in the case of an honorable few) to revise and improve it. How do errors in published mathematics come to light? By several methods. People read the papers and notice a problem; or they apply the result and are led to a contradiction; or they discover something which conflicts with the statement of the theorem. We are more likely to do this if the theorem in question remains an active part of our mathematical practice than if we put it on a dusty shelf somewhere and ignore this.

I believe that CFSG is too important to be put on a dusty shelf. So I am hopeful that it will stand up to the test.

Peter – do you know Alma Steinhart’s paper, A group theory of group theory: Collaborative mathematics and the ‘uninvention’ of a 1000-page proof

http://journals.sagepub.com/doi/full/10.1177/0306312712436547

She makes some good social science points, especially about “forgetting” proofs – or rather the background knowledge and tricks of the trade needed to understand them.

Interesting paper. Apart from writing Philip Hall out of the story (I think he is only mentioned in a quoted remark of John Thompson), it is a pretty good account of what happened.

There are more things around the classification that might be mentioned in such an account. For two examples, there was John Conway’s statement in around 1981 (widely quoted) that, if anyone finds a new simple group now, they should put it in their desk drawer for a couple of years until the papers have come out; and Michael Atiyah’s statement that the length of the proof and the lack of a pattern to the sporadic groups only shows that group theorists don’t really understand what they are doing (angrily rebutted by Danny Gorenstein).

There is also the issue of the “third generation proof” based on more geometric principles, championed by Ulrich Meierfrankenfeld and others — though I haven’t heard much of this for a few years.

I do believe that it is vital that these efforts continue. Maybe there is a new idea which will make the proof shorter and clearer; this will only come to light if we continue to think about the problems.

One way the CFSG has been given some new life is via the formal proof, by Gonthier and his team, of the Odd order theorem. I don’t know if they intend to continue on with the other parts of the proof of the CFSG, but it would certainly be a natural long term goal.

Indeed so. I mentioned this in my talk. It would be a huge job. One can’t, of course, just feed the papers as written into Coq; a great deal of preliminary work is required. And this may be worse for CFSG than for the Odd Order Theorem: as is suggested in the paper that Ursula Martin recommended above, finite group theorists got into the habit of writing their articles in a highly compressed, “encoded” style.

How direct a formal translation of a proof can be definitely depends on both the nature and written style of the proof.

Steinhart writes:

“Thompson’s classification of minimal simple groups was 410 pages and published in six parts; Walter’s classification of simple groups with abelian Sylow 2-subgroups was a 109-page paper; Alperin, Brauer, and Gorenstein’s classification of simple groups with quasi-dihedral or wreathed Sylow 2-subgroups was 261 pages; Gorenstein and Harada’s classification of simple groups whose 2-subgroups are generated by at most four elements was 461 pages; and Aschbacher’s ‘classical involution’ theorem was 115 pages long.”

Feit and Thompson’s paper on the odd order theorem was 255 pages. Are the other papers written in a comparable style or does the page numbers for the other papers translate into something more extensive?

I would say that the papers got more dense as time went on, though others might dispute this. In Michigan in 1973 I was part of a seminar reading Aschbacher’s proper 2-generated core paper; it was slow going (not least because we found a mistake in the paper, which Aschbacher quickly fixed).

But there is another problem. As well as these big papers, there were a large number of smaller paper, characterising particular simple groups by centraliser of involution, for example. Each of these would need to be processed, else a mistake in one of them could invalidate the proof.

Georges Gonthier was thinking about formalising the whole of CFSG I think, but he has recently left Microsoft Research to go back to academia, and so he may not now have the resources to do it.

Here is his account of the Odd Order proof

https://hal.inria.fr/file/index/docid/816699/filename/main.pdf