等式理论项目：简要概览

三周前启动了一个合作项目，结合专业和业余数学家、自动定理证明器、AI工具和Lean证明助手，研究4694个幺半群等式定律的蕴含关系。

项目已完成99.9963%，仅剩少数未解决的蕴含关系。

利用Lean和视觉工具分析这些关系，发现了新的代数结构，如“Asterix”和“Oberlix”定律。

传统自动定理证明器在核心问题上更有效，尽管AI工具有辅助作用。

项目进展顺利，参与者多样，贡献通过Github管理。

许多等式在文献中已有出现，编制了这些等式的“游览”列表。

Birkhoff完备性定理表明，如果一个等式定律蕴含另一个，则可以通过有限次重写操作证明。

反蕴含的证明更为微妙，通常需要构造特定的幺半群。

项目中获得了“线性”幺半群的构造收益，未解决的蕴含关系数量持续减少。

项目运行顺利，活动在Lean Zulip频道协调，所有贡献通过Github的拉取请求流程管理。

正在记录所有流程和经验教训，计划撰写相关论文。

对项目的进展感到满意，发现了一些新的技术和构造，参与者背景多样。

现代AI工具在项目中有辅助作用，但在解决蕴含关系的核心任务上，传统自动定理证明器更为有效。