文章摘要
【关 键 词】 方程理论、数学进展、自动证明、AI辅助、众包研究
陶哲轩领导的方程理论项目取得了显著进展，目前完成度已达99.9963%。该项目汇集了专业和业余数学家、自动定理证明器、AI工具以及证明辅助语言Lean，旨在描述4694条幺半群方程定理间的蕴含关系。项目自9月25日启动以来，已成功证明8178279个蕴含关系为真，13854531个为假，仅剩826个未解决。陶哲轩通过个人日志记录了项目每天的进展。
项目团队利用众包方式，结合编译效率和传递性，推导出广泛的蕴含关系集合。他们还利用蕴含图的对偶对称性进行简化，并开发了可视化工具来检查蕴含图的各个部分。例如，方程1491和65分别被称为”Obelix law”和”Asterix law”，这些方程及其蕴含关系正在被研究和可视化。
陶哲轩还编制了一份”导览”，介绍了这些方程在文献中的历史和应用，包括一些曾出现在Putnam数学竞赛中的方程和定义了”中心幺半群”的方程168。根据Birkhoff完备性定理，如果一个方程定理蕴含另一个，那么它可以通过有限次重写操作来证明，但所需的重写次数可能相当长。
在反蕴含关系的证明中，他们通过搜索小型有限幺半群来获得反例，但有些反蕴含关系需要构造无限幺半群来证明。这些构造方法与集合论中的forcing技术有相似之处。
项目遵循标准的GitHub实践，通过拉取请求和问题跟踪来协调贡献。陶哲轩对项目取得的进展非常满意，认为许多最初的期望已经实现。他们发现了新的技术和构造，用来证明一个给定的方程理论不蕴含另一个，并通过系统性搜索发现了一些具有有趣特征的奇特代数结构。
尽管陶哲轩原本期待现代AI工具能在项目中做出重大贡献，但实际上它们以辅助、次要的方式被使用。对于解决蕴含关系这一核心任务，更传统的自动定理证明器表现更好。然而，对于剩余的大约700个不适合使用传统工具处理的蕴含关系，陶哲轩认为现代AI可能会发挥更重要的作用。
原文和模型
【原文链接】 阅读原文 [ 2223字 | 9分钟 ]
【原文作者】 新智元
【摘要模型】 moonshot-v1-32k
【摘要评分】 ★★★★★
