Lean证明能为AI数学成果担保什么

2026 年 8 月 1 日，OpenAI 发布了下一代模型家族 Astra，同时公布了十项数学与理论计算机科学领域的新成果。每项成果对应的问题都至少悬而未决了十年，而且都附带了可由机器检查的 Lean 4 证明证书。

一个自然而然的问题，也是我们反复思考的问题：既然此前从未有人解决过这些问题，我们怎么知道 Astra 不是在幻觉中编造出了一套看似可信的故事？答案是：Lean 证明可以彻底消除其中一种疑虑，但对于另外三种疑虑，它什么也证明不了。弄清楚它能解决什么、不能解决什么，就是整个故事的关键，而且其意义远远超出了数学领域。

我们为受监管环境构建验证系统，因此这个问题正是我们的日常工作。下面我们将如实解读 Astra 的这些证明究竟确立了什么，又没有确立什么。

OpenAI 的 Astra 究竟做了什么

Astra 给出了十项研究成果，OpenAI 将全部成果的 Lean 证明证书以开放许可证发布在一个公开仓库中。这份清单具体且可验证：构造一个非 sofic 群、给出 Connes 刚性猜想的反例、证明 Ehrhart 体积猜想、给出 permanent 的新下界、证明最近向量问题的近似困难性、证明指数级量子并行重复、改进 Cohn-Elkies 阈值下的球堆积界，以及解决包括第 146、180 和 183 号问题在内的若干 Erdős 问题。据报道，整个计算过程的成本约为 2,000 美元。仓库显示，全部十项证明中仍未得到证明的步骤数量为零。

重要的并不是“十项”这个数字，而是任何拥有一台笔记本电脑和 Lean 编译器的人，都可以独立验证每一份证书，完全不需要信任 OpenAI。

为什么 Astra 的证明与 2025 年那次 Erdős 声明引发了截然不同的反响

OpenAI 以前也站上过这个舞台，但随后摔了下来。2025 年 10 月，该公司声称其某个模型解决了十个 Erdős 问题。事实并非如此。模型只是从已有文献中检索出了现成的解答，然后将其包装成新的成果。检查这项工作的数学家称，这是一次严重的失实陈述。整个声明建立在相信模型对自身工作的描述之上，而这种信任一经专家检验便土崩瓦解。

2026 年的不同之处并不在于模型变得更聪明了，而在于你不再需要相信模型的一面之词。Lean 4 是一个拥有小型可信内核的证明助手。Lean 中的证明不是一段读起来言之成理的论证，而是一个由内核依据公理逐步检查的项，检查结果是二元的：要么编译通过，要么无法通过。不会有听起来信心十足的段落蒙混过关，也不会有人用“因此，显然”来掩盖推理缺口。如果逻辑不成立，它就无法编译。

这就是确定性检查的样子。模型是概率性的生成器，而 Lean 内核则是一条非真即假的规则：要么满足，要么不满足。化解这场信任危机的方法很简单：不要再让人们相信模型，而是交给他们一个可以自行重新计算的事实。

AI 能否幻觉出一个仍能通过 Lean 检查的数学证明？

对于某一种特定的幻觉，答案是否定的，而这正是此次发布如此有分量的原因。那种论证行文流畅、但中间悄悄混入无效推理的失败模式已经被彻底消除了。内核并不关心证明写得多么流畅。每一步推理都会经过机械检查，因此，一个能够编译通过的证明在构造层面就是逻辑有效的。对于这类工作而言，这已经是最接近确定性的程度。

但绿色对勾并不能说明另外三件事，而这三件事都可能让你在完美通过编译的同时仍然犯错。

Lean 证书无法证明什么

陈述本身可能并不是你以为的那个意思。Lean 证明的是一个定理，但这个定理对应的是由人类写下的形式化陈述。如果“存在一个非 sofic 群”的形式化表达不易察觉地弱于原问题，或者悄悄在假设中预设了某些条件，那么 Lean 就会忠实且完美无误地证明一个错误的问题。这不是逻辑错误，而是从英文问题转换为 Lean 陈述时产生的翻译错误，无论进行多少次内核检查都无法发现它。必须由同时理解相关数学知识和形式语言的人阅读这条陈述，并确认它确实就是那个尚未解决的开放问题。

一条错误的公理可以证明任何命题。内核会基于提供给它的公理进行构建。无论是由于疏忽还是有意为之，只要加入一条错误的公理，系统就能证明任何陈述。Lean 允许你输出某个证明所依赖的完整公理列表，因此这件事是可以检查的——但前提是确实有人去检查。

能够编译不等于具有原创性。这正是 2025 年那次尝试失败的原因。一个完全从既有文献中检索出来的证明，可以与原创证明一样顺利地通过编译。Lean 能告诉你一个陈述是真的，却永远不会告诉你它是不是新的。只有熟悉该领域的专家才能判断某项成果究竟是真正的进展，还是一次重新发现。

信任并没有消失，只是转移了位置

这才是能够推广到其他领域的关键。验证并没有消除对人类判断的需求，而是转移并缩小了它的范围。

在 Lean 出现之前，数学家必须阅读完整的论证，判断其中每一步是否成立。这是一个庞大且容易出错的检查面。引入 Lean 之后，内核承担了这部分全部负担。留给人类的问题变得更加集中、也更加尖锐：这条形式化陈述是否与现实中的问题一致？它使用的公理是否诚实可靠？问题的范围缩小了，但重要性丝毫未减。它是地板之下的地板。机器检查是真实有效的，但在它的下方，仍然存在一层无法消除的人类检查：机器一开始被要求解决的，究竟是什么问题？

这一理念最有力的体现就在仓库本身。OpenAI 不只是发布了一批能在自家机器上编译通过的证书，还提供了工具，让外部人员可以独立重新运行这些检查。这是一层被公开、可重复运行的确定性地板，也是这种论证所能采取的最诚实形式：不要相信我们说它通过了，自己运行一遍。

这对所有使用 AI 构建系统的人意味着什么

阅读本文的大多数人并不从事定理证明，但只要 AI 介入重要事务，问题的形态其实都一样。模型生成一个流畅、自信，却可能错误的输出。真正的问题永远相同：由什么来检查它？这个检查机制是否比模型本身更值得信任？

Astra 证明带来的启示，并不只是 AI 如今已经能够从事数学研究——尽管它的确越来越擅长这件事。真正的启示是：能够赢得信任的系统，都是那些可以指出一层确定性地板并明确说明的系统：这是它必须满足的规则，这是它满足规则的证明，而且你可以亲自检查这份证明。然后，在更安静、更底层的位置，还要有一个能够确认规则本身是否正确的人。

构建这层地板。然后记住，地板之下还有一层地板，而这一层由真正理解机器究竟被要求证明什么的人组成。

Astra 的 Lean 证明证书位于 github.com/openai/ten-proofs，Lean 本身位于 lean-lang.org，两者都值得花一个下午研究。

因此，我们想把这个问题留给你：在你自己的系统中，哪些地方由机器给出最终结论？哪些地方仍然需要有人确认，机器一开始究竟被要求做了什么？我们曾不止一次惊讶地发现，这条分界线的实际位置与预想并不相同。

如需采取进一步措施，你可以考虑屏蔽此人和/或举报滥用行为。