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

在经过 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相关的等式有：

等式理论计划的目标是找出magma中不同等式之间的等价、推导和非推导关系。

以上述11个等式为例，最终的关系图将如下：

观察可知，常量公理等式（1）蕴含其他所有等式，即如果1成立，其他等式也自动成立；而反身公理等式（11）由于最宽松（x=x），几乎所有的magma都满足这一公理。

回到该计划本身，陶哲轩等人在初始阶段集中研究了那些只包含一个方程的magma定律，这类方程至多包含四个magma操作（即二元运算）。

举个例子，如果我们有一个magma（M，∗），其中M是元素的集合，∗是定义在M上的二元运算。

那么一个“最多四次使用magma操作”的表达式如下：

• a∗b（一次操作）

• (𝑎∗𝑏)∗𝑐(a∗b)∗c（两次操作）

• 𝑎∗(𝑏∗(𝑐∗𝑑)) a∗(b∗(c∗d))（三次操作）

• ((𝑎∗𝑏)∗𝑐)∗(𝑑∗𝑒)((a∗b)∗c)∗(d∗e)（四次操作）

其中𝑎,𝑏,𝑐,𝑑,𝑒都是集合M中的元素，每次∗的使用都计为一次magma操作。

这类等式定律共有4694个，由于每个定律可能蕴含其他4693个定律（一个定律不能蕴含自身），因此总共有4694*(4694-1) = 22,028,942个可能的蕴含关系需求进行证明或驳斥。

这里的蕴含关系包含“蕴含”和“反蕴含”，前者分为两种类型：

• 已被证实的蕴含：在Lean中已验证

• 假设的蕴含：尚未在Lean中验证，可能由人类或计算机生成

有关项目的更多细节，陶哲轩在项目日志中有详尽的记录——

9天进度99.866%，大模型发挥作用但未达预期

总结“等式理论计划”的进度简单来说就是一个词：快。

陶哲轩自己说：

这个项目的进度远超我的预期。

速度有多快？

在仅仅只有48小时的时间内，许多蕴含关系就已经“几近解决”。

项目开始的第5天，参与者们已经从2200万条蕴含关系中解决了许多简单的推导，剩下的300万左右需要进一步处理。

项目启动的第9天，伴随着第一轮重大重构的完成——合作者们改进了magma的运算符号，使Lean代码的编译速度大幅提高，以及一些研究问题的进展，项目完成度一举从87%跃升至99.866%。

第19天，项目完成度达到99.9963%。陶哲轩在他的博客中指出，撰写论文的事情已经被列入计划，并且可能会有数十位作者参与。

GitHub显示该项目有45位贡献者：

至2024年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的联系：

希望