saved
Proving at Scale for Universal Algebra
Hraness wrote this summary from a saved copy of the source. Quotations are taken word for word from the source.
gist
João Araújo and coauthors report that SemiBase certified every semigroup of order at most 6 as finitely based or not. Language-model agents searched for the Lean proofs and a separate referee rebuilt them, but a class counts only after the Lean kernel audits the corpus. Humans chose the targets and wrote no proofs. The order-6 bases define 505 varieties, while Vampire's reductions and the inclusion order are not in Lean.
ideas
- Every semigroup of order at most 6 is sealed. The catalogue covers all 1,309 semigroups of order at most 5 and all 15,973 of order 6, including Lean proofs that the four known nonfinitely based ones have no finite basis.
- Agents wrote the proofs and the kernel accepted them. Codex workers proposed bases and Lean proofs, a Claude referee rebuilt the corpus, and a class counts only after a whole-corpus Lean audit.
- Humans steered the campaign and wrote no proofs. They chose targets, approved pushes, and restarted stalled agents, about 1,100 prompts over three months.
- A script sealed the bulk, then the tail stalled. The pipeline closed 14,989 of the 15,973 order-6 classes; the last 390 took 23 more days, and one neighbour of a nonfinitely based semigroup needed a structural analysis before its proof closed.
- The certified bases define 505 varieties. Vampire removed redundant identities and finite evaluation completed the inclusion order, but those Vampire proofs and table checks are not formalized in Lean.
quotes
“LLM-guided agents search for these proofs; a referee agent rebuilds them from source, and the Lean kernel checks the resulting corpus”
“Humans wrote no proofs: they chose targets, approved pushes and restarted agents”
“a class is accepted only when the Lean kernel re-checks its proof in the whole-corpus audit.”
“The Vampire proofs and table evaluations have not been formalized in Lean.”