陶哲轩宣布“等式理论计划”成功，人类AI协作，57天完成2200万+数学关系证明

355 0 0

文章摘要

陶哲轩发起的“等式理论计划”在人类与AI的合作下取得显著成果。该计划旨在探索原群等式理论空间，通过数学家、AI工具和证明辅助语言Lean的协作，构建4694个magma等式间的蕴含关系图。项目启动9天内完成度已达99.866%，57天后宣布成功，22028942个蕴含关系中，8178279个被证实，13855193个被证伪，仅剩162个未解决。

项目采用去中心化研究方式，突破了传统数学研究的局限，实现了大规模协作。AI工具如ChatGPT、Claude和GitHub Copilot在项目中发挥了重要作用，尽管表现低于预期，但仍加速了代码编写和可视化工具的创建。项目参与者背景多元化，Lean在整合贡献方面表现出色。

“等式理论计划”的成功不仅标志着数学研究的新里程碑，也为未来AI数学工具的发展提供了基准测试。项目的主要维护人还包括意大利数学家Pietro Monticone和Shreyas Srinivas。尽管主项目已达成目标，但相关衍生项目仍在进行中，如研究有限原群下的蕴含图和数据分析等。