Source-linked AI summary
Proving at Scale for Universal Algebra
João Araújo, Jan Hůla, Mikoláš Janota, Edmond W. H. Lee, Bartosz Naskręcki
TL;DR
For finite semigroups, whether finite basability is decidable remains unknown. SEMIBASE uses agents to search for bases and proofs, with Lean proofs rebuilt and kernel-checked in a whole-corpus audit. It certifies every semigroup through order 6, including proofs that the four known nonfinitely based examples have no finite basis.
Problem
For finite semigroups, whether finite basability is decidable remains unknown, and a complete catalogue of nonfinitely based semigroups of order 7 is not yet known.
Source: §1 · p. 1Method
Agents propose candidate bases, search for counter-models, and write completeness proofs that are rebuilt and checked by the Lean kernel in a whole-corpus audit.
Source: §3 · p. 3Results
Takeaways & Limitations
The catalogue also yields an inclusion order for 505 varieties and 289 hard unit-equality benchmarks for automated provers.
Source: §5 · p. 5Extending the workflow to order 7 requires streamlining techniques to discharge the long tail automatically across 836,021 semigroups.
Source: §5 · p. 5
Abstract
from arXiv · showhide
We introduce SemiBase, a project that computes and formally certifies finite identity bases for small semigroups. Deciding finite basability is undecidable for finite algebras and remains open for finite semigroups. The task requires a proof that a candidate basis is complete, or a proof that none exists, rather than a single first-order validity query. LLM-guided agents search for these proofs; a referee agent rebuilds them from source, and the Lean kernel checks the resulting corpus in a final audit. Humans choose targets and approve final outcomes. We certify every semigroup of order at most 6: all 1309 semigroups of order at most 5 and all 15973 of order 6, including proofs that the four known nonfinitely based semigroups have no finite basis. The bases for order 6 define 505 distinct varieties, whose inclusion order Vampire determines except for four pairs. The resulting catalogue is a machine-checked account of results scattered across the literature and a tested foundation for order 7.
1 Introduction
The finite-basis problem asks whether a finite set of identities captures all identities of a finite algebra, a question undecidable in general and still unresolved for finite semigroups. SEMIBASE builds a certified catalogue of small semigroups using an agent-driven proof workflow and a Lean kernel audit.
1 Introduction
- Tarski [1968] asks whether all identities of a finite algebra can be described by finitely many identities; McKenzie [1996] shows deciding this is undecidable.For finite semigroups, decidability remains unknown, though it is believed to be undecidable.Source: §1 · p. 1
- Unlike a single validity query, the semigroup problem requires certifying a candidate basis as complete or proving that no finite basis exists.The project organizes instances by finite semigroup and addresses its full equational theory.Source: §1 · p. 2
- SEMIBASE uses an autonomous agent-driven workflow, but a class is accepted only after the Lean kernel re-checks its proof in a whole-corpus audit.The referee agent triages work and settles disputes but is not trusted to verify proofs.Source: §1 · p. 2
- SEMIBASE provides Lean proofs that every semigroup of order at most 6 has a finite basis or, for four semigroups, none, covering 1,309 semigroups through order 5 and 15,973 of order 6.The project also reports an inclusion order for the 505 varieties generated by finitely based semigroups of order 6 and 289 hard unit-equality problems.Source: §1 · pp. 1–2
- The catalogue formalizes a classification previously scattered across the literature and includes the complete inclusion order of 505 varieties generated by order-6 finitely based semigroups.The contributions also include 289 hard unit-equality problems prepared for the TPTP library.Source: §1 · p. 2
2 Preliminaries
The preliminaries define semigroups, identities, and finite bases, then give examples of nilpotence, a simple finite basis, and the variety generated by a semigroup.
2 Preliminaries
- A semigroup has an associative binary operation, denoted ∗, and its order n is the number of elements on which it operates.Finite semigroups are represented by multiplication tables; distinct counts identify isomorphic and anti-isomorphic structures.Source: §2 · p. 2
- An identity u ≈ v holds when every assignment of variables into the semigroup gives equal evaluations, and a basis derives all its identities by equational deduction.A semigroup is finitely based when it has a finite identity basis.Source: §2 · p. 3
- A nilpotent semigroup has a zero absorbing every sufficiently long product, and is finitely based; the left-projection semigroup has basis xy ≈ x despite not being nilpotent.In the left-projection example, each word evaluates to its first variable, so identities are determined by whether both sides begin with the same variable.Source: §2 · p. 3
- A semigroup T belongs to the variety generated by S exactly when T satisfies every identity of S; any basis of S therefore defines that variety.The paper denotes the variety generated by S as V(S).Source: §2 · p. 3
3 The proof factory
The proof factory combines a scripted baseline with agent-led work on harder cases, then screens candidates and certifies completeness proofs through rebuilds and kernel checks.
The proof factory
- Three worker agents do the mathematics while a coordinator assigns semigroups, allocates compute, and runs independent rebuilds; a referee certifies candidate bases and resolves disputes.Humans periodically select targets and restart stalled agents; records trace proofs back through a shared log to the initiating decision.Source: §3 · p. 3
Who did what
- 94% of classes were sealed by a scripted, language-model-free baseline; the remaining 984 required individual work, with agents proposing bases, seeking counter-models, and writing proofs.Humans chose targets, approved pushes, and restarted stalled agents but wrote no proofs.Source: §3 · p. 3
From a candidate to a proof
- Successful completeness proofs rewrite every word to a normal form determined by finite features visible to the multiplication table, allowing semigroups sharing a basis to share the proof.Only the finite check on each table differs among members of a family.Source: §3 · p. 3
- 76 candidates were refuted before Lean proofs began, and 143 of 443 independent kernel checks returned proofs to their authors.After two failed attempts, or later three, a worker had to stop and report to the referee.Source: §3 · p. 4
The neighbour of L
- C8 differs from the nonfinitely based semigroup L in two multiplication-table entries, enough to cut off L’s infinite identity family; C8 is finitely based.A candidate with nine identities was refuted by an order-20 semigroup beyond the screens’ search range, and a referee-supplied equality test and normal form enabled the final proof.Source: §3 · p. 4
Where the effort went
- Sharing bases across semigroup families and searching for counter-models before Lean saved the most work, while too-short word bounds and batchwise checks cost the most.The eventual workflow sealed the catalogue through shared proofs and whole-corpus checks.Source: §3 · pp. 3–4
4 Results
The catalogue certifies every semigroup through order 6 with a finite basis or a proof that none exists. Its certificates span a wide range of sizes, and the order-6 bases yield 505 distinct varieties with a completed inclusion order.
4 Results
- All 1,309 semigroups of order at most 5 and all 15,973 of order 6 are sealed; four order-6 semigroups have Lean proofs that no finite basis exists.Every other sealed class carries a certified basis.Source: §4 · p. 4
4.1 Proof size
- 445 semigroups of order 6 have generated proofs; the median is a few hundred lines, nine exceed 100,000, and the largest is 333,557 lines.These generated proofs differ in size by four orders of magnitude; the largest proofs are mechanically generated, while 2,918 new lines for the neighbour of L took four weeks.Source: §4.1 · p. 4, Figure 1 · p. 5
4.2 Basis size and the order of varieties
- Over four fifths of the 15,524 classes sealed by family proofs have bases of at most five identities; the certified bases contain between 1 and 64 identities, with median 4.The figure shows basis sizes before Section 4.2's reduction.Source: §4.2 · p. 4, Figure 1 · p. 5
- Vampire reduces 536 certified bases from 7,919 to 1,781 identities, and the bases define 505 distinct varieties whose inclusion order has 13,325 strict inclusions.Finite evaluation completes the order, including 1,317 covering pairs and 87 maximal varieties; Vampire proves the 31 remaining pairs equivalent.Source: §4.2 · p. 5
5 Summary and Conclusions
SEMIBASE addresses the finite-basis problem for semigroups, which remains open, by building a catalogue of certified outcomes. It covers every semigroup through order 6, with the order-7 catalogue as the next target and a substantially larger scale to address.
5 Summary and Conclusions
- SEMIBASE catalogues finite identity bases for small semigroups, where the finite-basis problem remains open, and certifies either a basis or nonexistence for each covered semigroup.Identity bases are syntactic counterparts of varieties.Source: §5 · p. 5
- The catalogue covers all 1,309 semigroups of order at most 5 and all 15,973 of order 6 with Lean certificates.Agents produced proofs; a referee and whole-corpus audit made them trustworthy, while humans chose targets and approved pushes but wrote no proofs.Source: §5 · p. 5
- The authors report that attacking semigroups en masse benefits from shared bases and recurring proof techniques.They also report a long-tailed workload: many proofs are routine, but the remaining few require substantial resources.Source: §5 · p. 5
- Order 7 is the next target, with 836,021 semigroups, an order of magnitude more than order 6; the tail must be discharged more automatically.Order 6 took three months, and its final case required structural analysis before a proof could be written.Source: §5 · p. 5
A The proof factory, step by step
Figure 2 maps the route from a multiplication table to a sealed class and assigns steps to agents or the referee. It also marks two return paths for work that does not pass screening or audit.
A The proof factory, step by step
- Figure 2 lays out the steps from a multiplication table to a sealed class by who performs them.Section 3 describes the steps.Source: Figure 2 · p. 8, A The proof factory, step by step · p. 8
- Blue marks Codex-agent steps, while orange marks the referee's steps.The referee is distinguished from the agents in the figure's division of work.Source: Figure 2 · p. 8
- Dashed red arrows return refuted candidates to step 2 and proofs that fail audit to step 4.Source: Figure 2 · p. 8
B How the Lean proofs are organised
Lean proof modules combine checked candidate identities with completeness proofs, while shared files organize reusable definitions and lemmas. The order-6 campaign sealed all 15,973 classes, with a long tail of unusually large proofs and a final whole-corpus audit.
B How the Lean proofs are organised
- Each proof module checks candidate identities on the multiplication table and proves completeness using normal forms or subdirect-product decompositions.Modules state BasisFor the semigroup and its transpose; generated modules reuse an earlier semigroup’s identities and split heavy computations across files.Source: B How the Lean proofs are organised · pp. 8–9
- The shared library defines identities, satisfaction, models, derivation, and BasisFor, while each module imports only the family lemmas it needs.A fixed-commit batch’s audit module lists exactly which semigroups it covers.Source: B How the Lean proofs are organised · p. 9
- All 15,973 order-6 semigroups were sealed after the scripted pipeline handled 14,989, agents sealed 943 more, and a final audit certified the last 41 together.The 984 classes left open were handled in 102 batches; the largest single build took more than a day on one core.Source: B How the Lean proofs are organised · p. 9
- Generated proofs have a heavy tail: the median is 334 lines and the mean 7,227 among 445 semigroups, while nine proofs exceed 100,000 lines.Family proofs are shorter, with a median of 170 lines and none above 10,000; the largest generated proof has 333,557 lines.Source: B How the Lean proofs are organised · p. 9
C Effort and resources
- The finishing campaign left 390 classes by 14 August, took another 23 days, and certified the final 41 together in the audit.The records do not split compute costs between nilpotent and other classes; one nilpotent class required a 291,860-line generated proof for a basis of 3,513 identities.Source: C Effort and resources · p. 10
D Worked example: the neighbour of L
The worked example distinguishes S6_3842 from its close neighbour L through a product that differs between their multiplication tables. Its certified basis is the published 38-identity basis, and the proof uses a normal form derived from combinatorial features of words.
D Worked example: the neighbour of L
- The product x y2 x separates S6_3842 from L: under x → e and y → d, it is 0 in S6_3842 but ede ≠ 0 in L.S6_3842 consequently satisfies identities that fail in L, including xyxy ≈ xyyx.Source: D Worked example: the neighbour of L · p. 11
- The certified basis is Lee and Zhang’s [2015] Proposition 19.1: twelve schemata expand to 38 identities.The variables H, K, and T in the schemata can each be absent or stand for one further variable.Source: D Worked example: the neighbour of L · p. 11
- A nine-identity candidate failed when a 20-element semigroup satisfied it but not a required instance; replacing its ninth identity with a five-variable instance yielded an equivalent basis.Equivalence to the published basis was checked by explicit derivations in both directions, outside Lean.Source: D Worked example: the neighbour of L · p. 11
- A normal form characterizes words by their letters, simple letters, component contents, and specified relations around each simple letter.Completeness follows by showing the basis rewrites every word to its normal form and that words sharing the features have the same normal form.Source: D Worked example: the neighbour of L · p. 11
- After structural analysis supplied the criterion and normal form, an agent delivered the proof in 25 new modules with 2,918 lines and 169 theorems.The final audit certified the class with all others; the certificate states BasisFor for the table and its transpose using only the three standard axioms.Source: D Worked example: the neighbour of L · p. 11
E The four proofs that no finite basis exists
The four nonfinitely based semigroups are certified by showing that identities with arbitrarily many variables cannot be derived from identities bounded by any fixed number of variables. The formal proofs reconstruct published arguments and differ in their word families and separating properties.
E The four proofs that no finite basis exists
- The audit accepts a proof for one of four classes only when its statement exactly matches NonfinitelyBased for the catalogue table, has no hypotheses, and uses only the three standard axioms.Source: E The four proofs that no finite basis… · p. 12
- For each bound k, the proofs exhibit an identity that does not follow from identities in at most k variables, because a separating word property survives every such derivation step.Since any finite set of identities has some maximum number of variables, it cannot be a basis for these semigroups.Source: E The four proofs that no finite basis… · p. 12
- The four proofs formalize published families and arguments, including Zhang and Luo [2011] for L and Trahtman [1987] and Sapir [1988] for A1 2.For A1 2, the proof characterizes identities using a marked directed graph of the word and a parity; published tables with a different element order are checked by relabelling.Source: E The four proofs that no finite basis… · p. 12
F A representative proof
A complete Lean example for the left-zero semigroup illustrates the proof pattern: verify a basis, derive normal forms, and distinguish them by valuation.
F A representative proof
- The left-zero example certifies a one-law basis by establishing soundness and deriving every valid identity from it.The proof structure is also used for larger families of semigroups.Source: F A representative proof · pp. 13–14
- Soundness follows by computation, while every word evaluates to the valuation of its first letter.The shared definitions describe word evaluation under a variable valuation.Source: F A representative proof · pp. 12–13
- Completeness reduces words to singleton first-letter normal forms, then separates unequal heads with a two-valued valuation.A valuation assigning different values to unequal heads distinguishes the resulting normal forms.Source: F A representative proof · pp. 13–14
- Its sole law is xy≈x, matching the semigroup's left-projection multiplication.The example's multiplication returns its left argument.Source: F A representative proof · p. 13
G Computing the inclusion order
Finite evaluation of certified bases completes the inclusion order among 505 varieties, resolving four directions left undecided by prover search.
G Computing the inclusion order
- For finite semigroups S and T, V(S)⊆V(T) exactly when S satisfies T's finite basis, so finite evaluation decides inclusion.Each basis identity can be checked on all assignments of its variables in S, yielding a terminating procedure.Source: G Computing the inclusion order · p. 14
- Evaluating each certified basis on a generator of each of the 505 varieties confirms 13,321 inclusions proved by Vampire or transitivity and adds four directions undecided after 12 hours of search each; the complete order has 13,325 strict inclusions, 1,317 covering pairs, and 87 maximal varieties.Source: G Computing the inclusion order · p. 14
- Finite evaluation confirmed 13,321 inclusions found by Vampire or transitivity and added the four directions left undecided after 12-hour searches.Explicit equational derivations have since been found for three of the four directions.Source: G Computing the inclusion order · p. 14
- The bases are Lean-certified, but finite table evaluations and Vampire's equational derivations are not formalized in Lean.The inclusion itself is settled by finite checks together with certified basis completeness.Source: G Computing the inclusion order · p. 14