主要证据
- On the Navier–Stokes Millennium Prize ProblemS2 · 官方机构来源 · 官方公告 · 2026-09-08
- Finite Time Blowup for Navier–StokesS1 · 主要研究来源 · 论文 · 2026-09-08
- Lean certificates accompanying Navier–Stokes and Euler resultsS1 · 主要研究来源 · 形式化工件 · 2026-09-08
OpenAI 发布 AI 生成的 Navier–Stokes 千禧年问题解答主张及 Lean 形式化
OpenAI 表示成功搜索约使用 10,000 个并发 Agent 工作约 88 小时，随后继续进行 Lean 形式化与验证。独立报道确认了这一发布事件，同时也记录了围绕 Tristan Buckmaster 与 Levent Alpöge 同期工作的归属、来源与优先权争议。
发生了什么？
OpenAI 报告一个大规模协同 Agent 系统构造了有限时间奇点，声称解决 Navier–Stokes 千禧年问题官方表述中的 C 与 D，并提供 Lean 形式化。
OpenAI 表示成功搜索约使用 10,000 个并发 Agent 工作约 88 小时，随后继续进行 Lean 形式化与验证。独立报道确认了这一发布事件，同时也记录了围绕 Tristan Buckmaster 与 Levent Alpöge 同期工作的归属、来源与优先权争议。OpenAI 现表示，经调查确认，Buckmaster 在 9 月 8 日发布前两个月内提交给 Codex 的 prompts 不可能以任何方式影响该系统，包括通过训练产生影响。这一直接声明缩小了 provenance 争议中的一个子问题，但围绕归属、优先权和合作过程的其他争议仍然存在于公开记录中。
为什么重要？
由于该主张涉及千禧年难题，并立即引发广泛独立审视与争议，无论其数学结论最终如何，该事件本身都具有历史重要性。证明本身、优先权、归属与共同体接受度仍应由外部数学与历史证据持续评估。
重要性说明：公开发布的 AI 生成千禧年难题解答主张本身就是历史级 AI4Math 事件，无论其底层数学结论最终能否经受住审查。H1 记录事件的重要程度；verification 则另行记录独立佐证、争议以及后续历史变化。
历史脉络
证据与状态一览
- 重要性
- H1 · 历史里程碑
- 验证状态
- 存在争议
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 自主主导
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 新证明
- 接口
- 非形式化, 形式化, 符号, 混合
- AI 贡献
- OpenAI 将核心构造归因于由内部模型驱动的多 Agent 协同系统，并使用 GPT-6 Astra 完成形式化与验证。
- 人类贡献
- OpenAI 研究者选择目标表述、组织评测并发布证明。Tristan Buckmaster 与 Levent Alpöge 当时正独立开展同期流体动力学研究，并非 OpenAI 证明的贡献者；他们的研究、对前沿 AI 工具的使用以及后续公开说明成为归属、来源与优先权争议的核心背景。外部数学家、数学机构与记者仍在持续审视该主张及其历史语境。
- 验证状态
- 存在争议 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-17
技术细节
- 系统
- openai-internal-model, gpt-6-astra, lean
- 机构
- openai
- 数学问题
- navier-stokes-existence-and-smoothness
- 方法
- multi-agent, autonomous-research, formalization, lean
全部来源与工件
- On the Navier–Stokes Millennium Prize ProblemS2 · 官方机构来源 · 官方公告 · 访问于 2026-09-17
- Finite Time Blowup for Navier–StokesS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- Lean certificates accompanying Navier–Stokes and Euler resultsS1 · 主要研究来源 · 形式化工件 · 访问于 2026-09-10
- OpenAI claims to have solved maths problem that stumped humans for decadesS4 · 可信二手来源 · 媒体报道 · 访问于 2026-09-10
- OpenAI's historic math solution overshadowed by credit controversyS4 · 可信二手来源 · 媒体报道 · 访问于 2026-09-11
- Position of the SMF board on the recent announcements of OpenAIS2 · 官方机构来源 · 官方公告 · 访问于 2026-09-17
验证历史
- 2026-09-08 · 核验中 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-08 · 已有独立佐证 · E3 · 可检查工件
独立报道确认了该事件的核心事实：OpenAI 公开宣布这一千禧年问题解答主张，发布证明稿与 Lean 形式化，并披露大规模多 Agent 搜索过程。这一事件级佐证并不认证底层数学主张的最终正确性。
- 2026-09-10 · 已有独立佐证 · E3 · 可检查工件
Chronicle 已确认公开的 166 页证明稿，以及形式化 Navier–Stokes 与 Euler 结果的 Lean 4 仓库。这些一手产物加强了证据记录并支持 machine-checked formal assurance；对底层数学主张的独立数学评估与事件级佐证属于不同问题。
- 2026-09-10 · 存在争议 · E3 · 可检查工件
可靠独立报道同时记录了围绕 Tristan Buckmaster 与 Levent Alpöge 同期工作的归属、来源与优先权争议。因此 Chronicle 将当前事件状态记为 `disputed`，同时保留“发布事件本身已获独立佐证”这一事实。
- 2026-09-11 · 存在争议 · E3 · 可检查工件
Axios 独立记录了 Buckmaster 与 Alpöge 对来源和署名的担忧，并报道了 OpenAI 当时公开给出的边界：公司称证明过程中没有访问两人的特定用户数据，同时对去标识化产品使用数据是否曾间接改善模型保留不确定性。这一证据进一步明确了 provenance 记录，但并不能证明这种间接使用确实发生。
- 2026-09-17 · 存在争议 · E3 · 可检查工件
OpenAI 当前公开说明称，经调查确认，Buckmaster 在 9 月 8 日公告前两个月内提交给 Codex 的 prompts 不可能以任何方式影响该系统，包括通过训练产生影响。这一声明实质性缩小了此前记录的 prompt-training provenance 不确定性。事件仍保持 `disputed`，因为公开记录中仍存在相互独立的归属、优先权与合作过程争议。法国数学会 9 月 15 日发布的正式立场也表明该事件仍持续引发机构层面的关注，但并未对底层证明作独立数学裁决。
更正
- 2026-09-10
将标题明确为 OpenAI 发布的“解答主张”，而非 Chronicle 自身对问题已解决的裁决，并记录独立报道中的归属 / 来源争议。