2026年9月8日，OpenAI公开了一份166页的Navier–Stokes有限时间奇性证明稿和配套的Lean 4形式化仓库。证明稿声称：对任意正黏度，都可以构造从静止开始、受光滑外力作用的三维不可压缩流体，使速度在有限时间内无界，同时动能保持有界；作者据此认为自己建立了Clay数学研究所正式问题说明中的C和D两种“失效”情形。OpenAI还报告，约一万个并行智能体用88小时得到结果，GPT-6 Astra又用17小时完成Lean形式化。独立报道确认了材料公开和这些开发者数据，但没有确认定理已经被数学界或Clay接受。仓库元数据把审查状态写为“self-assessed”，截至本文写作时也没有公开的完整独立复核结论。
这里真正值得讨论的问题不是AI是否比人更快，也不是智能体能否取得研究者身份，而是：当一项AI生成的数学结果已经有可以构建和检查的形式证明时，我们是否应当说数学知识已经确立？
至少需要区分四件事。第一，系统生成了一段看似合理的数学文字。第二，Lean接受了某个形式陈述的推导。第三，这个形式陈述准确表达了人们原本要解决的数学问题。第四，数学共同体有充分理由把结论纳入可依赖、可解释、可继续使用的公共知识。前两者可以由本次公开材料直接加强；后两者却不会自动随编译成功而完成。
形式验证的认识价值不能被低估。与只给出自然语言答案相比，证明助手要求每一步都落在明确的定义、类型、定理和推理规则中。OpenAI仓库还给出固定的Lean版本、依赖项、构建指令、主定理位置、所用公理和独立检查工具的入口，并报告主要结果没有未完成的sorry占位。这些条件大幅压缩了含糊跳步和局部逻辑错误可以藏身的空间。任何能够取得代码的人，原则上都可以重新构建，并检查形式推导是否被指定的内核接受。就证据结构而言，这远强于开发者内部基准、语言模型的自信陈述，甚至强于一篇只有自然语言而无法逐步检查的长证明。
但Lean接受的是“在这些定义、这些公理、这些库和这个内核下，此形式定理可由前提推出”。它不会凭自身判断该定理是否忠实对应Clay问题中的C和D，也不会自动识别某个数学定义虽然在形式上良好，却遗漏了原问题意图中的条件。形式化者必须完成从数学语境到符号对象的翻译；内核检查翻译后的推导，却不能独自保证翻译前后的问题相同。OpenAI使用了Formal Conjectures提供的参照陈述来比较这种对应，这是重要的加强，但仓库对齐说明仍是发布方自己的报告，需要外部专家核查定义、定理范围和参照之间是否真正等价。
数学知识也不只是一个布尔值式的“通过”。一个结论要进入研究共同体，其他人需要知道证明依赖什么、关键构造为何有效、它与已有理论怎样衔接，以及在受到反例、不同形式化或细节质疑时能否被修正。形式证书尤其擅长回答推导是否合规，却未必自动提供这种解释。166页证明稿中的物理描述、证明纲要和完整估计，正是在连接形式正确性与数学理解；而专家阅读、独立重建和替代检查，则是在检验这条连接是否牢固。
这不是把真理交给多数投票。若一个正确形式化的定理已经由可靠内核推导出来，共同体不能靠不喜欢它而使它为假。问题在于，我们当前要判断的对象不是抽象的推导串，而是“这个仓库证明了Clay所问的Navier–Stokes命题”这一复合主张。复合主张包含定理表述、语义对应、软件信任、依赖管理和数学解释。它们中的任何一项出现错位，都可能使“形式证明有效”和“原问题已解决”同时一真一假。
从维成论看，Difference首先要求把自然语言论文、Lean定理、Clay原问题和公共知识主张区分开来；这些不是同一对象的四种名称。Constraint不是泛指限制，而是定义、公理、类型系统、库版本、内核、构建环境和同行质疑共同构成的形成条件：它们使某些推导可以成立，也排除另一些推导。Sustained Coherence则要求形式陈述、非形式证明、原始问题和独立复核之间的对应，在重复构建、专家审查、反例搜索和版本修正中持续保持一致。这里的“持续”很重要，因为一次成功构建只能证明某个固定状态下的形式关系，不能替代跨工具、跨解释和跨审查者的校正。
我的判断是，这次公开材料已经建立了一个强度很高、可公开检验的数学知识候选。若仓库能由独立团队重建，形式陈述与Clay原命题的对应得到专家确认，证明稿的关键构造和估计也经得起审查，那么形式验证完全可以成为数学知识确立的核心部分，而不只是辅助证据。但在当前阶段，最准确的说法仍是：OpenAI公开了一项带有机器可检验证书的解决主张；形式系统内的推导获得了开发者自评支持，公共数学知识的完整确认过程尚未完成。
这个判断不要求每位数学家亲自读完每一行代码，也不预设AI不能产生真正的新数学。它只限定我们今天可以从现有证据推出什么。未来最有辨别力的证据不是更多模型自述或更大的智能体数量，而是独立构建记录、形式陈述的语义审计、专家对关键构造的复核、可回答的具体异议，以及发现错位后可追踪的修订。
参考资料
https://openai.com/index/navier-stokes-solution/
https://github.com/openai/NavierStokesAndEuler
https://plato.stanford.edu/archives/sum2026/entries/mathematical-practice/
了解 Geoffrey Chen 的更多信息
订阅后即可通过电子邮件收到最新文章。