What's new by TerryTao
·
等式理论项目：简要概览
💡
原文英文，约1400词，阅读约需6分钟。
📝
内容提要
三周前，我启动了一个合作项目，结合专业和业余数学家、自动定理证明器、AI工具和Lean证明助手，研究4694个幺半群等式定律的蕴含关系。项目已完成99.9963%，仅剩少数未解决。我们利用Lean和视觉工具分析这些关系，发现了新的代数结构，如“Asterix”和“Oberlix”定律。尽管AI工具有辅助作用，但传统自动定理证明器在核心问题上更有效。项目进展顺利，参与者多样，贡献通过Github管理。
🎯
关键要点
- 三周前启动了一个合作项目，结合专业和业余数学家、自动定理证明器、AI工具和Lean证明助手，研究4694个幺半群等式定律的蕴含关系。
- 项目已完成99.9963%，仅剩少数未解决的蕴含关系。
- 利用Lean和视觉工具分析这些关系，发现了新的代数结构，如“Asterix”和“Oberlix”定律。
- 传统自动定理证明器在核心问题上更有效，尽管AI工具有辅助作用。
- 项目进展顺利，参与者多样，贡献通过Github管理。
- 许多等式在文献中已有出现，编制了这些等式的“游览”列表。
- Birkhoff完备性定理表明，如果一个等式定律蕴含另一个，则可以通过有限次重写操作证明。
- 反蕴含的证明更为微妙，通常需要构造特定的幺半群。
- 项目中获得了“线性”幺半群的构造收益，未解决的蕴含关系数量持续减少。
- 项目运行顺利，活动在Lean Zulip频道协调，所有贡献通过Github的拉取请求流程管理。
- 正在记录所有流程和经验教训，计划撰写相关论文。
- 对项目的进展感到满意，发现了一些新的技术和构造，参与者背景多样。
- 现代AI工具在项目中有辅助作用，但在解决蕴含关系的核心任务上，传统自动定理证明器更为有效。
➡️
