陶哲轩携手AI，57天内证明2200万数学关系

近日，著名数学家陶哲轩在等式理论领域的一项重大研究项目——“等式理论计划”取得圆满成功。该项目自去年9月25日发起，旨在探索按蕴含关系排序的原群等式理论空间，经过57天的紧张合作，成功完成了4694个等式之间22028942个蕴含关系的分析。

“等式理论计划”由陶哲轩发起，汇聚了全球数学家的智慧，并将AI工具如ChatGPT、Claude和GitHub Copilot纳入合作团队。该项目从启动第一天起便展现出高效的工作节奏，仅9天时间便完成了99.866%的进度。目前，在2200万个需要证明的蕴含关系中，已有8178279个被证实，13855193个被证伪，仅有162个尚待解决。陶哲轩表示，随着论文的撰写工作逐步展开，宣布项目完全成功只是时间问题。

“等式理论计划”的核心理念是构建一个展示4694个magma等式之间所有蕴含关系的“蕴含图”。这一项目源于陶哲轩对“去中心化”研究方式的探索，通过数学家、AI工具和证明辅助语言Lean的协作，实现了大规模数学项目的大规模协作。

项目主要涉及代数领域中的magma，即由一个集合和在该集合上定义的二元运算组成的代数结构。该项目旨在找出magma中不同等式之间的等价、推出和非推出关系。例如，在11个等式中，常量公理等式蕴含了其他所有等式，而反身公理等式几乎适用于所有magma。

在项目实施过程中，陶哲轩等人集中研究了包含一个方程的magma定律，这些方程最多包含四个magma操作。通过对这些定律的分析，项目参与者们逐步解决了大量蕴含关系。

值得一提的是，该项目充分利用了AI工具在代码编写、可视化工具创建等方面的优势。虽然大模型在项目中的表现低于预期，但数学家们仍然依赖“经典AI”如自动定理证明器Vampire等，实现了高效的合作。

“等式理论计划”的成功，不仅标志着等式理论领域的重要突破，也为未来AI数学工具的基准测试提供了参考。该项目的主要维护人还包括意大利数学家Pietro Monticone和Shreyas Srinivas，两位都是Lean的重度爱好者。相信随着后续工作的推进，这一项目将在数学界和AI领域产生深远影响。