About the census
What is proved in Lean
For each of the 15,973 semigroups of order six in GAP Smallsemi 0.7.2, a theorem: either a finite list of identities is a basis, that is, the identities hold and every identity of the semigroup follows from them by equational logic, or no finite basis exists. One theorem collects them all, SemiBase.order6_classification. The Lean kernel checks every proof, and the proofs use no axioms beyond propositional extensionality, quotient soundness and choice. Sources, build instructions and the checks of the tables: nasqret/semibase-order6, archived on Zenodo as doi:10.5281/zenodo.23109225.
What is not proved in Lean
- The shortest known bases come from the certified ones by removing identities that follow from the others, with the prover Vampire; their equivalence with the certified bases rests on Vampire's proofs. Shortest known means shortest found, not proved minimal.
- The inclusions between the varieties are proved by Vampire, and the non-inclusions by semigroups of order six that lie in one variety and not in the other. 4 inclusions are undecided.
- That Smallsemi lists every semigroup of order six once, up to isomorphism and anti-isomorphism, is taken from GAP and the literature.
What was known
That exactly four semigroups of order six are not finitely based was shown by Lee, Li and Zhang (2012), and Lee and Zhang (2015) treat the semigroups of order six in detail. For most of the finitely based ones, 14,534 of the 14,600 semigroups without an identity element, finite basability follows there from sufficient conditions, which show that a finite basis exists without writing one down. The census gives an explicit basis for every one of them.
How the proofs work
Most proofs are transfers. If a semigroup S with a certified basis lies in the variety of a semigroup T, and T satisfies the basis of S, then every identity of T holds in S and so follows from the basis: the basis of S is a basis of T. The transfers differ in how S lies in the variety of T. Each semigroup page names the method of its proof.
| Proof | Classes | Idea |
|---|---|---|
| transfer from order ≤ 5 | 9,685 | S has order at most five and is a subsemigroup of this one (the final sweep of these transfers, and earlier waves) |
| embedding transfer | 1,740 | S is a subsemigroup of this one |
| divisor transfer | 2,728 | S is a quotient of a subsemigroup of this one |
| direct-power transfer | 589 | S is a subsemigroup of a direct power of this one |
| subdirect product | 195 | this semigroup is a subdirect product of two factors; the proof combines their bases |
| inflation | 58 | this semigroup is an inflation of a smaller one; the proof adapts the basis of that one |
| nilpotent certificate | 26 | all products of a fixed number of elements are equal to the zero; a generated certificate lists the identities between short words |
| heavy generated transfer | 63 | transfers of the final sweep that needed much heavier generated proofs |
| other generated proof | 365 | generated adapters and wrappers of transfers found by the campaign's search |
| individual proof | 13 | proofs written for one semigroup or a few, among them C₈ |
| family proof | 482 | one basis, proved once to derive every identity of every semigroup of a family; on each table only the identities of the basis are checked |
| wrapper | 25 | thin wrappers that restate proofs made earlier |
| no finite basis | 4 | the four proofs that no finite basis exists |
Conventions
Elements are numbered 1 to 6 as in Smallsemi (0 to 5 in Lean), and a table gives the product of the row element and the column element. An identity u ≈ v is written with the variables x, y, z, t, … in order of first occurrence and with powers for repeated letters, so x²yx stands for xxyx. V[k] is the variety generated by [6, k], with k the smallest number among its generators. A class that is not self-dual stands for two semigroups, a table and its transpose; a basis read backwards is a basis of the transpose. The links to Lean point to commit 5804539 of the repository.
Credits
Created and curated by @nasqret. The Lean proofs were written by language-model agents in a campaign from June to September 2026, described in Proving at Scale for Universal Algebra, MATH-AI workshop, NeurIPS 2026. The reduced bases and the order of the varieties were computed with Vampire by the bases-min tools of Mikoláš Janota. The tables come from GAP Smallsemi by A. Distler and J. D. Mitchell. The source of this website is nasqret/semibase-site.
References
- A. Distler and J. D. Mitchell, Smallsemi, a library of small semigroups, GAP package, version 0.7.2.
- E. W. H. Lee, J. R. Li and W. T. Zhang, Minimal non-finitely based semigroups, Semigroup Forum 85 (2012) 577–580.
- E. W. H. Lee and W. T. Zhang, Finite basis problem for semigroups of order six, LMS J. Comput. Math. 18 (2015) 1–129.
- P. Perkins, Bases for equational theories of semigroups, J. Algebra 11 (1969) 298–314.
- M. V. Sapir, Problems of Burnside type and the finite basis property in varieties of semigroups, Math. USSR-Izv. 30 (1988) 295–314.
- A. N. Trahtman, Some finite infinitely basable semigroups, Ural. Gos. Univ. Mat. Zap. 14 (1987) 128–131.
- M. V. Volkov, The finite basis problem for finite semigroups, Sci. Math. Jpn. 53 (2001) 171–199.
- W. T. Zhang and Y. F. Luo, A new example of a minimal nonfinitely based semigroup, Bull. Aust. Math. Soc. 84 (2011) 484–491.
Built 2026-10-02 from commit 5804539aee8e20acc0fa8efc01510a3806a0daa8.