OpenAI在9月8日分享了一份由AI生成的纳维–斯托克斯千禧年大奖问题解答。材料显示，这份工作同时包含一篇解答说明，以及使用Lean编写的形式化证明。它把大模型生成数学内容与定理证明器结合起来，关注点不只是给出一段看似完整的推导，还包括如何将证明表达为可由形式化系统检查的对象。
这次发布包含什么
目前可以确认的内容有两部分：一份面向阅读的解答说明，以及一份Lean形式化证明。前者承担解释和论证的功能，后者则试图把相关证明转写为形式化语言，使证明步骤能够在Lean环境中进行检查。对于复杂数学问题，这种组合比单独发布自然语言答案更容易被复核，也更适合进一步分析证明中的定义、假设与推理环节。
但需要区分“发布了一份AI生成的解答”和“问题已经得到正式解决”。给定材料只说明OpenAI分享了这项工作，没有提供数学界确认、评审结果，或千禧年大奖问题相关机构的认定信息。因此，Lean形式化证明的存在，能够说明作者提供了机器可检查的证明材料，但不能仅凭摘要判断该证明是否完整、正确，也不能据此判断问题已经获得正式解决。
对AI数学能力的启示
这项工作体现了一个值得关注的方向：AI在科研中的产出，开始从自然语言层面的答案，延伸到可形式化、可检查的证明对象。Lean为这种验证提供了明确的技术载体，至少让讨论可以落到具体代码和证明结构上，而不是停留在模型输出是否“看起来合理”。
不过，形式化仍然依赖正确的问题建模、假设表达和证明实现。即使有形式化文件，外部读者仍需要理解它对应的数学命题，以及证明是否覆盖了原问题要求。对开发者而言，这更像是一种科研工作流信号：模型负责生成和组织候选论证，形式化系统负责检查可执行的证明表达，最终结论仍需要专业审阅。
我的判断
这次发布的价值，在于展示了AI生成数学解答与Lean形式化验证结合的实践形态，而不是已经足以证明纳维–斯托克斯问题被解决。它适合被视为可复核科研材料和技术路线案例。当前材料没有给出证明细节、验证结果或外部确认，因此不宜把它直接宣传为数学突破。判断其实际贡献，还需要阅读完整说明与Lean证明，并等待更充分的独立检查。