The Unbalanced Group Theorem

The classification of finite simple groups (CFSG) has been called the biggest theorem in mathematics. It is big, not necessarily in terms of its importance, but in the sense that its proof developed over the course of decades and thousands of pages of journal articles. Two days ago Axiom announced it had formalized the proof of CFSG in 43.1 million lines of Lean. If you click on the link for the accompanying paper, you’ll find that the title of the paper is The Unbalanced Group Theorem, not The Classification of Finite Simple Groups. Why is that? The unbalanced group theorem (UGT) is a key component of the CFSG. In the course of their effort to formalize CFSG Axiom found counterexamples to an assertion that the 1986 proof of UGT depends on. The UGT, and the CFSG that depends on it, is correct, but the proof was flawed. Axiom formalized the entire CFSG but focused their paper on their new proof of the UGT. *** What exactly does the UGT say? For that matter, what is a finite simple…