Group theory and generalizations

The Lean Pool projects whose card's first MSC2020 code is in class 20, Group theory and generalizations: 12 articles, one per card.

TheoremThe 5/8 theorem#

Proves Gustafson's 5/8 theorem — the Mathlib commuting probability of a nonabelian group is at most 5/8, with the infinite case immediate from commProb being zero — via the finite-group index bounds for the center and centralizers of noncentral elements.

Quoted from the card LeanPool/projects/five-eighths-theorem.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanFiveEighths.commProb_le_five_eighths

TheoremAperiodic and simple-group wreath-division towers#

Constructs a finite recursive wreath-division tower for every finite monoid in universe zero, with finite aperiodic or finite simple-group factors and every simple-group factor a monoid divisor of the original monoid. Implements a variant of the Diekert–Kufleitner–Steinberg local-divisor argument, with reusable monoid and semigroup division, local divisors, action coverings, wreath reassociation, and the Krasner–Kaloujnine group embedding. The endpoint permits arbitrary aperiodic factors and recursive intermediate bases; it does not assert the three-element flip-flop reduction, a single transformation-monoid strong division, or quantitative decomposition bounds.

Quoted from the card LeanPool/projects/krohn-rhodes.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • LeanPool.KrohnRhodes.krohn_rhodes_prime_decomposition (theorem; a main declaration), declared in LeanPool/KrohnRhodes/PrimeDecomposition.lean, line 1032: “Every finite monoid M in universe zero admits a finite list of finite monoid factors, each witnessed to be aperiodic or a simple group, with DivTowerWreath M factors and every simple-group factor a monoid divisor of M. An empty tower means M divides the trivial monoid. At a nonempty step, M divides F wreath B for a finite action of a finite monoid B that itself has the tail tower.” Its source, as the card gives it: “Upstream PrimeDecomposition.lean, completed September 28, 2026 at 07:36:52 UTC and publicly released at 08:48:24 UTC. Variant of Diekert–Kufleitner–Steinberg, arXiv:1111.1585, Sections 3–4, with left actions, the larger local divisor cM intersect Mc, arbitrary aperiodic factors, and recursive semigroup divisions. The stronger flip-flop and transformation-monoid claims of Theorem 4.1 are not asserted. Upstream CITATION.cff attributes the proofs primarily to Claude Code under Aditya Rao's direction.”
  • LeanPool.KrohnRhodes.krasnerKaloujnine_injective (theorem), declared in LeanPool/KrohnRhodes/Foundations/KrasnerKaloujnine.lean, line 139: “For any group G and normal subgroup N, the constructed monoid homomorphism from G to Mathlib's regular wreath product of N and G/N is injective. No finiteness assumption is required.” Its source, as the card gives it: “Upstream Foundations/KrasnerKaloujnine.lean; the classical Krasner–Kaloujnine embedding theorem.”
  • LeanPool.KrohnRhodes.LocalDivisor.localDivides (theorem), declared in LeanPool/KrohnRhodes/Foundations/LocalDivisor.lean, line 166: “For any monoid M and c in M, the local divisor on cM intersect Mc, with its twisted multiplication and identity c, is a quotient of a submonoid of M.” Its source, as the card gives it: “Diekert–Kufleitner–Steinberg, arXiv:1111.1585, Section 2.5; uses the full local divisor rather than the smaller cMc union {c}.”
Project
Sources
LeanLeanPool.KrohnRhodes.krohn_rhodes_prime_decomposition

TheoremClassification of groups of order p * q#

Classification of noncyclic finite groups of order p*q, including the prime-square direct-product case and the p<q semidirect-product normal form.

Quoted from the card LeanPool/projects/order-p-q.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanOrderPQ.exists_card_eq_prime_mul_prime_and_not_isCyclic_iff

TheoremCommon-neighbour counterexamples for Saxl graphs#

Proves that for every base size B at least two and every prescribed degree bound, there is a finite faithful primitive permutation group of at least that degree and exact base size B whose generalized Saxl graph contains two nonadjacent vertices with no common neighbor. The supporting library constructs an explicit infinite family from binary deleted permutation modules over finite fields and proves the required base-size, irreducibility, primitivity, and graph-theoretic properties.

Quoted from the card LeanPool/projects/common-neighbour-conjecture.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanSaxlCounterexamples.MainTheorems.mainTheorem

TheoremExistence of a finitely presented non-sofic group#

Constructs a finitely presented group that is not sofic, resolving the question whether every group admits arbitrarily accurate finite permutation approximations. The development combines an explicit elementary group with property T, a finite-table construction of a finitely presented group, finite-model expansion, and a local obstruction to sofic approximation.

Quoted from the card LeanPool/projects/non-sofic-group.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
  • Authors: OpenAI, Dean Cureton.
  • Source: Ten Advances in Mathematics and Theoretical Computer Science by OpenAI.
  • Project repository: openai/ten-proofs, at commit 94bc0feb.
  • Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
  • License: Apache-2.0.
  • MSC2020: 20F65, 20E22.
  • In Lean Pool: LeanPool/NonSoficGroup, from the card LeanPool/projects/non-sofic-group.yaml.
Sources
LeanSoficGroups.exists_finitelyPresented_nonsofic_group

TheoremFel's Conjecture on Syzygies of Numerical Semigroups#

Formalizes Fel's conjectural formula for syzygies of numerical semigroups.

Quoted from the card LeanPool/projects/fel-conjecture.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
  • Authors: Evan Chen, Kenny Lau, Ken Ono, Jujian Zhang.
  • Source: arXiv:2602.03716.
  • Project repository: AxiomMath/fel-polynomial.
  • Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
  • License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0, keeping its copyright line: “Copyright (c) 2026 Axiom Math”.
  • MSC2020: 20M14, 13D02.
  • In Lean Pool: LeanPool/FelConjecture, from the card LeanPool/projects/fel-conjecture.yaml.
Sources
Leanfels_conjecture

TheoremFormalisation of the Bruhat-Tits Tree#

Formalizes the Bruhat-Tits tree for GL₂ over the fraction field of a discrete valuation ring.

Quoted from the card LeanPool/projects/bruhat-tits.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanBruhatTits.BTtree · BruhatTits.BTlaplace_surjective

TheoremKurosh and Schreier subgroup theorems via covering graphs#

Proves the Kurosh subgroup theorem for arbitrary subgroups of indexed free products, with factors given by actual intersections with conjugates of the original factors and with the decomposition maps induced by their inclusions. The development constructs Bass–Serre trees, quotient graphs, graph-of-groups covers, path lifting, and normal forms. It also gives an explicit finite Schreier basis and classifies automorphisms of a finite regular Schreier action by its quotient group. The finite-graph basis infrastructure is reused from LeanPool.FiniteGraphFundamentalGroup.

Quoted from the card LeanPool/projects/kurosh.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanGraphCoveringTheory.KuroshStatement.kurosh_decomposition_with_inclusions

TheoremMarshall Hall's theorem through finite cores#

Formalizes Marshall Hall's finite-index free-factor theorem for finitely generated subgroups of finite-rank free groups. The proof extracts the finitely many suffix states of a subgroup generating set, completes the resulting partial generator actions to permutations of a finite state set, identifies the connected orbit with a finite core, and extends a geodesic spanning tree to obtain an inclusion-compatible free-product decomposition. It also exposes an explicit finite permutation separator for every finitely generated subgroup and element outside it, yielding the LERF consequence. The repository also proves binary and finite-indexed free-group instances of Grushko--Neumann rank additivity, and the arbitrary-factor binary theorem. The arbitrary-factor proof is carried by a finite labelled-graph fold, source-unfold, and monochromatic-vertex contraction reduction.

Quoted from the card LeanPool/projects/marshallhalltheorem.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanMarshallHall.marshallHall · MarshallHall.rank_freeProduct_eq_add

TheoremSmall undecidable groups and effective Adian–Rabin families#

Proves the existence of a finitely presented group with three generator slots and nine relator slots whose word problem is undecidable, and effective families with undecidable triviality having respectively four generators and eleven relators, and two generators and ten relators. The dependency closure includes computable machine-to-Thue reductions, synchronized rewriting, Borisov’s group simulator, injective HNN and Tietze compression, and general Miller–Tancer and Gordon constructions. Formalizes the algebraic results of the cited paper; its four-manifold consequences are outside this project.

Quoted from the card LeanPool/projects/small-undecidable-groups.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanUndecidability.exists_small_undecidable_presentations

TheoremUlm's theorem for countable reduced abelian p-groups#

Formalizes Ulm's classification theorem for countable reduced abelian p-groups in arbitrary Lean universes. The development constructs the transfinite Ulm filtration and invariants, proves their invariance under additive equivalence, establishes Kaplansky's one-generator extension lemma, and completes the countable back-and-forth classification. A finite-group regression distinguishes Z/4 x Z/4 from Z/2 x Z/8 at the zeroth Ulm invariant.

Quoted from the card LeanPool/projects/ulms-theorem.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanUlmsTheorem.ulm_theorem

TheoremVerified Stallings folding for finitely generated subgroups of F2#

Constructs a finite inverse automaton recognizing the subgroup generated by any finite list of signed words in the rank-two free group. Proves exact subgroup preservation and correctness of canonical reduced-word membership testing. Reusable infrastructure includes inverse-automaton walks, reduction-compatible traversal, finite fold congruences, coset potentials, flower graphs, and basis roses. Folding uses exhaustive finite search over Boolean relations; no complexity bound, core pruning, subgroup basis, intersection, or index algorithm is claimed.

Quoted from the card LeanPool/projects/stallings-folding.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • Stallings.folded_recognizer_exists (theorem; a main declaration), declared in LeanPool/StallingsFolding/Recognizer.lean, line 56: “For every finite list S of signed words on two generators, there exist a finite type of states, a base state, and a partial transition table with inverse-labelled reverse edges, such that traversing the canonical reduced word of any g in FreeGroup (Fin 2) returns to the base exactly when g lies in the subgroup generated by the word values in S. The witness is the computed flower-graph fold.” Its source, as the card gives it: “Upstream Solution.lean, completeStatement and folded_recognizer_exists.”
  • Stallings.foldWords_loopSubgroup_eq_generatorSubgroup (theorem), declared in LeanPool/StallingsFolding/Flower.lean, line 305: “For every finite input list of signed words in the rank-two free group, the based-loop subgroup of the computed folded flower graph equals the subgroup generated by the input words.” Its source, as the card gives it: “Upstream Stallings/Flower.lean.”
  • Stallings.foldedMembershipTest_eq_true_iff (theorem), declared in LeanPool/StallingsFolding/Flower.lean, line 325: “For any finite generating list S and any rank-two free-group element g, the executable folded-automaton test returns true if and only if g belongs to the subgroup generated by S. There is no efficiency guarantee for constructing the automaton.” Its source, as the card gives it: “Upstream Stallings/Flower.lean.”
Project
  • Authors: Arthur Freitas Ramos.
  • Source: Verified finite automata for finitely generated subgroups of F2.
  • Mathematical source, as the card gives it: “John R. Stallings, Topology of Finite Graphs, Inventiones Mathematicae 71 (1983), 551-565, doi:10.1007/BF02095993. This is the rank-two finite-recognizer special case, implemented through least congruences rather than a sequence of local folds.”
  • Background, as the card gives it: “Ilya Kapovich and Alexei Myasnikov, Stallings Foldings and Subgroups of Free Groups, Journal of Algebra 248 (2002), 608-668, doi:10.1006/jabr.2001.9033.”
  • Project repository: Arthur742Ramos/stallings-folding, at commit 117dde0a.
  • Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”. The card's note: “Upstream formalization.yaml records human-directed GPT-6 Codex proof development. Lean Pool porting, cleanup, and optimization were also performed by OpenAI Codex. Author attribution follows upstream.”
  • License: Apache-2.0.
  • MSC2020: 20E05, 68Q45, 03B35.
  • In Lean Pool: LeanPool/StallingsFolding, from the card LeanPool/projects/stallings-folding.yaml.
Sources
LeanStallings.folded_recognizer_exists

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.