OpenAI发布722篇AI数学手稿引争议：证明过剩与透明度危机
OpenAI近日发布由未公开内部模型生成的722篇数学研究手稿，声称涵盖纳维-斯托克斯方程等重大难题，但引发数学界强烈质疑。主要争议点包括模型缺乏透明度、Lean形式化验证存在不一致、以及优先权归属问题。数学家担忧AI快速生成大量“证明”导致人类无法有效消化和验证，可能破坏科研信任体系。
事件概述
美东时间10月6日，OpenAI发布了一份包含722篇数学研究手稿的清单，这些成果由一款尚未公开的专有内部模型生成。官方宣称，每项成功结果平均消耗的算力相当于ChatGPT Pro思考3小时。手稿涵盖四维Kakeya猜想、广义黎曼猜想相关问题等372个成果类别，其中162篇附有主结果的Lean形式化证明。
核心争议
1. 透明度缺失与复现困难
OpenAI发言人向《科学美国人》表示，几乎所有结果是在向单个代理发出单一指令后生成的，且未公开发布新模型。顶尖数学家如麻省理工学院的安德鲁·萨瑟兰指出，除非公布完整模型、具体提示信息和计算过程以允许独立复现，否则任何关于单智能体一次性解决复杂问题的说法都应视为未经证实。
2. Lean验证存在技术瑕疵
尽管OpenAI提供了Lean形式化证明，但米兰比可卡大学副教授瓦莱里奥·卡普拉罗发现其纳维-斯托克斯方案的论文与Lean代码至少存在两处不一致：
- 论文中的估计仅需四个额外输入导数，而Lean版本需要五个，导致形式化结果较弱。
- 压力-通量估计采用了不同的界限和证明方法。
Lean仅能检查逻辑形式错误，无法判断证明内容是否真正对应原难题或具备新意，因此验证不等于数学界的最终认可。
3. 优先权争议与学术伦理
在OpenAI官宣解决纳维-斯托克斯千禧年难题前12小时，纽约大学数学家特里斯坦·巴克马斯特与Anthropic合作者莱文特·阿尔珀格已公开相近成果（使用Claude、Codex等模型）。巴克马斯特批评OpenAI处理不当，曾要求排除其合作者署名，OpenAI则否认使用私人数据并称研究独立完成。此外，OpenAI在发布后因符号错误撤回了3篇手稿并修改了14篇，暴露出生成内容的可靠性问题。
行业影响：证明过剩危机
此次发布引发了对“证明过剩”的担忧。数学界传统上依赖缓慢、严谨的消化流程来建立信任（如四色定理的形式化验证耗时数十年），而OpenAI一次性倾倒700多篇手稿，远超人类数学家的阅读和理解能力。陶哲轩等学者强调，数学的核心在于概念理解和理论发展，而非单纯的答案生成。若AI竞赛导致未经充分验证的成果泛滥，可能破坏数学研究的根基和信任机制。