Markdown 版本

AI-translated from English; not yet reviewed by a fluent editor.

# Tristan Buckmaster 谈如何检查 AI 生成的数学证明

> 在 World Science Festival 的访谈中，Tristan Buckmaster 解释了 AI 生成的论证如何经过形式化检查，以及为什么易读的证明和独立评估仍然重要。

By BIG CHANGE Editorial

Published: 2026-10-08T22:26:20.730Z
Updated: 2026-10-08T22:26:20.730Z
Canonical: https://bigchange.ai/blog/tristan-buckmaster-ai-math-proof-checking

![An anonymous person stands back from a wall-mounted blackboard; crowded chalk strokes at left give way to an erased center and sparse strokes at right.](https://bigchange.ai/api/media/file/buckmaster-proof-readability-hero-v1.png)
Conceptual illustration of the work of making a dense argument readable. It does not show Tristan Buckmaster, the interview venue, an actual proof or a completed proof check. AI-generated illustration by BIG CHANGE.

在一场[10月2日的 World Science Festival 访谈中](https://www.worldsciencefestival.com/programs/the-moment-ai-changed-mathematics-forever/)，数学家 Tristan Buckmaster 介绍了一项由 AI 生成的结果；他认为结果正确，但其他数学家很难读懂。他的讲述将近期 Navier–Stokes 声明引出的疑问说得更具体：当易读的解释还需要进一步工作时，研究共同体如何检查一个形式化论证？

Buckmaster 谈到他与 Levent Alpöge 关于**带光滑外力的三维 Euler 方程**的工作。他们的结果不同于[OpenAI 9月8日提出的声明](https://openai.com/index/navier-stokes-solution/)，后者涉及**带光滑外力的 Navier–Stokes 方程**。Navier–Stokes 方程包含黏性，Euler 方程则没有。OpenAI 发布了一篇论文和 Lean 形式化文件，支持其关于有限时间内发生奇异的主张。负责管理 Millennium Prize 的机构尚未宣布颁奖。

## 重大变化

- **变化之处：**Buckmaster 首次亲自讲述了如何使用 AI 生成的论证和 Lean 建立另一项受迫 Euler 结果，以及向数学家解释此类证明仍需开展哪些工作。
- **这为何重要：**形式化检查可以确认编码后的论证是否由指定的定义和依赖关系推出。数学家还需要理解定理的含义、其思想如何运作，以及它借鉴了谁的先前工作。
- **后续观察：**Clay 对 OpenAI 的 Navier–Stokes 声明进行评估、出现易读的证明说明，以及关于作者身份和访问权的公开讨论，都将显示这一结果如何被评价。Buckmaster 对结果的信心是专家观点，并非颁奖决定。

## 经过检查的论证仍需要解释

在这场[访谈中](https://youtu.be/PQYFRuZ5phs)，Buckmaster表示，人工智能为他的Euler结果生成的第一份证明中，既有有用的思路，也夹杂着无关计算和难以阅读的表述。他的团队先借助其他智能体逐步检查论证，随后将其转写为Lean以进行形式化验证。他说，尽管呈现方式不佳，最终证明仍然正确。这段讲述针对的是**他的 Euler 工作**；不应将其理解为他独立核验了 OpenAI 另一篇 Navier–Stokes 论文的每个部分。

这种区别有实际意义。Lean 会在指定的证明环境中检查精确定义的命题，但它本身不会让长篇论证变得易读，也无法自动帮助研究者复用其中的方法。Buckmaster 告诉 Brian Greene，其他 AI 系统能够解析一些他几乎读不懂的段落；请 AI 将其改写成普通数学语言也成为工作的一部分。他还说，尽管已发表的 PDF 很难读，他仍能理解 Navier–Stokes 论证中的思想。这些是他的评估，并非 BIG CHANGE 对证明的审计；我们没有运行 Lean 文件，也没有评审任一条定理。

NYU Courant 的[9月14日报道](https://cims.nyu.edu/dynamic/news/1528/)将 Buckmaster 和 Alpöge 的成就描述为：带光滑外力和有限能量初始数据的受迫三维 Euler 方程在有限时间内失去正则性。报道说，合作团队的三篇论文均以 Lean 形式化，并将结果置于 Diego Córdoba 和 Luis Martínez-Zoroa 开创的研究路径中。准确分配贡献时，这些细节很重要：模型生成的证明可以延展现有数学路径，同时不抹去奠定该路径的人。

## 快速发展的一系列事件中的两个结果

OpenAI 表示，其内部智能体系统最初产生了一个关于**无外力 Euler 方程**的结果，随后将这一研究方向用于其另一项 Navier–Stokes 构造。其[公告](https://openai.com/index/navier-stokes-solution/)承认 Buckmaster 和 Alpöge 在**受迫 Euler**结果上的优先贡献，同时称自己的证明是独立开发的。Buckmaster 在访谈中表示，这些数学机制彼此相关，并称 OpenAI 增加了一个关于涡旋塌缩的想法来处理黏性。双方叙述都认为这些主张涉及不同方程和证明步骤，但并未解决所有关于时间先后或智力贡献的问题。

欧洲数学 [学会](https://euromathsoc.org/news/ems-statement-on-recent-navier-stokes-announcement-225)欢迎了这项公告，同时强调此前的工作，并呼吁关注作者身份、贡献归属以及对内部模型的访问权。Clay 在[9月11日的回应](https://www.claymath.org/news/navier-stokes-announcement/)称 Navier–Stokes 问题*似乎*已经解决，但对成果的评估和贡献归属将谨慎进行，不会仓促决定。Buckmaster 告诉 Greene，他相信 OpenAI 已有解决方案。读者可以同时接受两种说法：专家的正面判断，以及机构仍在进行评估。

最近[OpenAI 另外三篇数学手稿撤回](https://bigchange.ai/blog/openai-withdraws-three-math-manuscripts-sign-error)是另一件独立事件。他们报告的符号错误说明应逐一检查各项主张；但这并不证明 Navier–Stokes 证明也有同样错误。BIG CHANGE 的[仓库检查指南](https://bigchange.ai/blog/openai-math-repository-manuscripts-formal-proofs)说明了如何查找手稿版本和证明材料；我们的[评审能力观点](https://bigchange.ai/blog/ai-research-discovery-review-capacity)则认为，解释和检查需要专门支持。[先前的 Navier–Stokes 报道](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes)记录了这一系列事件的起点。这次访谈补充了一位在职数学家的讲述：AI 系统提出论证之后会发生什么。

对于如此重大的主张，接下来有用的出版物包括精确易读的说明、可检查的形式化材料，以及独立的数学回应。它们各有作用。生成候选证明的速度让这些工作更加紧迫，而 Clay 声明的流程也为谨慎处理留出了空间。

## 来源与延伸阅读

- [World Science Festival 10月2日的节目](https://www.worldsciencefestival.com/programs/the-moment-ai-changed-mathematics-forever/)确认了访谈日期和参与者；[访谈视频](https://youtu.be/PQYFRuZ5phs)是 Buckmaster 本人讲述的来源。他的评估均归于本人。
- [NYU Courant 9月14日的报道](https://cims.nyu.edu/dynamic/news/1528/)说明了 Buckmaster 和 Alpöge 的受迫 Euler 结果、此前的数学工作以及 Lean 形式化。
- [OpenAI 9月8日发布、9月10日更新的公告](https://openai.com/index/navier-stokes-solution/),介绍了其声称的受迫 Navier–Stokes 构造、公开论文和 Lean 形式化，以及对同期工作的说法。这是提出结果一方的叙述，并非独立认可。
- [Clay 9月11日的声明](https://www.claymath.org/news/navier-stokes-announcement/)阐明了其谨慎的公开立场和评估流程。[European Mathematical Society 9月10日的声明](https://euromathsoc.org/news/ems-statement-on-recent-navier-stokes-announcement-225)讨论贡献归属、来源脉络和访问权。
- BIG CHANGE 关于[最初 Navier–Stokes 报道](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes)、[仓库检查](https://bigchange.ai/blog/openai-math-repository-manuscripts-formal-proofs)、[评审能力观点](https://bigchange.ai/blog/ai-research-discovery-review-capacity)以及[另外三篇手稿撤回报告](https://bigchange.ai/blog/openai-withdraws-three-math-manuscripts-sign-error)的报道，提供了这条发展中故事的背景。

## Sources

- [AI 永远改变数学的那一刻](https://www.worldsciencefestival.com/programs/the-moment-ai-changed-mathematics-forever/) — 节目身份、日期和访谈范围。
- [World Science Festival 访谈视频](https://youtu.be/PQYFRuZ5phs) — Buckmaster 对 AI 辅助 Euler 工作、Lean 检查、OpenAI 声明及后续评估的自述。
- [Tristan Buckmaster 构造带光滑外力的三维 Euler 有限时间爆破解](https://cims.nyu.edu/dynamic/news/1528/) — 机构对结果和先前工作的描述。
- [关于 Navier–Stokes 千禧年大奖问题](https://openai.com/index/navier-stokes-solution/) — OpenAI 作为结果提出方的主张，以及对同期工作的说法。
- [Navier–Stokes 声明](https://www.claymath.org/news/navier-stokes-announcement/) — Clay 谨慎的回应和评估流程。
- [欧洲数学学会关于近期 Navier–Stokes 声明的表态](https://euromathsoc.org/news/ems-statement-on-recent-navier-stokes-announcement-225) — 数学学会关于贡献归属和访问权的立场。