The state of finite simple groups

Stream: general

[Peiran Wu]

I am trying to understand where the Lean community are in terms of defining and proving the simplicity of finite simple groups and what can be done. Below is the picture I have now.

• Alternating groups: These have been in mathlib since quite early on I think. Antoine Chambert-Loir has formalised their simplicity and been gradually adding the proof to mathlib.
• Groups of Lie type: It seems the classical groups (linear/symplectic/unitary/orthogonal) have been defined in mathlib, without proof of simplicity. I couldn't find any exceptional groups. Ad hoc informal proofs of simplicity are sketched in Rob Wilson's book The Finite Simple Groups; the main ingredient is Iwasawa's criterion, which Antoine has formalised. A more systematic approach involves BN-pairs, and I remember seeing some progress being announced in this area. Affine algebraic groups would become relevant here, so I'm also curious about the progress on those (e.g. how much of Malle and Testerman's Linear Algebraic Groups is in Lean?).
• Sporadic groups: I'm not sure if any of the 26 sporadic groups has been defined in Lean. A lot of results that depend on the CFSG involve checking the 26 groups one by one, so a useful statement of CFSG should probably explicitly give these 26 groups.
  • The biggest obstacle is of course the Monster group. There is a Python library called mmgroup which has been used in a recent paper classifying all maximal subgroups of the Monster group, so I suppose construction is possible in a reasonable amount of time.

And regarding the classification (CFSG). The final volumes of the second-generation proof in the project initiated by Gorenstein, Lyons and Solomon are near completion now, and the whole series is apparently at around 5000 pages. Formalising this might be too ambitious to contemplate at the moment, but I would be interested to hear any thoughts about it.

[Kevin Buzzard]

I think that defining the sporadic groups should be easy, as short presentations are known for all of them or you can just define them as subgroups of symmetric groups by giving generators. Of course proving anything about these definitions will be much harder. As for porting the proof of the classification to lean, I think this should become a standard challenge for AI. In stark contrast to FLT which needs a lot of machinery, the arguments here are far more low level and it would not surprise me if AI could make a decent job of this soon. I think it would be hopeless trying to get humans to do it because the proof is so long.

[Mario Carneiro]

I remember there was a project in the long long ago to formalize finite simple groups with the aim of stating the CFSG, maybe @Floris van Doorn or @Thales know how far along it got or where the code is

[Mario Carneiro]

I think it was committed to the formal abstracts project

[Mario Carneiro]

Oh, indeed there it is: https://github.com/formalabstracts/formalabstracts/blob/master/src/group_theory/classification.lean

[Mario Carneiro]

I am really impressed how simple they got the definition of the monster group

[Edward van de Meent]

@Johan Commelin was supervisor for a few bachelor-theses defining some of these groups.

[Edward van de Meent]

(mine among them)

[Peiran Wu]

Kevin Buzzard said:

I think that defining the sporadic groups should be easy, as short presentations are known for all of them or you can just define them as subgroups of symmetric groups by giving generators. Of course proving anything about these definitions will be much harder.

Ah yes, I forgot about presentations.

[Mario Carneiro]

I guess it's not hard to define the monster group using abstract nonsense, the hard part is giving a definition which is manifestly finite, or proving that the simple presentation is finite

[Peiran Wu]

Mario Carneiro said:

Oh, indeed there it is: https://github.com/formalabstracts/formalabstracts/blob/master/src/group_theory/classification.lean

So indeed they've gone the presentations route. But it would be very hard to prove things about them (even finiteness?)

[Mario Carneiro]

I'm inclined to think that this is the "right" definition for mathlib

[Edward van de Meent]

i'm not sure...

[Mario Carneiro]

the manifestly-finite route requires you to manipulate ~165000 dimensional objects

[Edward van de Meent]

i think you want (at least for M12 and M24) to also talk about the codes that these are the automorphism group of?

[Edward van de Meent]

(thats the route i went)

[Mario Carneiro]

I think for most purposes it's fine to just have a proof sequestered away somewhere that the group is finite and possibly what its order is, and do the rest of the proof (of CFSG) over an object that doesn't take gigabytes to store

[Peiran Wu]

Edward van de Meent said:

i think you want (at least for M12 and M24) to also talk about the codes that these are the automorphism group of?

M12 and M24 are defined as automorphism groups of Steiner systems in the formal abstracts project

[Edward van de Meent]

precisely

[Peiran Wu]

Mario Carneiro said:

I think for most purposes it's fine to just have a proof sequestered away somewhere that the group is finite and possibly what its order is, and do the rest of the proof (of CFSG) over an object that doesn't take gigabytes to store

For CFSG, perhaps. One might also want to verify for example the classificaion of maximal subgroups of the Monster. And the known proof requires a computational library at the moment.

[Mario Carneiro]

Maybe, but this depends intimately on the way the proof is actually structured. But we would like the definitions to be small so that as many proofs as possible don't depend on large objects, especially in advance of knowing the details of all the proofs that touch this object from one or another angle. By the way, this question is basically why I asked https://mathoverflow.net/questions/199874/how-do-you-state-the-classification-of-finite-simple-groups

[Mario Carneiro]

The original answers to that question had a bunch of logician style technically-true-but-not-helpful definitions like "the group which is simple and has order <big number>". The work in the formal abstracts is much closer to a real answer to the question

[Johan Commelin]

I think we should port this to Lean 4. Even if AI might do the proofs, we still want to do the statement by hand.

[Johan Commelin]

Also, formal abstracts only states one half (the hard part) of the classification. I think a good warmup would be the other half: that all the groups in the list are in fact simple.

[David Michael Roberts]

Peiran Wu said:

• There is a Python library called mmgroup which has been used in a recent paper classifying all maximal subgroups of the Monster group,

What's that recent paper?

[David Michael Roberts]

Is it https://arxiv.org/abs/2304.14646 ?

[Peiran Wu]

David Michael Roberts said:

Is it https://arxiv.org/abs/2304.14646 ?

Yes

[Oisin McGuinness]

Related blog entry by Robert Wilson here .

[Peiran Wu]

Johan Commelin said:

Also, formal abstracts only states one half (the hard part) of the classification. I think a good warmup would be the other half: that all the groups in the list are in fact simple.

And that they are finite.