发生了什么？
Tristan Buckmaster 与 Levent Alpöge 报告了三维不可压 Euler 方程、二维无粘 Boussinesq 方程以及不可压多孔介质方程在光滑外力下的有限时间爆破结果；研究过程中 Claude 与 Codex 提供了大量实质性帮助，公开 Lean 产物则形式化了 Euler 与 Boussinesq 两项结果。
两位研究者明确将底层强迫爆破研究路线归功于 Diego Córdoba 与 Luis Martínez-Zoroa，并描述其使用 LLM 将该路线从较粗糙的外力条件推进到光滑外力及相关流体方程。公开的 `fluid_lean` 仓库包含 Euler 与 Boussinesq 定理的完整 Lean 开发，其文档将 Lean 代码归因于在 Alpöge 指导下工作的 Claude。
为什么重要？
该事件是一个少见且可检查度较高的案例：AI 对前沿数学研究作出实质性贡献，而研究路线、判断与主张责任仍由人类掌握。这些结果还立即成为同期 OpenAI Navier–Stokes 主张的重要历史背景，因此准确区分不同数学命题及其归属对 Chronicle 尤其重要。
重要性说明：该发布把三个重要流体方程中的光滑外力爆破新结果，与有明确记录的 LLM 实质性证明辅助，以及 Euler、Boussinesq 结果的公开 Lean 形式化结合在一起。若被接受为 H1，其历史意义来自前沿数学研究中的人类主导 AI 协作，而不是 AI 从零提出了底层研究路线。
证据与状态一览
- 重要性
- H1 · 历史里程碑
- 验证状态
- 部分核验
- 证据等级
- E3 · 可检查工件
- AI 角色
- 人机协作
- 形式保障
- 有形式化工件
如何理解这些标签？ →
贡献与验证
- 数学新颖性
- 新结果
- 接口
- 非形式化, 形式化, 符号, 混合
- AI 贡献
- Buckmaster 的公开说明称项目全过程使用了 Claude 与 Codex，并由 LLM 在推进既有研究路线时提供大量帮助。公开的 Euler 与 Boussinesq Lean 仓库说明，包括可信 statement 文件在内的全部 Lean 代码均由 Claude 在 Alpöge 指导下编写。作者同时明确说明，底层研究路线并非由 LLM 原创提出。
- 人类贡献
- Buckmaster 与 Alpöge 选择并推进研究方向、评估与组织数学论证、撰写公开稿件，并对最终主张负责。他们将基础性的强迫爆破研究路线归功于 Córdoba 与 Martínez-Zoroa；Alpöge 还指导并审阅了公开 Lean 形式化流程。
- 验证状态
- 部分核验 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-11
技术细节
- 系统
- claude, codex, lean, mathlib
- 机构
- —
- 数学问题
- forced-euler-blowup, forced-boussinesq-blowup, forced-ipm-blowup
- 方法
- human-ai-collaboration, proof-development, formal-theorem-proving, lean
验证历史
- 2026-09-08 · 论文已发布 · E3 · 可检查工件
三份稿件与一个公开 Lean 仓库同期发布。该仓库包含 Euler 与 Boussinesq 的专门形式化项目，而公开仓库目录中没有对应的 IPM Lean 项目。
- 2026-09-11 · 部分核验 · E3 · 可检查工件
Terence Tao 独立讨论了这项数学工作及其与 Córdoba–Martínez-Zoroa 研究路线的关系；OpenAI 也独立承认 Buckmaster 与 Alpöge 在 forced Euler 结果上的优先权。这些来源佐证了事件及其历史背景，但 Chronicle 不据此认定三个底层定理均已得到独立验证，也不视为对 Lean 产物的独立重放。
