在57天的时间内，人类与AI携手攻克了4694个等式之间的22,028,942个蕴含关系，这一壮举由数学大神陶哲轩激动地宣布为“等式理论计划”的成功。

该计划由陶哲轩于2024年9月25日正式发起，旨在探索按蕴含关系排序的原群（magma）等式理论空间。这一项目不仅汇聚了众多人类数学家的智慧，还创新性地引入了AI工具作为合作者，包括ChatGPT、Claude和GitHub Copilot等。

项目启动后，进展迅速。在仅仅9天的时间内，项目进度就达到了惊人的99.866%。截至第57天，2200多万个需要证明的蕴含关系中，已有8178279个被证实，13855193个被证伪，仅剩162个尚未解决。陶哲轩表示，宣布完全成功只是时间问题，并已开始着手撰写论文。

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

在项目中，陶哲轩等人集中研究了只包含一个方程的magma定律，这些方程最多包含四个magma操作。他们利用Lean进行验证，并借助AI工具加速代码的编写和可视化工具的创建。ChatGPT则扮演了激发数学家们灵感的小助手角色。

尽管大模型在项目中的表现略低于预期，但陶哲轩仍对其在加速代码编写和提供灵感方面的作用表示赞赏。他强调，项目的参与者非常多元化，包括处在职业生涯各个阶段的数学家和计算机科学家、学生和业余爱好者。Lean在整合人类和机器生成的贡献方面表现出色。

随着主项目里程碑的达成，“等式理论计划”的其他衍生项目仍在进行中，如研究在有限原群限制下的类似蕴含图、对蕴含图进行数据分析等。陶哲轩希望项目中的蕴含关系能够作为未来AI数学工具的基准测试，为数学研究的发展注入新的活力。

该项目的成功不仅展示了人类与AI合作的巨大潜力，也为我们探索数学世界的奥秘提供了新的方法和工具