热点事件持续更新
论文质疑OpenAI纳维-斯托克斯证明自动形式化
2 篇报道2 个报道来源2 小时前更新
先了解这件事
AI 综述
2026年9月，OpenAI公布一份166页的纳维-斯托克斯方程相关证明，称约1万个AI智能体在88小时内得出结果，并用17小时完成Lean形式化及验证。10月8日，Hacker News热门讨论（buzzing.cc中文翻译）报道一篇arXiv论文。该论文指出，AI将自然语言数学文本自动形式化为Lean语言后通过机械验证，并不必然证明原自然语言论证本身可靠；论文称消解数学自然语言歧义在Solvability Complexity Index（可解性复杂度指数）层级中SCI=∞，并给出多个AI误译案例。作者还表示，OpenAI该证明中的Lean形式化证明与自然语言证明并不对应，从而对自动形式化环节的有效性提出质疑。10月17日IT之家报道称，该证明遭数学界质疑，多智能体的实际贡献仍不明。目前报道仅涉及论文及外界的质疑主张，尚未见OpenAI方面的回应。
AI 根据报道生成 · 1 小时前更新
最新进展10月17日 18:31
10月17日报道称该证明遭数学界质疑，多智能体实际贡献仍不明。事件进展
2 个进展
- 10月17日 18:31 · 1 篇报道学界质疑OpenAI纳维-斯托克斯证明方法IT之家：OpenAI 纳维-斯托克斯方程证明遭数学界质疑，多智能体实际贡献仍不明
- 10月8日 01:10 · 1 篇报道论文质疑OpenAI纳维-斯托克斯证明自动形式化Hacker News 热门（buzzing.cc 中文翻译）：arXiv 论文称 OpenAI 纳维-斯托克斯证明的 Lean 形式化与自然语言证明不对应
报道时间线
沿着报道，了解事件的不同侧面。
10月17日
- IT之家OpenAI 纳维-斯托克斯方程证明遭数学界质疑，多智能体实际贡献仍不明
OpenAI 今年 9 月公布 166 页纳维-斯托克斯方程相关证明，称约 1 万个 AI 智能体在 88 小时内得出结果，并用 17 小时完成 Lean 形式化及验证。
10月8日
- Hacker News 热门（buzzing.cc 中文翻译）arXiv 论文称 OpenAI 纳维-斯托克斯证明的 Lean 形式化与自然语言证明不对应
一篇 arXiv 论文指出，AI 将自然语言数学文本自动形式化为 Lean 后通过机械验证，并不必然证明原自然语言论证可靠。论文称消解数学自然语言歧义在 Solvability Complexity Index 层级中 SCI=∞，并给出多个 AI 误译案例；作者还表示 OpenAI 公布的纳维-斯托克斯方程解爆破证明中，Lean 证明与自然语言证明不对应。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。