标题：陶哲轩宣布“等式理论计划”成功，57天完成2200万+数学关系证明

57天内，人类与AI合作完成了4694个等式之间22028942个蕴含关系的证明。大神陶哲轩宣布“等式理论计划”成功。

陶哲轩于2024年9月25日发起了“等式理论计划”，旨在探索原群等式理论空间中的蕴含关系。该项目集结了人类数学家的力量，并引入了AI工具，包括ChatGPT、Claude和GitHub Copilot。

项目启动仅9天，进度已达99.866%。目前，2200万多个需证明的蕴含关系中，8178279个已被证实，13855193个已被证伪，仅剩162个未决。陶哲轩认为，项目成功只是时间问题，并开始撰写论文。

“等式理论计划”采用数学家、AI和Lean证明辅助语言的协作方式，构建4694个magma等式之间所有蕴含关系的“蕴含图”。灵感源自陶哲轩对“去中心化”研究方式的设想。传统项目通常由少数专家进行，而借助AI工具，大规模协作成为可能。

项目聚焦于magma中不同等式之间的关系。magma是由一个集合和定义在其上的二元运算组成的代数结构。项目初期研究了包含一个方程的magma定律，最多包含四次magma操作，共4694个定律，需证明22028942个蕴含关系。

项目进展迅速，48小时内解决大量蕴含关系。第5天，剩下约300万个需解决。第9天，进度达99.866%。第19天，进度达99.9963%，写论文提上日程。第57天，项目目标达成，论文可正式开写。

陶哲轩指出，大模型工具表现“低于预期”，更多依赖经典AI，如自动定理证明器Vampire。GitHub Copilot加速代码编写，Claude创建可视化工具，ChatGPT激发灵感。项目参与者多元，包括数学家、计算机科学家、学生和业余爱好者。Lean在整合人类和机器生成的贡献方面表现出色。

项目衍生项目继续进行，陶哲轩希望这些蕴含关系能成为未来AI数学工具的基准测试。项目由陶哲轩、意大利数学家Pietro Monticone和Shreyas Srinivas共同维护。