一个经Lean验证的证明仍可能证错问题版本
摘要
本文探讨了OpenAI针对Navier-Stokes问题的Lean证明的验证，强调了确保形式证明与预期数学问题一致的重要性，以及数学家进一步审查的必要性。
我一直关注AI/Navier-Stokes事件，仍在试图弄清楚究竟证明了什么。OpenAI表示其系统构建了一个平滑的三维流体，从静止开始，施加平滑外力，并在有限时间内发展出奇点。它还发布了在Lean中验证的形式证明。Lean检查结论是否从编码的定义和假设中推导出来。仍需有人确认这些定义准确代表了原始的Clay问题。这就像软件通过了所有测试，但仍未能满足需求，因为测试衡量了错误的东西。
因此，我将OpenAI的论文、Clay问题陈述和一些解释提供给Apodex，并要求它将每个官方要求映射到新结果的相应部分。我想看看初始条件、外力、能量界限和奇点声明是否一致。这包括检查每个逻辑步骤、确认Lean陈述与分析论文匹配，以及验证论文是否回答了Clay提出的问题。数学家仍需理解并独立审查该构造。"Lean已验证，所以官方解决了"说得太过分。但"它使用了外力，所以不算数"也可能错误，因为官方表述的部分内容允许在指定条件下使用平滑外力。Clay的奖金规则要求在合格期刊上发表、发表后至少两年，并在数学界普遍接受后才予以考虑。对于从事形式证明的人：如何检查Lean中编码的定理是人类意图证明的定理？
相似文章
OpenAI的Navier-Stokes发布包含了Lean 4的形式化证明
OpenAI宣布使用Lean 4为Navier-Stokes方程提供了形式化证明，将形式化验证的成本从数万小时减少到仅17小时，突显了人工智能在数学和验证中的变革性作用。
Navier–Stokes：失之翻译
本文论证了用 Lean 对 AI 自动形式化进行验证，并不能保证原始自然语言证明的正确性：语义忠实的翻译在可解性复杂度指数层级中是不可判定的。作者展示了实际存在的 AI 误译案例，其中包括 OpenAI 宣布的 Navier–Stokes 爆炸证明中的一处不一致。
数学家应该了解的 Lean 定理证明器：可靠性与人工智能
Thomas Hales 为 Terence Tao 的博客撰写客座文章，介绍了数学家应该了解的 Lean 定理证明器相关知识，涵盖形式化证明的可靠性、mathlib 库的发展，以及 AI 驱动的自动形式化如何在 2026 年成为现实。
研究者已在 OpenAI 最新数学成果基础上取得显著改进，并经 Lean 形式化验证
研究者正迅速超越 OpenAI 近期由 AI 生成的数学成果，改进后的证明已通过 Lean 进行形式化验证，凸显了 AI 辅助定理证明领域的飞速进展。
OpenAI 的 Lean 4 Navier-Stokes 证明零错误编译通过，但流体在 0.7 纳米处汽化。这对神经符号 AI 意味着什么？[D]
一个研究团队对 OpenAI 的 Lean 4 三维 Navier-Stokes 爆炸形式化证明进行了审计，发现该解在数学上虽完全成立，但在原子尺度上会物理失效（流体在 0.7 纳米处汽化）——这是一种典型的规格博弈（specification gaming）。他们提出为神经符号 AI 系统增加一个物理边界层，并开源了其验证脚本。