Infinite Groups, Classification, and Computability
Oct 28, 2026 · @David
Axiom Math produced in October 2026 a Lean formalization of the Classification of Finite Simple Groups (CFSG).
Over 24 days, AI agents directed by Axiom's team produced about 43.1 million lines of Lean.
A natural question follows: What about infinite groups? Is there any hope for a classification there, or are infinite groups full of uncomputable questions due to being more akin to Turing Machines?
Infinite groups are far more varied than finite ones, and the reason is indeed computability: groups given by generators and relations can encode Turing machines, and the group axioms do nothing to stop it.
There is no classification of infinite groups
Nobody expects one, even for infinite simple groups. A few facts show how untamed they are:
- Too many to list. B.H. Neumann showed there are uncountably many non-isomorphic groups generated by just two elements. Only countably many finite descriptions exist, so most of these groups can't even be written down.
- Every countable group fits inside a small simple one. Every countable group embeds in a simple group generated by two elements (Hall, Schupp). In the infinite world, "simple" doesn't mean atomic and tidy; simple groups can contain arbitrary complexity.
- Monsters. Tarski monsters (Olshanskii, ~1980) are infinite groups in which every proper nontrivial subgroup is cyclic of one fixed prime order p. There are infinite finitely generated groups where every element has finite order (the Burnside problem, answered by Golod–Shafarevich and Novikov–Adian). Grigorchuk's group grows faster than any polynomial but slower than any exponential.
What does get classified are infinite groups with extra structure: finitely generated abelian groups, compact Lie groups, simple Lie groups (Killing–Cartan), and algebraic groups. The finite groups of Lie type in CFSG are essentially finite-field versions of the Killing–Cartan list. Geometric group theory gets partial results by studying groups up to large-scale geometry; Gromov's theorem, for example, says groups of polynomial growth are exactly the virtually nilpotent ones.
You can encode a Turing machine in a group
This is one of the great results of 20th-century logic.
Dehn's word problem (1911). Given a finite presentation (generators plus relations), can you decide whether a word in the generators equals the identity? Novikov (1955) and Boone (1958) built finitely presented groups where this is undecidable. Their construction encodes a Turing machine's configurations as words, with the relations simulating its transitions, so "this word is trivial" becomes "this machine halts." Markov and Post had done this earlier for semigroups. Groups were harder because inverses let you "run the machine backwards," and the construction must keep that from creating unintended equalities.
Adian–Rabin (1955–58). Almost any interesting property of a finitely presented group is undecidable from its presentation: whether it is trivial, finite, abelian, free, simple, and so on. You can't even computably tell whether a presentation defines the one-element group. Isomorphism between two presentations is undecidable too. A classification of finitely presented groups is therefore provably impossible in any algorithmic sense.
Higman's embedding theorem (1961). A finitely generated group embeds in a finitely presented group if and only if it has a recursively enumerable set of relations. "Describable by a finite presentation" and "computably enumerable" are the same thing for subgroups, so group theory is as expressive as computation itself. Later work showed every computably enumerable Turing degree occurs as the difficulty of some finitely presented group's word problem.
Topology. Every finitely presented group is the fundamental group of some 4-manifold. Markov (1958) used this to show that deciding whether two 4-manifolds are homeomorphic is undecidable.
Why finite groups are tame
The group axioms are the same in both settings; finiteness is what saves you. A finite group is a finite multiplication table, so every question about it is decidable by brute force. Turing-machine encodings need unbounded room to run.
There are hints that structure can push back against computation:
- Kuznetsov's theorem. A finitely presented simple group always has a solvable word problem. To test whether w = 1, enumerate consequences of the relations looking for w = 1. In parallel, add w = 1 as a relation and search for g = 1 for some generator g ≠ 1; simplicity guarantees one search ends.
- Boone–Higman theorem. A finitely generated group has a solvable word problem exactly when it embeds in a simple subgroup of a finitely presented group. The Boone–Higman conjecture strengthens this to "embeds in a finitely presented simple group." It is proved for hyperbolic groups (Belk–Bleak–Matucci–Zaremsky, 2023) but open in general.
- Logic. The first-order theory of groups is undecidable (Tarski), but the theory of abelian groups is decidable (Szmielew). The theory of free groups is also decidable: Tarski's problem, solved by Kharlampovich–Myasnikov and Sela.
The group axioms are simple, but "group given by generators and relations" is a full model of computation. Finite groups escape only by being finite, and even their decidable world took 15,000 pages, and now 43 million lines of Lean, to classify.
Sources
- Formalizing the Enormous Theorem — Axiom (October 26, 2026)
Further reading
Most 1950s–60s originals sit behind journal paywalls (Annals via JSTOR, Royal Society). The free links below are the originals where available, otherwise good open-access surveys of the same result.
Charles Miller's "Decision problems for groups — survey and reflections" (1992, in Springer's Algorithms and Classification in Combinatorial Group Theory) is the standard overview of the whole area. Not looked up here: B.H. Neumann (1937), Hall–Schupp embeddings, Olshanskii's Tarski monsters, Kuznetsov, Markov on 4-manifolds, and Szmielew.