来源：量子位 | 公众号 QbitAI
鱼羊 一水 发自 凹非寺
57天，
人类和AI合作
搞定了4694个等式之间22028942个蕴含关系！
大神陶哲轩激动宣布：
等式理论计划
，成功。
“等式理论计划”，由陶哲轩本人在2024年9月25日发起，目的是探索按蕴含关系排序的原群（magma）等式理论空间。
特别的是，在这个项目里，陶哲轩不仅集合了人类数学家的力量，还把
AI工具
纳入了合作者的范围，包括
ChatGPT
、
Claude
和
GitHub Copilot
。
项目发起当日就正式启动，仅仅9天，项目进度就达到了
99.866%
。
而现在，在2200万+个需要证明的蕴含关系中，8178279个已被证实，13855193个已被证伪，仅有162个还悬而未决。
按陶哲轩的说法，就是离“宣布完全成功”基本只是“时间问题”：
因此，我们现在已经开始着手撰写论文了。
什么是“等式理论计划”
还是先来扒一扒陶哲轩这回究竟是整了个什么样的活儿。
简单说，“等式理论计划”是指：
采用”数学家+AI（包括自动定理证明系统和大模型）+证明辅助语言Lean”这样的协作方式，构建一个展示
4694个
magma等式（最多四次使用magma操作）之间所有蕴含关系的 “蕴含图”。
首先，这个计划的最初灵感源于陶哲轩本人对“
去中心化
”研究方式的畅想。
传统上，大部分数学研究项目都由少数专业数学家（通常1~5名）进行，每个人都对自己的部分更专业，且彼此可以相互验证。
不过也是因为存在验证环节，组织更大规模的数学项目（尤其是需要涉及公众贡献），一直具有挑战性。
而现在，通过AI工具以及Lean这样的证明辅助语言，数学项目的大规模协作变得可能。
打前阵的就有
开源社区寻找梅森素数的成功尝试
，在这个代号GIMPS的志愿项目中，任何拥有强大PC或GPU的人都可以加入寻找梅森素数。
虽然证明助手这样的AI工具在这个项目里用得还不多，但表达的精神是类似的。
因此，在开展等式理论计划之前，陶哲轩就打算搞一个实验：
在一个数学项目中，聚齐专业/业余数学家、AI工具、证明辅助语言Lean等，一同干大事！
受去年MathOverflow上一个等式问题的启发，这一次，陶哲轩将目光瞄准了代数领域中的magma。
交换恒等式和常量恒等式之间是否存在等价关系？
抛开具体问题不谈，这里主要想说明magma
涉及等式之间的关系
。
简单来说，magma是一个代数结构，它由一个集合和一个在该集合上定义的二元运算组成，但不要求满足任何额外的代数性质，如结合律、交换律等。
而等式理论计划，就是要找出magma中不同等式之间的等价、推出和非推出关系。
就拿上面这11个等式来看，最终的关系图be like：
可以看出，常量公理等式（1）蕴含了其他所有等式，即如果1成立，那么其他等式也自动成立；而反身公理等式（11）由于最宽松（x=x），几乎所有的magma都满足这个公理。
回到计划本身，陶哲轩等人在初始阶段集中研究了那些
只包含一个方程的magma定律
，这些方程最多包含四个magma操作（即二元运算）。
举个例子，如果我们有一个magma（M，∗），其中M是元素的集合，∗是定义在M上的二元运算。
则一个“最多四次使用magma操作”的表达式如下：
其中𝑎,𝑏,𝑐,𝑑,𝑒都是集合M中的元素，每次∗的使用都算作一次magma操作。
这样的等式定律有
4694个
，由于每个定律都可能蕴含其他4693个定律（一个定律不能蕴含自身），因此总共有4694*(4694-1) = 22,028,942个可能的蕴含关系需要被证明或反驳。
这里的蕴含关系包括“蕴含”和“反蕴含”，其中“蕴含”关系又涉及到两种类型：
更多项目细节，陶哲轩在项目日志中，留下了非常详细的记录——
9天进度99.866%，大模型有用但“表现低于预期”
简单总结“等式理论计划”的进度，就是一个字：
快
。
陶哲轩本人都说
：
这个项目的进度远超我的预期。
有多快？
仅仅
48小时
，很大一部分蕴含关系就已“解决在望”。
项目启动
第5天
，项目参与者们已经从最初的约2200万条蕴含关系中解决了大量简单蕴含，只剩下约300万的数量尚待解决。
项目启动
第9天
，随着首次重大重构的完成——合作者们改进了magma的运算符号，以使Lean代码的编译速度显著加快，以及一些研究问题的推进，项目完成度一举从
87%
跃升到了
99.866%
。
第19天
，项目进度来到
99.9963%
。陶哲轩在他的博客文章中提及，写论文的事已经提上日程，并且可能包含数十名作者。
GitHub显示该项目有45位贡献者：
到了11月21日，也就是项目
第57天
，随着主项目最后一个未解决的蕴含关系被搞定（待验证），“等式理论计划”目标已宣告达成。
论文可以正式开写了。
陶哲轩透露，论文的框架早已拟好，但后续还需要大量工作来对其进行更新，并转换为可以提交的形式。
日志中也详细谈到了大模型工具发挥的作用。
在第一天，陶哲轩就对GitHub Copilot大加赞赏：
GitHub Copilot在处理日常任务时非常有用，比如输入需要证明的新Lean定理，或者更新蓝图来整合最新的PR结果。
他具体举了个例子：要将Lean转换为LaTeX，把Lean代码粘贴为注释，开始敲LaTeX，GitHub Copilot就会自动补全剩下的内容。
不过，陶哲轩也坦率表示，
大模型们在项目中的表现“低于预期”
，更多的时候，数学家们用到的还是“经典AI”，比如自动定理证明器Vampire等。
他还提到：
项目的参与者非常多元化，包括处在职业生涯各个阶段的数学家和计算机科学家，学生和业余爱好者。Lean在整合人类和机器生成的贡献方面表现出色。机器生成的部分在数量上是贡献的最主要来源，不过，许多自动生成的结果最初是人类在特殊情况下得出的，之后被进一步推广和形式化。
具体到项目中，GitHub Copilot的主要作用还是加快代码的编写，而Claude则被用来帮忙创建可视化工具，比如这个“等式浏览器”：
ChatGPT则更多扮演激发数学家们灵感的小助手角色。
对陶哲轩来说，ChatGPT能帮他快速掌握通用代数的一些细节。
而lyphyser、Daniel Weber、Fan Zheng和Bhavik Mehta这几位项目参与者，还通过跟ChatGPT的讨论，证明1659这个等式可能具有非平凡的合流性。
主项目里程碑达成，不过“等式理论计划”的其他衍生项目仍在进行中，比如研究在有限原群限制下的类似蕴含图、对蕴含图进行数据分析等等。
希望项目中的蕴含关系能够作为未来AI数学工具的基准测试。
除了陶哲轩之外，项目的主要维护人还有意大利数学家Pietro Monticone和Shreyas Srinivas。
△Shreyas Srinivas主页
Pietro Monticone还和他特伦托大学的同事们一起搞过指数3的费马大定理的Lean版证明。
GitHub：
https://github.com/teorth/equational_theories
参考链接：
[1]https://mathstodon.xyz/@tao/113522452070896956
[2]https://teorth.github.io/equational_theories/
[3]https://terrytao.wordpress.com/2024/10/12/the-equational-theories-project-a-brief-tour/
阅读最新前沿科技研究
报告，欢迎访问
欧米伽研究所的“未来知识库”
未来知识库
是“
欧米伽
未来研究所”建立的在线知识库平台，收藏的资料范围包括人工智能、脑科学、互联网、超级智能，数智大脑、能源、军事、经济、人类风险等等领域的前沿进展与未来趋势。
目前拥有超过8000
篇重要资料。
每周更新不少于100篇世界范围最新研究
资料
。
欢迎扫描二维码或点击本文左下角“阅读原文”进入。
截止到10月25日 ”未来知识库”精选的100部前沿科技趋势报告
1. 牛津大学博士论文《深度具身智能体的空间推理与规划》230页
2. 2024低空经济场景白皮书v1.0（167页）
3. 战略与国际研究中心（CSIS）人类地月空间探索的总体状况研究报告（2024）
4. 人工智能与物理学相遇的综述（86页）
5. 麦肯锡：全球难题，应对能源转型的现实问题（196页）
6. 欧米伽理论，智能科学视野下的万物理论新探索（50页报告）
7. 《美国反无人机系统未来趋势报告（2024-2029 年）》
8. Gartner 2025 年主要战略技术趋势研究报告
9. 2024人工智能国外大模型使用手册+中文大模型使用手册
10. 详解光刻巨人ASML成功之奥妙-241015（94页）
11. CB Insights：未来变革者：2025年九大科技趋势研究报告
12. 国际电信联盟2023-2024年联合国人工智能AI活动报告388页
13. 《人工智能能力的人类系统集成测试和评估》最新51页，美国防部首席数字和人工智能办公室（CDAO）
14. 2024瑞典皇家科学院诺贝尔化学奖官方成果介绍报告
