# 陶哲轩博客发了一篇客座文章：AI 解出纳维-斯托克斯问题，不代表数学被终结了

> 原标题：After Math

- 来源：Hacker News 首页
- 发布时间：2026-09-13T03:16:41.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/56228
- 原文：https://terrytao.wordpress.com/2026/09/12/after-math/

## 摘要

9月8日 OpenAI 宣布用 AI 生成了纳维-斯托克斯存在性与光滑性问题的解答，还附上了 Lean 形式化验证和一份手稿。客座作者 Silvia De Toffoli 和 Eamon Duede 直接泼了盆冷水：逻辑上有效的证明不等于数学家要的证明。数学家需要的是能读懂、能消化、能接着往下推进的“可理解的证明”，而 AI 给出的东西目前还漂在形式逻...

## 推荐理由

陶哲轩的平台、两位署名学者、直接回应 OpenAI 9 月 8 日的声明，这三样加在一起让这篇文章分量很重。它不止是表态，而是提出了“可理解的证明”这个具体框架，把形式验证和数学研究之间的鸿沟说清楚了。对 AI 从业者来说，这比一百篇“AI 又赢了”的标题都有用，所以我会给 featured 并打 78 分——信息密度高，但正文没给出更多技术细节，分数先不打满。

## 锐评

这篇文章给 OpenAI 的“数学里程碑”泼了盆冷水，核心论点很清晰：数学不只是解题，证明也不只是逻辑校验。作者区分了“逻辑有效”和“可理解”两种证明，认为 AI 目前给出的东西，即便通过了 Lean 形式化验证，也还漂在形式逻辑层面，人类数学家读不懂、消化不了，更没法接着往下推进。这个判断直接否定了“AI 解决数学”的叙事。

文章没去纠缠技术细节，而是从数学实践的本质出发，指出数学是发展概念、统一领域、维持学术共同体的事业，不能简化成下棋式的输赢游戏。这个视角很有力，但正文没披露 OpenAI 模型架构、训练数据或算力成本，也没说明那份“非形式化手稿”到底可读到什么程度。所以，AI 的证明究竟是彻底的天书，还是只是目前没人愿意花时间啃，这点还缺关键信息。如果是前者，那 OpenAI 的宣称确实该打折；如果是后者，讨论可能得换个方向。