AI 颠覆数学研究！陶哲轩借 AI 破解数学猜想，形式化成功惊呆数学圈

【新智元导读】历时三周，陶哲轩成功地用 AI 工具完成了形式化多项式 Freiman-Ruzsa 猜想证明过程的工作。他再次呼吁数学研究者学会正确利用 AI 工具，网友惊呼：以后的数学论文不需要人类可读了？

用 AI 工具辅助研究数学的项目，再一次被陶哲轩跑通！

三周前，他曾发布一篇博文，记录下自己使用 Blueprint 在 Lean4 中形式化多项式 Freiman-Ruzsa 猜想的证明过程。

就在昨天，他激动宣布：将多项式 Freiman-Ruzsa 猜想的证明形式化的 Lean4 项目，在三周后取得了成功！

现在，依赖关系图已经完全被绿色所覆盖，Lean 编译器也报告说，这个猜想完全遵循标准公理。

陶哲轩表示，在整个团队中，自己贡献的代码大概只有 5%。这个结果很鼓舞人心，因为这意味着数学家即使不具备 Lean 编程技能，也能领导 Lean 的形式化项目。

他发现，项目中在数学上最有趣的部分，形式化起来比较容易，而技术上看起来最显而易见的步骤，却最耗时。

而使用 Blueprint 将项目分解成难度小到中等的部分，效果很好，这就让大量并行工作成为可能。

这样，许多贡献者就可以处理特定的子任务，而无需理解整个证明过程，甚至可以完全不了解相关的数学领域知识。

就在几分钟前，Lean 成功证明了 PFR 猜想，且没有留下任何悬而未决的问题（后文将会提到的「sorry」）。这意味着，这个项目的所有主要目标，都已经圆满完成。

与此同时，他在三周前也就是 11 月 18 日的那篇博客也被网友翻出，引发热议。

果然，AI 加持数学研究颠覆力量的后劲，得需要数月的时间才能让人们认识到。

而只有在最前线的研究者，才能在第一时间切实感觉到这种巨大力量的冲击和震撼。

陶哲轩呼吁：数学家们一定要学会用 AI 了

有网友向陶哲轩提问：这是否意味着，有越来越多的证明是人类不可理解，但机器可解决的？

陶哲轩表示，恰恰相反，如果证明的形式化变得更加主流，并且更多地得到 AI 辅助，那完全有可能创建出既人类可读、又能被机器阅读的证明。

PFR 证明的 blueprint 就证明了这一点 —— 既人类可读，每个证明步骤还带有形式化的理由，还能得到一个依赖关系图，来可视化整个论证的全局结构。

当然，陶哲轩也提醒道，不要把「计算机辅助证明」和「不能提供理解 / 偶然成立的证明」搞混了。

比如对于有限单群分类的超过 10000 页的证明，几乎百分百是由人工生成的，但一个由计算机协助处理的替代证明，在某些方面看更令人满意。

跟网友经过几轮讨论后，陶哲轩做出以下总结 ——

Blueprint 本身就是一种编程语言，可以看作一种 Lean 的伪代码。

许多数学家都应该将写作风格从标准数学英语 / LaTex，转换为 Blueprint / LaTex。

网友：以后研究都不需要「人类可读」，AI 懂就行了

网友表示，陶哲轩对于各种研究工具随意掌握的程度，几乎可以称得上是可怕。

我在研究生阶段对数学的尝试，就就好像一个穴居人本来在摇晃一辆普通的独轮车，忽然眼前出现了一辆直升机，上面的人向我伸出手，告诉我来试试看，一点也不可怕。

自从听说四色定理以来，我一直很清楚，形式化是数学的未来。但我没有预料到的是，陶哲轩如此从容不迫，形式化才刚刚获得牵引力，他就能用 AI 完成几乎所有的数学写作。

形式化，是指从基本公理和规则中真正推导出证明中的每个陈述。而陶哲轩在这篇博文里，把需要死记硬背的劳动都抽象出来，交给了机器。

他的工作表明，形式化才刚刚开始在主流数学中受到关注。

已经有人开始畅想：很可能会有一段时间，大多数证明只是在 Lean 或类似系统中完成，再也没有人需要费心写一篇「人类可读」的论文了。

数学，将变成一种编程！

一位数学硕士表示，现在自己的研究步骤有三步 ——

1.理解自己想证明的东西，通过阅读或者与人交谈；

2.用纸笔绘制出包含要点的草图；

3.将校样输入到 LaTeX 中，让自己要交的作业变得人类可读。

是的，如果我们只是要训练或微调 AI 来产生答案，然后编写一个循环来反馈，直到编译器正确输出，那我们自己并不需要真的理解。

用这种方法，我们还能生成更多的训练示例，可以手动检查结果是否符合要求，做上注释。而训练，可以提高初始答案的准确性。

PFR 猜想的形式化过程

以下是陶哲轩发在博客上的形式化过程，感兴趣的读者可以挑战一下。

11 月，陶哲轩与 Yael Dillies 和 Bhavik Mehta 启动了一个合作项目，目的是利用 Lean4 对自己之前关于 Freiman-Ruzsa（PFR）猜想的预印本论文进行形式化。

项目虽然启动不到一周，但进展相当顺利，大部分文件都被形式化了。

这个项目得益于 Patrick Massot 的 Blueprint 工具，这个工具让团队能够编写与 Lean 形式化紧密相关的、人类可读的证明「蓝图」。

在 Blueprint 中，有一个陶哲轩特别喜欢的功能，那就是自动生成的依赖图。它可以提供形式化进度的大致快照。截至当时，依赖图的样子如下：

在依赖图的图例中，不同的气泡（表示引理）和矩形（表示定义）被赋予了不同的颜色。

简单来说，绿色的气泡或矩形表示那些已经被完全形式化的引理或定义，而蓝色的则指那些已准备好进行形式化的引理或定义（这意味着它们的陈述已经形式化，但证明还没有，同时所有相关的前置引理和证明也是如此）。

而陶哲轩团队的目标，就是将所有通向「pfr」气泡的底部气泡，都变成绿色。

点击依赖图底部的「pfr」气泡时，可以看到以下内容：

图中，Blueprint 显示出一种人类可读的 PFR 语句形式，还附带了这个语句的人类可读证明，该证明依赖于项目中的其他语句：

注意，「pfr」气泡是白色的，但有一个绿色边框，这意味着 PFR 的陈述已经在 Lean 中正式化，然而证明并没有。

证明本身还没有准备好被形式化，是因为一些先决条件（特别是「entropy-pfr」Theorem 6.16）甚至还没有形式化的陈述。

单击依赖关系图中 PFR 陈述下方的 Lean 链接，就可以进入相应的 Lean 文档：

这就是 Lean 中的典型定理的样子。在冒号之前有许多假设，例如：

G 是一个属于顺序 2 的有限初等阿贝尔群 （这就是团队选择形式化有限场向量空间的方式）；A 是 G 的非空子集；A+A 的基数＜K 倍 A 的基数。

冒号后边的陈述是结论：A 可以以 c+H 的和的形式包含在 G 的子群 H 中，以及在最多 2K¹² 的基数的集合 c 中。

聪明的读者可能会注意到，上面的定理似乎缺少一两个细节，例如，它没有明确断言 H 是一个子群。

这是因为「pretty printing」模式抑制了定理陈述中的一些信息，只要单击「来源」链接，就可以看到了。

可以看到，H 需要具有 G 加法子群的类型。

该定理底部有一个明显的「sorry」，这意味着尚未为该定理提供证明，但最终意图当然是用实际证明，来代替这个「sorry」。

填补这个「sorry」现在还很难做到，所以需要寻找一个更简单的任务。

下面是一个简单的中间引理「ruzsa-nonneg」，它出现在证明中：

该表达式 d【X;Y】指的是 X 和 Y 之间的熵 Ruzsa 距离，它是一个实数。

气泡是蓝色的，带有绿色边框，这意味着陈述已经形式化，证明也准备好形式化了。

Blueprint 依赖关系图表明，这个引理可以从前面的一个引理中推导出来，称为「ruzsa-diff」：

「uzsa-diff」也是蓝色的，边框是绿色的，所以它与「ruzsa-nonneg」具有相同的当前状态：陈述是形式化的，证明也准备好形式化了，但证明还没有用 Lean 编写。其中，H【X】是 X 的香农熵。

通过观察 Lemma 3.11 和 Lemma 3.13，我们可以清楚地看到 | H [X] - H [Y]| 显然是非负的。

因此，即使我们还不知道如何证明 Lemma 3.11，但假设 Lemma 3.11 成立，并补全 Lemma 3.13 的证明，应该是轻而易举的事。

Lemma 3.11 的形式化如下：（「sorry」表示 Lemma 目前还没有证明）

同时，Lemma 3.13 的形式化为：

现在，我们要试着把后一个「sorry」填上。

在 PFR github 仓库的本地副本中，陶哲轩用编辑器（Visual Studio Code，扩展名为 lean4）打开了相关的 Lean 文件，并导航到「rdist_nonneg」的「sorry」处。

随附的「Lean 信息视图」就会显示 Lean 证明的当前状态：

在底部，可以看到我们需要证明的目标。

接下来，在证明这个说法时，需要运用一系列「战术」来改变目标和 / 或假设。

第一步是加入应用 Lemma 3.11 所需的因子 2。

现在，我们有了两个目标（和两个「sorry」）：一个是证明 0≤2d [X;Y] 等价于 0≤d [X;Y]；另一个是证明 0≤2d [X;Y]。

在填上第一个「sorry」之后的状态如下（删去了一些无关的假设）：

这里可以使用一种非常方便的「linarith」策略，它能解决任何可以通过现有假设的线性运算得出的目标：

成功之后可以看到，状态报告显示这个分支已经没有需要证明的目标了。所以，我们继续剩下的「sorry」，也就是证明 0≤2d [X;Y]：

在这里，我们将尝试引用 Lemma 3.11。为此，陶哲轩添加了几行代码：

于是，我们又有了两个子目标，一个是证明约束

（可以称之为「h」），另一个是就从 h 推导出前一个目标 0≤2d [X;Y]。

对于第一个目标，需要调用正在编码 Lemma 3.11 的「diff_ent_le_rdist」引理。

其中一种方法是尝试使用「exact? 」策略，它会自动搜索，看目标是否可以立即从现有的引理中推导出来：

于是，陶哲轩点击了建议的代码（系统会自动将其粘贴到正确的位置）。结果成功了，只留下最后的「sorry」：

这里，陶哲轩通用使用了「exact?」策略，并按照它的建议建立匹配了边界

：

在补全最后一个「sorry」时，陶哲轩再一次尝试了「exact?」，想知道如何把 h 和 h' 结合起来才能达到预期目标，结果成功了！

可以看到，所有的下划线都消失了。也就是说，Lean 已将其视为有效证明。

通过省略几个中间步骤，我们可以将这个证明压缩得相当紧凑：

现在证明完成了！

我们最后得到的，基本就是一个「单线证明」，考虑到 Lemma 3.11 和 Lemma 3.13 是如此接近，这也是合情合理的。

然后，陶哲轩将所有内容推送回 Github 主版本库。

Blueprint 的重建需要相当长的时间（约半小时），依赖关系图现在以绿色显示 「ruzsa-nonneg」：

因此可以说，PFR 的形式化更接近完成了。

不过，虽然「ruzsa-nonneg」现在被涂成绿色，但还没有这个结果的完整证据，因为它所依赖的引理「ruzsa-diff」不是绿色的。

从这一点上看，证明仍然是局部完成的。

陶哲轩表示，希望在未来的某个时候，前身结果也能被证明，那时，就可以说 PFR 猜想的结果，得到了完全的证明。

参考资料：

• https://news.ycombinator.com/item?id=38528582

• https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/

本文来自微信公众号：新智元 （ID：AI_era）

广告声明：文内含有的对外跳转链接（包括不限于超链接、二维码、口令等形式），用于传递更多信息，节省甄选时间，结果仅供参考，IT之家所有文章均包含本声明。