OpenAI于9月8日公布一个内部系统生成的Navier–Stokes千禧年难题候选解，并同时发布论文说明与Lean形式化证明。官方表示该构造展示受力三维流体可能在有限时间形成奇点，也明确不准备申领奖项。无论数学界最终如何审阅，这一事件都说明AI科研成果必须从“模型给出答案”升级为可机器检查、可专家复核、可讨论优先权的完整证据链。
自然语言证明为何不够
数学证明中一个量词、边界条件或光滑性假设被忽略，就可能让整套推导失效。语言模型文字流畅并不能保证逻辑闭合。研究团队应列出定义、前提、关键引理和依赖关系，让每一步都能独立审查。
Lean形式化能解决什么
Lean把证明转换成计算机可检查的形式，能够发现类型、依赖和逻辑缺口，但形式化只证明编码进去的陈述。如果问题表述、定义或外部公理有误，验证通过也不代表原始科学问题已解决，因此仍需数学家检查形式化与题意一致。
独立复现与压力测试
第三方应在独立环境编译证明，检查依赖版本、公理使用和隐藏自动化。专家还要尝试找反例、简化构造并比较已有文献。发布源代码、环境和可读说明，才能让评议超越对模型权威的信任。
大规模搜索的成本与边界
官方披露多组Agent长时间探索并使用极大规模信息交互。此类成果不能直接推断普通模型在一般数学问题上同样可靠。报告应同时说明计算投入、失败路径、人工指导和筛选过程，避免只展示成功结果。
优先权与数据责任
并行研究可能出现相近方向，团队需保存时间线、提示和中间结果，并主动处理学术优先权。还要确认训练与产品数据政策，避免未经授权使用他人私有研究。最终论文责任仍由署名研究者承担。
进一步实施建议
普通研究团队可从已有答案的定理开始：让模型生成证明、形式化并与标准解比较。等工具链稳定后再探索开放问题。每个候选结论设置“未验证、自动验证、独立复核、专家认可”四个状态，页面与论文不能提前把候选写成已确认事实。
落地检查清单
- 核对形式化陈述与原问题完全一致。
- 第三方独立编译并检查依赖和公理。
- 公开计算投入、人工干预和失败范围。
- 保存研究时间线并尊重学术优先权。
