堆代码网讯 本周OpenAI公布了数百个号称能解答全球顶级数学难题的成果，这家前沿AI实验室表示，已提前咨询由顶尖数学家组成的顾问小组，避免重蹈此前模型破解领域长期难题时引发的争议。但OpenAI最终未能达标，尤其在数学家强调的“人类必须能理解数学推导结果”这一核心要求上存在明显短板。此前一篇新论文就指出，OpenAI模型声称破解的百万美元级难题，其自然语言表述版本与形式化表述版本的解答之间存在明显偏差。

由普林斯顿高等研究院牵头成立的数学与人工智能顾问小组（AGMAI），成员来自全球各地的9位顶尖数学研究者。该组织在9月底面向前沿AI实验室发布了数学问题求解的相关指南。针对OpenAI最新发布的这批证明成果，AGMAI在声明中表示：“相关指南的落地效果，最终要由整个数学界来评估”。但该组织的首条要求就是“禁止在闭源模型上测试前沿数学问题”，而OpenAI本次发布的内容明确说明，其正是用公开数学研究难题来评测自家闭源模型。

TechCrunch就OpenAI最新的证明成果向该顾问小组申请更全面的评估，暂未得到回应。OpenAI确实遵循了部分指南原则，比如第一时间公开成果、附上模型得出结论的相关过程信息，但并未覆盖全部要求：719份文稿中，仅10份公开了模型的完整思维链。针对人类无法理解的证明内容，数学家建议必须完成形式化校验，但OpenAI发布的证明里，仍有42%的内容未经过这一流程。

最终来看，目前仍无法确认OpenAI在发布这些证明时，是否按照AGMAI的原则，承担起“确保后续人类能完成对成果的理解”的责任。AGMAI曾建议OpenAI提供资金支持人类数学家开展相关工作，让这些AI生成的解答真正具备实际学术价值。知名数学家陶哲轩此前就曾批评过OpenAI的相关做法，他在本次成果发布后于社交媒体发文表示：“现在很多AI提示工程师能自主‘解出’难题，但他们本身对整个数学领域毫无兴趣，达成初始目标后就不再跟进，也完全看不懂AI的输出，没法针对结果答疑、做学术分享，更无法和领域内其他研究者开展交流。”

剑桥大学与伦敦国王学院的数学家本周发布的一篇论文，就集中体现了这一问题，直指前沿AI实验室当前的解题思路存在明显缺陷。AI模型求解数学题时，会先生成“自然语言”版推导说明，再尝试用Lean编程语言将结果转化为形式化代码——理论上通过编译代码就能验证证明的准确性。但模型将自然语言证明转化为代码的过程很容易出问题：这篇论文就记录了OpenAI针对纳维-斯托克斯方程衍生难题给出的解答中，自然语言证明和背后的Lean代码之间，至少存在两处不一致。

这些偏差未必能直接推翻两个版本的解答，但足以引发质疑：我们是否能完全脱离人类，单纯依赖模型自行完成解答的形式化校验。这也是AGMAI要求OpenAI“加入机器可读元数据，关联自然语言内容与形式化产物”的原因，而OpenAI本次发布的成果完全没有做到这一点。这篇名为《翻译迷失》的论文作者总结道：“正如本文指出的误译现象，OpenAI的自然语言证明以及其他自动形式化生成的Lean证明，在没有经过和普通数学证明同等的同行评审与严格核验前，绝不能直接默认其可信。”

数学家们强调，人类得出新的数学成果时，会为结果全权负责，通过论文、学术报告、研讨会和整个领域开展交流。这个过程能深化对解答的理解，提炼出可迁移到其他问题的解题思路，还能让新知识落地到实际应用领域。

哈佛大学数学教授Melanie Wood在接受TechCrunch采访时表示：“当模型被提示去解一道难题、输出一个结果时，发布的当下根本没有人类真正理解它，所有后续的验证和理解工作才刚刚开始。”