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 group?
A short post like this can only go into so much detail, but I’ll see what I can do.
A group represents some kind of symmetry. Groups can be built out of simple groups sorta like the way integers can be built out of primes. See more on the comparison between simple groups and prime numbers here.
The CFSG says that every finite simple group is cyclic, alternating, of Lie type, or sporadic. The UGT is a technical result used in proving that nothing is missing from this list of possibilities.
What does it mean for a group to be “unbalanced”? This depends on a few preliminary definitions.
- Define O(G) to be the largest normal subgroup of G with an odd number of elements.
- An element t in G is called an involution if it has order 2: t is not the identity but t² is.
- The centralizer of an element t of a group G, written CG(t), is the set of elements of G that commute with t.
A group G is unbalanced if O(CG(t)) is a not a subgroup of O(G) for some involution t.
The UGT is a classification theorem for unbalanced groups.
This post brings back memories from when I was a young grad student, over 50 years ago now. I was accepted at Caltech (probably due to a recommendation from my algebra teacher Rimhak Ree), where there was a group busily working on the CFSG.
I remember centralizers of involutions being an important research topic, but I never heard of the UGT. That must have been developed after my time there.