Proving at Scale for Universal Algebra

João Araújo, Jan Hůla, Mikoláš Janota, Edmond W. H. Lee, Bartosz Naskręcki

arXivarxiv/2610.02500Oct 1, 2026cs.LOscore 0

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…

SourceJSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/arxiv/2610.02500
curl -X POST /api/v1/records/arxiv/2610.02500/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2610.02500/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'