Reproduce “Proving at Scale for Universal Algebra” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
João Araújo, Jan Hůla, Mikoláš Janota, Edmond W. H. Lee, Bartosz Naskręcki
SemiBase certifies finite-basis results for semigroups of order at most six. It uses scripts and agents to propose bases and counter-models, then Lean checks that each basis holds and derives every identity, or certifies no finite basis exists. The catalogue covers 1,309 semigroups through order five and 15,973 of order six, including four nonfinitely based cases; it formalizes a classification established previously.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.