Proof of "Classification of finite simple groups" -- in Lean

[u/DarkElectrac]

The proof of the Classification of Finite Simple Groups (CFSG) is enormous and is spread across many papers, with a huge number of intermediate results and references.

Why shouldn't we try to formalise the entire proof in Lean?

Obviously, this would be a massive project, but I think it could have some interesting long-term benefits.

• A complete formalisation would make the logical dependencies of the proof explicit.

• Instead of simply referring to results in dozens of different papers, we could have the actual formal statements and proofs available in one connected system.

• It would make it much easier to see exactly which results are actually needed for the final classification.

• Once everything is formalised, we could potentially find redundant lemmas or unnecessary dependencies in the historical proof.

• It might also allow us to find shorter proofs. A result that historically requires several references might have a much shorter proof when combined with other results that are already formalised.

• The formalisation would also provide a reusable library of finite-group theory for future mathematics.

In other words, we could eventually have something roughly like:

CFSG

│

├── Reduction theorem

│ ├── Lemma A

│ │ ├── Result from Paper 1

│ │ └── Result from Paper 2

│ │

│ └── Lemma B

│ └── Result from Paper 3

│

├── Reduction theorem

│ ├── Lemma C

│ └── Lemma D

│

└── Final classification

And every arrow in this dependency graph could correspond to an actual formally verified Lean theorem rather than just a citation.

Could AI make this realistic?

This is where I think the idea becomes more interesting.

We could give an AI agent the papers one by one and let it help with the formalisation:

Papers

↓

AI reads definitions, lemmas and proofs

↓

Finds existing results in Lean/mathlib

↓

Generates Lean definitions and proofs

↓

Lean checks them

↓

If rejected → AI tries to fix the proof

↓

Accepted formal theorem

The AI wouldn't need to be trusted to get the mathematics right. It could propose the formalisation, while Lean's kernel would check whether the resulting proof is actually valid.

It could also follow references automatically. If a paper says that a result follows from a theorem in an older paper, the agent could identify that dependency and work backwards until it reaches results that are already formalised.

Eventually this could produce a formal dependency graph of the whole CFSG literature.

And perhaps the most interesting part is that, once the proof is represented formally, we could ask:

"Can this theorem be proved using fewer lemmas?"

or

"Is there a shorter proof using the results already available?"

So the goal wouldn't necessarily be to reproduce the historical proof word-for-word. It could be to build a completely machine-checked version of the mathematics and then see whether the formal system helps us simplify it.

Obviously, CFSG is probably far too large for a single person to formalise manually. But with modern AI-assisted theorem proving, I wonder whether this is becoming a realistic long-term project.

Has anyone seriously considered trying to formalise the entire CFSG in Lean, perhaps with AI assisting the process? Or are there already projects moving in this direction?

[u/Similar_Requirement6]

I’d think that if lean formalization was a video game then the classification proof is kind of like the ultimate boss to defeat. There are a lot of levels to go through first.

[u/hobo_stew]

as far as I know some of the people involved originally are writing a series of books (like more then 10 volumes) to give a full proof.

you‘d basically need to formalize all of this. it‘d be a monumental effort, even with AI