A Lean 4 formalization of the Krohn–Rhodes decomposition of finite monoids into aperiodic and simple-group factors. The aperiodic factors are arbitrary finite aperiodic monoids: unlike the classical prime decomposition theorem, they are not reduced to copies of the flip-flop monoid (see What it does not cover). It is registered in the Palomar registry as PALOMAR-2026-09-30-000017; see Registry entry and citation.

Theorem. Let M be a finite monoid. There are finite monoids F₁, …, Fₖ, each either aperiodic or a simple group, such that every Fᵢ that is a simple group divides M as a monoid, and finite monoids B₀ = M, B₁, …, Bₖ with Bₖ trivial, where each Bᵢ (i ≥ 1) acts on a finite set Yᵢ, such that

Bᵢ₋₁ ≺ Fᵢ ≀_Yᵢ Bᵢ for i = 1, …, k.

Here A ≺ B (A divides B) means that A is a homomorphic image of a subsemigroup of B; a monoid divides M as a monoid if it is a quotient of a submonoid of M. A finite monoid is aperiodic if all of its subgroups are trivial, or equivalently if all of its H-classes are singletons. For a monoid A and a monoid B acting on a set Y, the wreath product A ≀_Y B is A^Y × B with the product (f, b)(g, c) = (y ↦ f(c·y) g(y), bc).

Equivalently, M ≺ F₁ ≀ (F₂ ≀ (⋯ ≀ (Fₖ ≀ 1))) for suitable finite actions at each level, where 1 is the trivial monoid, so that the innermost level Fₖ ≀ 1 is a finite direct power of Fₖ. A chain as above gives such a single division because A ≀_Y B ≺ A ≀_W×Y W whenever B ≺ W, where W acts on W × Y by w·(w′, y) = (ww′, y); conversely, a single division gives a chain. This equivalence is not formalized. For k = 0 the statement says that M is trivial.

The Krohn–Rhodes theorem (1965) is the basic decomposition theorem of finite semigroup theory and of algebraic automata theory: every finite semigroup divides an iterated wreath product of finite simple groups and finite aperiodic semigroups. Diekert, Kufleitner and Steinberg call Krohn–Rhodes theory "the closest thing to a Jordan–Hölder theorem for semigroups", and Krohn–Rhodes complexity, the least number of group layers needed in such a decomposition, is defined from it. Here, as in the classical statement, every simple-group factor divides M.

The statement is in Challenge.lean, which imports only Mathlib, and it is proved in Solution.lean (namespace KrohnRhodes):

theorem krohn_rhodes_prime_decomposition (M : Type) [Monoid M] [Finite M] :
    Nonempty (KRFactorTowerGrp M)

A KRFactorTowerGrp M consists of:

• factors : List KRFactor: each factor is a finite monoid with a proof that it is either aperiodic (every element has a trivial H-class) or a simple group (a simple group structure whose underlying monoid is the factor's monoid);
• divides : DivTowerWreath M factors: the chain of divisions displayed above;
• groupFactorsDivide: every simple-group factor divides M as a monoid.

DivTowerWreath is defined by recursion on the list of factors. DivTowerWreath M [] says that M divides the trivial monoid, so M is trivial. DivTowerWreath M (F :: rest) says that there are a finite monoid B and a finite type Y on which B acts such that M divides WreathProduct F.carrier B Y and DivTowerWreath B rest holds.

The theorem depends only on the axioms propext, Classical.choice and Quot.sound, with no sorry. Comparator, configured by comparator.json, checks that the theorem proved in Solution.lean is the one stated in Challenge.lean, with the same definitions.

The theorem is due to K. Krohn and J. Rhodes, Algebraic theory of machines. I. Prime decomposition theorem for finite semigroups and machines, Trans. Amer. Math. Soc. 116 (1965), 450–464, doi:10.1090/S0002-9947-1965-0188316-1.

The proof is the local-divisor proof of V. Diekert, M. Kufleitner and B. Steinberg, The Krohn–Rhodes Theorem and Local Divisors, Fundamenta Informaticae 116 (2012), 65–77, arXiv:1111.1585, written for left actions. Theorem numbers refer to version 1 on arXiv.

• By Cayley's theorem, M acts faithfully on itself.
• Theorem 3.1: if a faithful transformation monoid (X, M) is generated by A and c ∈ A, then the constants closure of (X, M) divides the wreath product of the closures of (Xc, M_c) and of (X ⊔ N, N), where M_c is the local divisor of M at c and N is the submonoid generated by A ∖ {c}.
• Corollary 3.2: if A is a minimal generating set and c ∈ A is not a unit, then M_c and N are smaller than M, so induction on |M| reduces to groups with the constant maps adjoined. The simple groups obtained divide M, because M_c and N divide M.
• The groups are then decomposed as in the proof of Theorem 4.1. Lemma 2.9: the constants closure of a faithful group action (X, G) divides (X, U_X) ≀ (G, G), where the reset monoid U_X consists of the identity and the constant maps on X. Reset monoids are aperiodic. Corollary 2.8: a finite group divides a wreath product of simple groups that divide it; here the step along a normal subgroup N uses the Krasner–Kaloujnine embedding of G into N ≀ (G/N) instead of the proof of Proposition 2.7.

The Lean proof also differs from the paper in these ways. The local divisor is taken on cM ∩ Mc rather than cMc ∪ {c}; the paper notes that its proofs work for both. Division is semigroup division of monoids rather than strong division of transformation monoids. The towers produced by the induction are joined using associativity of the wreath product up to division. Theorem 4.1 of the paper goes on to replace each reset monoid by copies of the flip-flop monoid (Lemma 2.10 and Example 2.4); that step is not formalized.

A web search in September 2026 (Lean and Mathlib, Rocq/Coq, Isabelle and its Archive of Formal Proofs, HOL4, Agda) found no earlier machine-checked proof of the Krohn–Rhodes theorem. This is not a claim that none exists.

• Aperiodic factors are not reduced to the flip-flop. The classical statement takes every aperiodic factor to be the flip-flop monoid (U₂ in the notation of Diekert, Kufleitner and Steinberg: the identity and the two constant maps on a two-element set). This statement only requires the factors to be aperiodic. For an aperiodic M it therefore holds with M itself as the only factor; in general it separates the group structure of M, as simple groups dividing M, from aperiodic factors. The proof's aperiodic factors are reset monoids, each of which embeds in a direct power of U₂, but that step is not part of the formal statement.
• Monoids, not transformation monoids. Diekert, Kufleitner and Steinberg state Theorem 4.1 for finite transformation monoids, with strong division. The formal statement concerns the monoid M, with semigroup division.
• Monoids, not semigroups. The statement is for finite monoids. Finite semigroups are not treated separately.
• Universe 0. M ranges over Type.
• No size bounds. The bounds on the size of the decomposition in Corollaries 3.2 and 4.2 of Diekert, Kufleitner and Steinberg are not formalized.

• Function.End Q multiplies by composition, (f * g) x = f (g x), so constant maps are left zeros.
• In WreathProduct A B X, (p * q).func x = p.func (q.base • x) * q.func x and (p * q).base = p.base * q.base.
• The tower condition uses semigroup division (SgDiv). The simple-group factors divide M as monoids (KrohnRhodes.MonoidDivides: a quotient of a submonoid).

Requires elan. The toolchain (Lean 4.35.0-rc2) and Mathlib (v4.35.0-rc2) are pinned in lean-toolchain and lake-manifest.json.

lake exe cache get        # fetch Mathlib and its prebuilt cache
lake build
lake env lean Check.lean  # prints the statement and its axioms

scripts/verify-comparator.sh runs Comparator with comparator.json. It needs Linux with bubblewrap (bwrap), as in the CI workflow.

formalization.yaml records the sources, scope, authorship and review of the formalization.

The Lean definitions, statements and proofs were written by Claude Code agents under the direction of Aditya Rao, and the documentation and metadata were revised by a Claude Code agent. The models used and the review performed are listed in formalization.yaml.

Commit 1f4a7e39ba2baede5434ac48c7571a442f8d521d of this repository is registered in the Palomar registry as PALOMAR-2026-09-30-000017, version 1: https://palomar-registry.org/entry?id=PALOMAR-2026-09-30-000017&version=1. The record covers that commit only; later commits are not part of it. The registry's citation of the entry is:

@misc{palomar-2026-09-30-000017-v1,
  author = {{Aditya Rao}},
  title = {{Krohn–Rhodes decomposition of finite monoids into aperiodic and simple-group factors}},
  year = {2026},
  howpublished = {Palomar, PALOMAR-2026-09-30-000017 v1},
  url = {https://palomar-registry.org/entry?id=PALOMAR-2026-09-30-000017&version=1},
}

The first commit targeted Lean 4.28.0. This version ports it to Lean 4.35.0-rc2 and to the module system, and splits the statement from the proof. No statement changed in meaning.

• No declaration was renamed. Eight helpers in KrasnerKaloujnine.lean (section_, section_apply, krasnerLeftRaw, krasnerLeftRaw_mem, krasnerLeft, krasnerKaloujnineFun, krasnerKaloujnine_map_mul, krasnerKaloujnine_map_one) are no longer private, because public declarations use them.
• The definitions that the statement uses moved to KrohnRhodes/Defs.lean, which replaces Foundations/GreenRelations.lean, and are repeated in Challenge.lean. The theorem and krFactorTowerGrpOf moved to Solution.lean.
• Proof-only edits for the new toolchain: push_neg became push Not, haveI/letI became have/let, two simpa calls name an extra definition to unfold, and the action actW is marked @[instance_reducible]. A new linter warning about the Fintype arguments of dks_aux and dks_aux_group is switched off instead of changing their statements.
• The lakefile no longer sets maxSynthPendingDepth or relaxedAutoImplicit, so the library is elaborated with Lean's default elaboration options, as Challenge.lean is when compiled on its own.
• In Mathlib 4.35, ⊆ on sets elaborates to ≤, so one hypothesis of main_decomposition has a different elaborated form with the same meaning.
• Several docstrings were corrected.

Apache-2.0; see LICENSE. Citation metadata is in CITATION.cff.