Formal verification of identity bases for small semigroups at scale
Proving at Scale for Universal Algebra
Logic in Computer Science
Summary
Figuring out the complete rules that describe small math structures called semigroups is a hard puzzle. The authors created a system named SemiBase that uses AI-assisted tools and a proof-checker to find and verify these rule sets for all semigroups with up to six elements. This work confirms known tough cases and organizes hundreds of variations systematically. It builds a trustworthy collection of results that were previously scattered and prepares the way for studying bigger semigroups.
What this means in practice
- •For formal methods engineers: Verify and certify algebraic properties of small finite structures in software and hardware systems using machine-checked proofs.
- •For automated theorem proving teams: Use AI-guided agents combined with proof assistants to automate complex algebraic proofs beyond single queries.
Authors
João Araújo, Jan Hůla, Mikoláš Janota, Edmond W. H. Lee, Bartosz Naskręcki
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.