发表机构
Universidade Nova de Lisboa; Czech Technical University in Prague; Nova Southeastern University; Adam Mickiewicz University, Poznań; Warsaw University of Technology（新里斯本大学; 布拉格捷克理工大学; 新东南大学; 波兹南亚当·密茨凯维奇大学; 华沙理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
SemiBase项目利用LLM智能体搜索证明并借助Lean内核认证，完成了阶数至多6的所有半群的有限恒等式基的正式验证，包括四个非有限基半群的证明。
AI 中文摘要
我们介绍了SemiBase项目，该项目计算并正式认证小型半群的有限恒等式基。对于有限代数，判定有限可基性是不可判定的，对于有限半群这一问题仍然开放。该任务需要证明候选基是完备的，或者证明不存在这样的基，而非单一的一阶有效性查询。LLM引导的智能体搜索这些证明；裁判智能体从源代码重建它们，Lean内核在最终审计中检查生成的语料库。人类选择目标并批准最终结果。我们认证了阶数至多6的每个半群：所有1309个阶数至多5的半群和所有15973个阶数为6的半群，包括证明四个已知的非有限基半群没有有限基。阶数为6的基定义了505个不同的簇，Vampire确定了除四对之外的包含序。生成的目录是对文献中分散结果进行机器检查的说明，也是阶数7的经过测试的基础。
英文摘要
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.
