Lean 验证为何不等于证明正确：AI 时代数学证明的可信度问题

鉴于AI 现在能做什么，这可能是关于数学现状及其未来系列文章的第一篇。我希望它能相当有启发性地说明，何时以及多大程度上应当重视如今无处不在的“在 Lean 中已验证”，同时也写下一些不那么基于事实的个人信念。

六月，我得以在科罗拉多山区待了几天，作为交换，我做了一场关于在 Lean 中对旗代数进行计算形式化的报告。¹这不是一个好讲的题目，因为形式化证明验证和旗代数都是人们常常急于使用、却不那么急于理解的工具。在对 Lean 做了那段必不可少的、过于简略而无甚用处的介绍之后，我收到了一个类似这样的问题：

“那么，如果有人提交了一篇论文，并声称它已在 Lean 中完全验证，作为编辑，我如何知道这实际上意味着这篇论文是正确的？”

这发生在 Fable 和 Astra 公开发布之前，但就在两周前，Erdős 的单位距离猜想已经被OpenAI 的“一个内部模型”证伪。我做报告的那天晚上，也是我第一次看到四位终身教授晚上 10 点站在黑板前，挠着头，试图决定是否要相信“它”为他们正在研究的一个问题想出的一个证明。所以，虽然这个问题并非我的报告所要回答的，但它或许至少值得尝试给出一个答案。

关于 Lean 代码何时可能实际上并不能作为证明的证书，有一个技术性且事实正确的答案。你最喜欢的 AI 聊天平台很可能会给出与下面这份清单类似的内容，这是我为上一轮 Lean 课程写下的：

1. 相关部分未被形式化。一个有趣的例子来自OpenAI 的证明，即平面的色数至少为 6：在一个脚注中，它简要提到一份手稿已经声称该数为 7，并暗示有 Lean 形式化验证；然而，那个形式化验证只涉及所声称证明的一部分。其主要形式化定理假设了单位圆上无单位距离子集的角测度的一个界——而正如 OpenAI 的内部模型所指出的，这个界并不成立。换句话说，一个 LLM 正确地事实核查了一篇人类撰写、并宣称有 Lean 证书的论文。

2. 形式化证明与书面证明不同。Bastounis、Circelli 和 Hansen发现，伴随OpenAI 关于 Navier–Stokes 爆破的证明的 Lean 代码中，若干中间估计比书面论文中相应的估计多需要一个导数。定理得到了验证，但严格来说，那篇论文中的证明并没有。

3. 形式化陈述与预期陈述不同。多年来，已发表的关于\(\zeta(3)\)无理性的 Coq 形式化，其主定理陈述中使用的是 = 而不是 ==。这个错误的陈述只是说部分和序列不是常数；它并没有确立其极限是无理数。证明本身没有问题。

4. 证明存在漏洞或依赖额外公理。一个sorry会留下一个未证明的步骤，而一个axiom则直接断言一个超出三条标准公理（propext、Classical.choice、Quot.sound）之外的公理。一个更隐蔽的变体是native_decide，它信任编译后的代码而非内核。所有这些都会被标记出来，但可以通过一个简单的set_option关闭这些警告。

5. 内核漏洞被利用。今年七月，一个对考拉兹猜想的“反证”在没有sorry或额外公理的情况下通过了编译，因为它利用了内核处理嵌套归纳类型时的一个漏洞。²

6. 编译器链或硬件存在信任问题。内核本身就是一个编译后的程序，因此人们最终要信任该链条中的每一个编译器，以及它所运行的硬件。

这些都是正确且相关的，但我认为它们并没有真正回答这个问题。对某些人——尤其是编辑——来说，形式化验证的承诺在于你不再需要思考证明就能信任它；但上述几点表明，它只是转移了你必须思考的内容。

真正的答案令人遗憾地既不技术性也不令人满意：Lean 代码是一种言语，而言语既可以用来传递信息，也可以用来误导。作为一种形式语言，Lean 施加了强有力的约束，使得后者变得困难得多，但它最终无法阻止——尤其是当误导信息存在于与自然语言的接口处时。与此同时，这些约束增加了接收者对信息正确性的信任，这可能使滥用——无论是出于恶意还是疏忽³——更有可能发生。

如果非要给出一个实际的答案，那就是：只有当至少三件事由足够有知识的人检查过时，Lean 代码才在认证目的上有意义：

1. 声称被验证的陈述实际上就是代码中被验证的陈述。
2. 代码建立在社区公认的定义和陈述之上，理想情况下这些陈述和定义并非来自提供证明的同一批人。如果不是这样，至少最终陈述、其假设以及所需的定义必须经过审查。
3. 没有滥用或误用系统的迹象：没有添加axiom（用#print axioms检查），没有遗留的sorry，没有禁用关于不安全操作的 linter 警告，也没有任何看起来像利用内核漏洞的东西。理想情况下，它使用最新版本的 Lean 和 Mathlib 编译通过。

在大多数情况下，这比完全消化一份手写证明要容易得多，但并非微不足道。重要的是，如果你在问这个问题，你很可能已经有某种理由不信任结果的来源或 Lean 证书。没有人怀疑Liquid Tensor Experiment真正形式化并验证了 Clausen 和 Scholze 的工作，因为它是一个公开交流的项目，是数学家之间的合作，其真诚目标是消除对一个黑箱结果——其证明很少有人会完整阅读或消化，但会被下游使用——是否真正成立的最后一丝疑虑。

但对于大量 AI 生成的证明来说，情况就不同了——它们全都带着“已在 Lean 中验证”的印章。如果附上 Lean 代码的原因是作者自己都没有充分消化这个证明，以至于不好意思署上自己的名字，那么再配上一段同样没人读过的 Lean 代码，在我看来只会削弱而非增强信任。廉价的形式化削弱了人类投入的信号，即便证书在数学上仍然有效。换个更有建设性的说法：如果你已经读过这个证明，判断它成立，并用自己的话写了一份阐述，那么再让 LLM 生成一段没人会读的 Lean 代码，意义不大。

需要说明的是，这并不意味着我认为 OpenAI 抛出的那 700 多篇论文——其中许多按大多数标准都算得上是突破——是错误的。恰恰相反，过去几个月里，我对最新 LLM 检测数学论证中缺陷的能力（即便没有任何 Lean 验证）的信心大幅提升，以至于用 LLM 做一些批判性探查，就能实现“已在 Lean 中验证”印章的大部分承诺。同样很可能的是，形式化证明验证对大型 AI 实验室达到这一水平起到了重要作用，也就是说，在决定训练中强化哪些信号时起到了作用。但那是另一个问题，对不从事机器学习、也不参与这些网络训练或评估的数学家来说，关系不大。

以一个稍微更令人振奋的结尾收束：正如一个证明的价值从来就不仅仅在于它解决了一个命题，形式化代码的价值也从来不仅仅在于那张证书。理想情况下，它还能帮助编写或阅读它的人通过一种更严格、更不留情面的结构来理解证明。为 Mathlib 做贡献也意味着与他人讨论，并就定义、陈述和证明达成共识——这是一个比发表论文更具侵入性的过程。至少对我来说，使用 Lean 显著塑造了我对数学及其基础的思考方式，我对此心怀感激。

1. 其目标基本上是让人能够写下任何 flag algebra（不）等式（平方和或其他形式），并让 Lean 验证它，再将其与图论中的实际陈述联系起来。我应该指出，Gyeongwon Jeong、Seonghun Park、Jihoon Hyun、Sang-il Oum 和 Hongseok Yang 也独立地在 Lean 中形式化了 flag algebra，并且（与我不同）已经公开了他们的代码。 ↩

2. 它还通过利用另一个独立的 bug 通过了独立检查器。内核 bug 在报告后一小时内就被修复，独立检查器中的 bug 也早已修复，但那次检查是用过时的版本运行的。 ↩

3. 人们当然可以想象，一位数学家下意识地对定义中的某个问题视而不见，因为这样证明才能成立；而尽管他们恶意行事不太可能，成千上万个被困在盒子里、面对不可能任务的智能体却有可能这么做。 ↩