How do you *state* the Classification of finite simple groups?

From the point of view of formal math, what would constitute an appropriate statement of the classification of finite simple groups? As I understand it, the classification enumerates 18 infinite families and 26 sporadic groups and asserts that a finite group is simple iff it is in one of these families. Now the 18 infinite families are all fairly clearly defined as cyclic groups, permutation groups, matrix groups over finite fields, etc. so I don't think there is much difficulty in defining these precisely. Much more problematic are the sporadic groups, which are "known" and hence apparently need no definition.

To give an example, since the monster group is some finite object we could just write down its Cayley table and define that to be the monster group. There are two big problems with this: (1) this table is huge and redundant, and (2) it's not easy to work with this table to prove properties of it. The main problem is that we don't think about the monster group in terms of its Cayley table, nor even as the group generated by a certain pair of $196882^2$ matrices. Instead we view it as a specific group which satisfies some properties and is uniquely defined by those properties; presumably it is in this context that a given sporadic group will show up in the course of the classification proof.

My problem is that I have no idea what those characterizing properties are. Indeed under some definitions it would rather weaken or trivialize the statement of classification, for example if I defined the sporadic groups as the simple groups that are not in the 18 families. What definition of these objects is actually used in the proof?

(Side question: 16 of the 18 families are usually collected under one label, the "groups of Lie type". Is this class definable in some uniform way, or are the definitions individualized and the name is just due to some commonalities we recognize between these families?)

• The double cover of the Baby Moster is the centralizer of an involution in the Monster. That probably was the first definition of the Baby Monster, but on the other hand the Baby Monster was proved to exist before the Monster was! Many of the the sporadic groups have several possible definitions. Originally the Monster was defined to be a group (not yet known to exist) with a certain character table. I think the question is probably too broad. Mar 13, 2015 at 12:20
• No of course not! But different people work with the Monster in different ways. A lot of its theoretical properties can be deduced from its description as an automorphism group of an algebra, which was used in its existence proof by Griess. But Robert Wilson has set it up on a computer using a double coset representation of elements, which enables at least some structural computations to be carried out on a computer. That was how some of its maximal subgroups were found. But my point is that this is much too large a topic to allow a sensible answer in this forum. Mar 13, 2015 at 12:35
• Just curious but is this not the main aim of Rob Wilson's book "The finite simple groups"? On page 3 he states "It is the chief aim of this book to explain, as far as space allows, the statement of CFSG. Thus we seek to introduce all the finite simple groups, to provide concrete constructions whenever possible, to calculate the orders of the groups, prove simplicity, ..." Mar 13, 2015 at 12:55
• @JayTaylor Yes that's right! So it takes (at least) a whole book to answer this question. Mar 13, 2015 at 13:05
• You may be interested in mathoverflow.net/questions/136880/… regarding your side-question. Mar 13, 2015 at 13:13

EDIT Nov 2023: Although I still stand by my answer below, I think that it's interesting to revisit this question now that the GLS project is in its home stretch. One of the OP's central questions is how to define the sporadic groups in a way that not only identifies them uniquely, but also reflects the properties that are used in the actual proof of the CFSG.

I think that there is no succinct answer to this question, but we can get some idea by looking at the Preface to Volume 10, which summarizes the progress to date. We see that there is a short list of key theorems that collectively imply the CFSG, and many of these have the form, "if a group has such-and-such properties then it must also have these other properties." In some cases, such as Theorem $$\mathcal{C}^\star_4$$, the statement is that if a group satisfies certain conditions, then it must be isomorphic to one of an explicit list of groups. To me, that suggests that there is a lot of leeway for formalization; for each group, you need to pick some way of defining it and proving that it exists, so that you can refer to it using a standard label, but there are probably many different ways to proceed that are all equally valid. Some options may be more efficient than others, but there is not going to be a definition that intrinsically captures all the properties of the group that you're going to need; you just have to pick some definition of the group, and prove its properties as the need arises.

ORIGINAL ANSWER: There are really two separate questions that you seem to be conflating here.

The first is how to state the CFSG in a way that could be mechanically formalized. The second is how to state the CFSG that adequately reflects how human mathematicians think about it.

For the former question, one straightforward possibility for the sporadic groups, since we know their orders, is simply to state something like, "There exists a unique simple group, not in one of the aforementioned families, of each of the following orders: 7920, 95040," etc. This is the barest possible statement that could count as a classification theorem, and for a computer, it provides (in principle) enough information to reconstruct the groups in question.

For the second question, though, there's no sharp boundary demarcating where the classification theorem ends and the detailed study of the properties of the sporadic groups begins. There's also no canonical way of describing a particular group of interest in a way that satisfies a human that he or she now "knows what the group is." But there's nothing unique about group theory here. Any sufficiently large and complicated mathematical object is going to suffer from this problem. There will be some bare-minimum way of referring to it that in principle picks it out from the amorphous universe of all mathematical objects but that fails to answer basic questions about it. There will be a continuum of theorems that answer other basic questions, shading off into questions that we can't answer. It is a matter of opinion how many questions we have to be able to answer before we can claim to have "adequately described" the object.

• Just “there exist 26 simple groups not in one of the aforementioned families” is by itself enough information to reconstruct the groups, in principle, by a computer. Mar 13, 2015 at 18:02
• @EmilJeřábek In recursively enumerable fashion, maybe, but that construction wouldn't be recursive (in some abstract sense) without specifying at least a bound on the size of the largest of those groups. Mar 13, 2015 at 18:38
• @StevenStadnicki: It’s most certainly recursive, it’s just not efficient (but neither is enumeration of all groups of the Monster’s size, as in the answer). You don’t need an a priori bound on the size of the groups, you just need to know when to stop the machine. And you know that: stop as soon as you found 26 group. Mar 13, 2015 at 19:34
• Excuse my ignorance, but what is the "GLS project"? Nov 21, 2023 at 7:43
• @TheAmplitwist, the series of books by Gorenstein, Lyons & Solomon which is also referred to as the "second generation" proof. Nov 21, 2023 at 8:16

I can't answer your general question but I can answer your side question. Almost all of the groups of Lie type are constructed as follows. You take a simple algebraic group $$G$$ defined over an algebraic closure of the prime field $$\overline{\mathbb{F}_p}$$ for some prime $$p>0$$. You then take a generalised Frobenius endomorphism $$F : G \to G$$ and consider the fixed point subgroup $$G^F = \{g \in G\mid F(g) = g\}$$. Up to a very small number of exceptions the quotient $$G^F/Z(G^F)$$ is then a finite simple group, known as a finite simple group of Lie type. Tits's very elegant theory of BN-pairs allows you to show relatively easily that $$G^F/Z(G^F)$$ is simple. I actually think the order formula for the group as a polynomial in $$q$$ also allows you to deduce quick quickly that you mostly get a pairwise non-isomorphic list.

Now the simple simply connected algebraic groups are labelled using Lie theoretic notation. For instance, if $$G$$ is $$\mathrm{SL}_n(\overline{\mathbb{F}_p})$$ then this would be of Lie type $$\mathrm{A}_n$$. Now the generalised Frobenius endomorphisms on $$G$$ are essentially classified by pairs $$(q,\phi)$$ consisting of $$q = p^a$$ a power of $$p$$ and an automorphism $$\phi$$ of the Dynkin diagram of $$G$$. For instance, in type $$\mathrm{A}_n$$ there is exactly one non-trivial automorphism of the Dynkin diagram say $$\tau$$. One then has two sets of triples $$(\mathrm{A}_n,q,\mathrm{id})$$ and $$(\mathrm{A}_n,q,\tau)$$. The first corresponds to the infinite series $$\mathrm{PSL}_{n+1}(q)$$ consisting of the projective special linear groups and the second corresponds to the series consisting of the projective special unitary groups $$\mathrm{PSU}_{n+1}(q)$$. Obviously there are some known cases where these are not simple. For instance $$\mathrm{PSL}_2(2) \cong \mathfrak{S}_3$$ and $$\mathrm{PSL}_2(3) \cong \mathfrak{A}_4$$ are not simple but if I remember rightly these are the only examples in the family $$\mathrm{PSL}_{n+1}(q)$$.

Annoyingly there is one group of Lie type which cannot be described in this way, namely the Tits group. This is the derived subgroup of the Ree group $${}^2\mathrm{F}_4(2)$$ and is usually denoted $${}^2\mathrm{F}_4(2)'$$. Many people working in groups of Lie type would consider this to be a Sporadic group because of this reason. However, as everyone knows by now that there are 26 sporadic finite simple groups you would like quite stupid claiming there to be 27.

Edit: You may find the recent book "Linear algebraic groups and finite groups of Lie type" by Malle and Testerman enlightening. Section 24 of the book specifically talks about constructing finite simple groups of Lie type in quite a readable way. Specifically have a look at Remark 24.9, Theorem 24.17 and Remark 24.18.