陶哲轩用AI证明方程理论，19天进度99.99%！论文即将上线

AI，已成为菲尔兹奖得主最得心应手的工具。

大约三周前，陶哲轩提出了一个协作项目——

结合专业和业余数学家、自动定理证明器、AI工具，以及证明辅助语言Lean，来描述与4694条幺半群（magmas）方程定理定理相关的蕴含图。

这些定理最多可以使用，四次幺半群运算来表达。

也就是说，需要确定4694条定理之间可能存在4694 * (4694 - 1) = 22028942蕴含的关系真伪。

这一项目在9月25日发布当天便启动了，如今，已经紧锣密鼓进行了19天。

刚刚，陶哲轩公布了项目的最新进展：

从已解决原始蕴含关系角度来看，截至目前，项目进度已完成99.9963%。

在需要解决的22028942个蕴含关系中，8178279个被证明为真，13854531个被证明为假，只有826个仍未解决。

而且，项目每一天的进展，他都记录到了个人日志中。

一起看看，陶哲轩如何通过「众包方式」，探索数学新领域。

在集合中，有249个蕴含关系推测为假，并且很快就证明了是假的。

出于编译效率的考量，他们并没有在Lean中记录每一个证明，只在其中证明了一个较小的592790个蕴含关系集合，然后通过传递性推导出更广泛的蕴含关系集合。

例如，利用如果方程X蕴含方程Y，方程Y蕴含方程Z，那么方程X蕴含方程Z的事实。

他们还很快利用蕴含图对偶对称性，对其进一步简化。

经过项目志愿者的不懈努力，陶哲轩称现在有了很多出色的可视化工具（尚未完成的），来检查蕴含图的各个部分。

比如，如下这张图描述了方程1491：x = (y ◇ x) ◇ (y ◇ (y ◇ x ))的所有结果。

陶哲轩将其称之为「Obelix law」。它还有一个伙伴Asterix law，即方程65：x = y ◇ (x ◇ (y ◇ x ))。

如下是，他们正在研究的所有方程定理的表格，以及它们蕴含/被蕴含定理数量。

这些界面也在某种程度上与Lean集成。

比如，我们可以点击查看Obelix law蕴含方程359，陶哲轩将其作为题目，让大家进行挑战。他暗示，在Lean中仅用4行就可以完成证明。

在过去的几周里，他还了解到这些定理中，有许多之前已经出现在文献中。

由此，这里编制了这些方程的「导览」。

例如，除了众所周知的交换律（方程43）、结合律（方程4512）之外，一些方程（方程14、方程29、方程381、方程3722、方程3744）曾出现在一些Putnam数学竞赛中；

方程168定义了一个引人入胜的结构，被称为「中心幺半群」（central groupoid）。特别是，由Evans和Knuth研究过，并且是Knuth-Bendix完成算法的关键灵感来源；

而方程1571则对指数为二的阿贝尔群（abelian groups）进行了分类。

根据Birkhoff完备性定理，如果一个方程定理蕴含另一个，那么它可以通过有限次重写操作来证明。

不过，所需的重写次数可能相当长。

上面提到的1491蕴含359的证明已经相当具有挑战性，需要四到五次重写。

另外，方程1689蕴含方程2的证明，更是极其冗长。尽管如此，标准的自动定理证明器，如Vampire，完全有能力证明绝大多数这些蕴含关系。

更微妙的是反蕴含关系，在这种情况下必须证明定理X不蕴含定理Y。原则上，只需要展示一个遵循X但不遵循Y的幺半群即可。

在很大一部分情况下，他们可以简单地搜索小型有限幺半群——比如两个、三个或四个元素的幺半群——来获得这种反蕴含关系。

但这些并不足够，事实上，他们只知道有些反蕴含关系，只能通过构造无限幺半群来证明。

比如，现在已知的Asterix law不蕴含Obelix law，但所有反例必然是无限的。

有趣的是，已知的构造方法与集合论中著名的forcing技术有一些相似之处，即不断向（部分）幺半群添加「通用」元素，以forcing存在具有某些特定属性的反例。

不过，这里的构造肯定比集合论构造简单得多。

他们还从「线性」幺半群x ◇ y = ax + by构造中取得了有益的进展。这些构造存在于交换环和非交换环中。

与「汇聚」（confluent）方程定理相关的自由幺半群，以及更普遍的具有完整重写系统的定理。

因此，未解决的蕴含关系数量继续稳步减少。

经过相当繁忙的后端设置和「灭火」（putting out fires）工作后，项目现在运行得相当顺利。

项目在Lean Zulip频道上协调，所有贡献都通过GitHub上的拉取请求（pull request）过程进行，并通过基于问题的GitHub项目进行跟踪。

另外两位维护者Pietro Monticone、Shreyas Srinivas为其提供了宝贵的监督。

与之前的PFR形式化项目相比，这次项目的工作流程遵循了标准的GitHub实践，大致如下：

如果在Zulip讨论过程中，明确需要完成某些特定任务以推进项目（比如，在Lean中形式化讨论线程中已经推导出的蕴含关系证明），就会创建一个「问题」（通常由陶哲轩自己或其他维护者创建），其他贡献者可以「认领」这个问题，单独工作（使用主GitHub仓库的本地副本）。

然后提交「拉取请求」将他们的贡献合并回主仓库。这个请求随后可以由维护者和其他贡献者审查，如果获得批准，就会关闭相关问题。

更广泛地说，他们正努力记录这个设置中的所有过程和经验教训。

这将成为即将发表的关于这个项目的论文的一部分，现正处于初步规划阶段，可能会包括数十位作者。

陶哲轩表示，自己对项目取得的进展非常满意，而且许多最初的期望已经实现。

在科学方面，他们发现了一些新的技术和构造，用来证明一个给定的方程理论不蕴含另一个；他们还发现了一些具有有趣特征的奇特代数结构，如Asterix和Obelix对，是通过系统性搜索方式被发现的。

参与者方面，非常多样化，从各个职业阶段的数学家、计算机科学家，到感兴趣的学生和业余爱好者。

此外，Lean平台在整合人工生成和机器生成的贡献方面表现良好。

机器生成在数量上是迄今为止最大的贡献来源，但许多自动生成往往是基于人类最初在特殊情况下发现的，然后由项目的不同成员进行推广和形式化。

在讨论线程中，他们还进行了许多非正式的数学论证，但这些论证往往会迅速在Lean中形式化，消除了关于正确性的争议就。

进而，研究人员可以转而专注于如何最好地部署各种经过验证的技术，来解决剩余的蕴含关系。

原本，陶哲轩期待看到现代AI工具，能够在项目中做出重大贡献。

但实际上，它们以一种辅助、次要的方式被使用。

比如，通过GitHub Copilot等工具来加速编写Lean证明、LaTeX文档框架、其他软件代码。

此外，他们的几个可视化工具，也主要是使用Claude等大模型共同编写的。

然而，对于解决蕴含关系这一核心任务，更「传统」的自动定理证明器表现更好。

不过，目前剩余的大约700个蕴含关系，大多数不适合使用传统工具来处理。

有几个蕴含关系（特别是涉及Asterix和Obelix那些），已经让人类专家困惑多日。

陶哲轩认为，在解决剩余的、更困难的蕴含关系时，现代AI可能会发挥更重要的作用。