OpenAI数学证明未达学界标准：自然语言证明与Lean形式化代码出现矛盾，数学家提出质疑
OpenAI近期公开数百份号称攻克高难度数学难题的AI解答，为规避此前AI证明引发的学术争议，官方表示本次项目征询了精英数学家咨询小组的意见。但来自数学界的反馈显示，这批成果并未达到该领域通行的学术标准，核心争议集中在AI产出的证明缺少人类层面的理解，自然语言论证和Lean形式化代码之间存在断层。
由普林斯顿高等研究院主办、汇集9位全球顶尖学者的数学与人工智能咨询小组AGMAI，早在9月底就发布了AI实验室开展数学研究的规范指南。AGMAI的首要诉求之一，就是停止在闭源专有模型上测试前沿数学开放问题，但OpenAI本次发布，恰恰使用这类专有模型来评估开放数学猜想。
OpenAI落实了部分AGMAI原则，比如及时公开成果、附带模型推导的相关信息，但大量要求并未满足：719份手稿里，仅有10份附带模型的思维链记录；仅有42%的证明完成形式化校验。同时缺少能够关联自然语言文本和形式化产物的机器可读元数据，而这是AGMAI明确提出的要求。按照准则，OpenAI还应当资助数学家跟进核验，真正让AI产出的结论具备可被人类理解的完整论证。
菲尔兹奖得主陶哲轩在社交平台上表达了担忧。他认为当前模式下，AI提示工程师只以“完成解题目标”为终点，本身并不深耕对应的数学领域，也无法解读AI产出、在学术圈交流分享，AI的证明产出之后，没有配套的学术沟通与阐释环节。
剑桥大学与伦敦国王学院数学家新发表的论文《lost in translation》，用纳维-斯托克斯方程相关问题作为案例，直观暴露了漏洞：OpenAI给出的自然语言版本证明，在转换成Lean验证代码的过程中，至少存在两处不一致。这些矛盾虽不能直接推翻结论，但足以警示，不能直接信任AI自主完成的形式化转换。
Lean这类形式化证明语言的思路，是把数学证明编译成代码来核验正确性。但AI在翻译论证逻辑的过程中会出现“误译”，因此论文作者强调，OpenAI的这类成果，必须和人类数学家论文一样，经过完整同行评审，不能直接采信。
哈佛大学数学教授Melanie Wood向媒体总结了核心矛盾：人类数学家发布新定理时，本身已经吃透整个论证，能够向学界讲解、延伸出新方法；但AI输出证明的瞬间，人类还没有理解这套论证，真正的核验工作才刚刚开始。
要点小结
- 核心事件：OpenAI发布719份AI生成数学手稿，声称解决多项高难度数学开放问题，但遭到数学界质疑，未满足学术规范。
- AGMAI准则冲突：不建议在闭源模型测试前沿数学问题；大量手稿缺少思维链、形式化覆盖率不足，缺失关联元数据。
- 关键缺陷：AI自然语言证明转Lean形式化代码存在翻译偏差，两套内容出现逻辑出入，无法独立自证可靠。
- 学界观点：数学成果不只是“得出答案”，还需要人类理解、同行评审、学术交流；AI输出证明不等于完成数学研究。
- 陶哲轩等学者提出警告：当前AI解题流程缺少研究者深度参与，产出成果很难直接融入数学共同体。
