Can We Make the CFSG Formalization Shorter?

NOVEMBER 5, 2026

The Classification of Finite Simple Groups (CFSG) is one of the largest results in modern mathematics. Recently, Axiom released a Lean formalization of the proof, making it possible to check the argument by computer. This is a remarkable achievement. It also raises a question: when a formal proof has tens of millions of lines, how much of it can be shared, compressed, or removed?

We used AI agents to explore this question. Starting with the existing formalization, we looked for repeated proofs, data that could be written more compactly, and dependencies that might no longer be needed.

So far, we have built a candidate source tree with 573,340 fewer lines, or about 1.3% less than the original. This is the actual difference between the two source trees. We compiled some of the changes with Lean and checked some modules that depend on them. But, due to resource limits, we have not rebuilt the whole CFSG project from scratch with all the changes applied. We do not yet know whether the final classification theorem will pass in the candidate version. The patches and reproduction instructions are public.

We worked in two steps. First, we ran a small experiment to see whether we could remove repetition from real source files. Then we scanned the full codebase for more opportunities.

Starting with 77 lines

In the first experiment, we examined six CFSG modules. We looked for proofs that could use existing lemmas and for local arguments that could be made shorter. Together, the six files originally had 2,875 lines. After nine changes, they had 2,798 lines: a reduction of 77 lines. The files were:

Here is one example. In TypeISecondWitnessComparison.lean, the theorem hallIndFam_eq_indFam_hallCore had a 28-line proof. We found that an existing theorem, hallIndFam_eq_indFam, gave the result we needed. We kept the original theorem statement and replaced its proof with a one-line call to the existing theorem. The changed module compiled with Lean.

Seventy-seven lines is a small change in a project of this size. But the experiment showed that we could find repetition in real CFSG source files, try to remove it, and check the result with Lean. We also compiled selected downstream modules to check how the changes affected them.

Searching the full codebase

The version we studied contains about 43.07 million lines of Lean source. We then explored three ways to reduce the source tree.

1. Share one implementation of a theorem. The odd order theorem, also known as the Feit–Thompson theorem, says that every finite group of odd order is solvable. Axiom's CFSG project contains two formalizations of this theorem: one in Axiom's proof code and another from the Qiuzhen project. Other parts of the classification already use related Qiuzhen code.

We tried changing an interface that used the Axiom version so that it called the Qiuzhen version instead. We wanted to see how this would change the dependencies of the full classification. The result was interesting: the saving came from sharing dependencies that were already in use, not from a shorter standalone Qiuzhen proof. After the change, the original supporting code became a candidate for removal.

Think of the two implementations as two toolboxes. If a project already carries toolbox B for other work, but one task also carries toolbox A, letting that task use B may allow the project to leave A behind. In fact, our analysis found that if we look only at the dependencies of the odd order theorem itself, switching to the Qiuzhen route makes that dependency set larger.

Removing the original supporting modules from the candidate tree saved 273,054 lines. This count includes statements, definitions, imports, and documentation in the removed files. There is also a compatibility cost: external code that imports the deleted internal modules directly would need changes. We compiled the original and replacement interfaces and some real downstream users, but we have not rebuilt the full classification.

2. Write proofs and data more compactly. Some proofs can call existing results. Some files also contain large amounts of certificate data that can be generated from a more compact construction. We combined and checked these changes, reducing the source by 66,103 lines. Most of the reduction came from certificate construction; a smaller part came from reusing and shortening proofs.

Together, these first two changes reduced the candidate source tree by 339,157 lines.

3. Check repeated imports. Lean files import other modules. If a module is already available through another suitable import path, a direct import may be unnecessary.

We scanned the project's import graph and initially found 234,496 candidate redundant imports. We repeated the analysis on the candidate tree above, excluded imports in deleted files and special cases that needed to be kept, and built a patch removing another 234,183 import lines.

We checked the headers of all modified modules and compared dependencies with a model of Lean's import loading. We also compiled some changed modules and their downstream users with Lean. The combined effect of all import changes still needs a full rebuild.

With all three changes, the candidate source tree went from 43,068,005 lines to 42,494,665 lines, a difference of 573,340 lines. The earlier 77-line experiment was separate and is not added to this total.

What does this tell us?

This exploration suggests that a large formal proof can contain work worth consolidating: multiple implementations of the same result, lemmas that can be shared, expanded data, and repeated imports.

But shorter source does not necessarily mean a shorter mathematical proof. Removing imports and compressing certificate data mainly change how the project is organized or written. Reusing an existing proof of the odd order theorem does not mean that we have found a shorter proof of the Feit–Thompson theorem.

The next step is to rebuild the project from scratch with the combined patches and check the final classification theorem. We can also look for other large theorems with shareable implementations, or trace the declarations actually used by the final theorem. We ran a small test of the latter idea on the Gorenstein–Walter theorem, but it is too early to estimate how many lines it could save across the full classification.

A more ambitious direction is to rethink how the mathematical problem and its proof are organized. Could a different approach lead to a simpler classification proof? That is harder than cleaning up the existing source and goes beyond what we have achieved here.

Actually the Lean community is also exploring how to improve existing formal proofs. For example, the VeriCodeGen workshop at NeurIPS 2026 includes the Lean Refactor Arena, a competition for rewriting proofs while keeping their theorem statements and correctness.

For us, this was also an experiment in what one person can do with AI agents. Agents can help search, suggest changes, and organize checks and reviews. The results still need clear mathematical statements, reproducible experiments, and checks by Lean.