{"id":"arxiv/2610.02500","url":"https://arxiv.org/abs/2610.02500","tags":["cs.LO","math.GR"],"score":0,"title":"Proving at Scale for Universal Algebra","domain":"cs.LO","source":"arxiv","authors":["João Araújo","Jan Hůla","Mikoláš Janota","Edmond W. H. Lee","Bartosz Naskręcki"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-10-01","reactions":{}}