陶哲轩宣布“等式理论计划”成功：人类 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 个等式来看，最终的关系图 be like：

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

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

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

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

• a∗b（一次操作）

• (