Proving at Scale for Universal Algebra
Abstract
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.
Related
- The Buchholz Algebra from the Universal Resolvent Algebra--Particle Structure, Gibbs States, and Closed-Path Expansions without Fock Representations
- Extending structures for the linear framework of Universal Algebra with applications to transposed Poisson algebras
- An Explicit Construction of Commuting Quantum KdV Hamiltonians in the Universal Virasoro Vertex Algebra
- Finite-dimensional Lie subalgebras of the universal enveloping algebra of sl(2,ℂ)
- Embeddings of matrix algebras into the universal Roe algebra
BibTeX
@misc{araujo2026proving,
title = {{Proving at Scale for Universal Algebra}},
author = {João Araújo and Jan Hůla and Mikoláš Janota and Edmond W. H. Lee and Bartosz Naskręcki},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.02500},
eprint = {2610.02500},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.02500},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Proving at Scale for Universal Algebra
AU - João Araújo
AU - Jan Hůla
AU - Mikoláš Janota
AU - Edmond W. H. Lee
AU - Bartosz Naskręcki
PY - 2026
DA - 2026/10/06
PB - arXiv
DO - 10.48550/arxiv.2610.02500
UR - https://arxiv.org/abs/2610.02500
AB - 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.
ER -