本周，OpenAI 公布了对一系列高难度数学问题的数百个解决方案。然而，这一成果并未完全达到数学界设定的评估标准，尤其是在强调人类对结果理解方面。
随着一篇新论文指出自然语言描述与形式化表达之间存在显著差距，外界对前沿实验室在解决复杂数学问题时的透明度提出了质疑。
普林斯顿咨询小组的准则与挑战
由普林斯顿大学高级研究院主办的“数学和人工智能咨询小组”（AGMAI）汇聚了全球九位著名研究人员。该组织于9月底发布了针对前沿实验室解决数学问题的指南，并明确表示：“最终由数学界来评估我们的建议是否得到了成功的执行。”
AGMAI的首要要求是“停止在专有模型上测试先进的数学问题”。但 OpenAI 此次发布明确指出，其评估基于专有模型对数学开放研究问题的解答能力。
当 TechCrunch 请求对该证据发布进行更彻底的评估时，AGMAI未予回应。尽管实验室遵循了部分原则，如尽快公布结果及说明模型如何得出结论，但在719份手稿中，仅有10份包含了模型的思维链信息。
此外，数学家建议对于人类难以理解的论文，证明应当被正式化。然而，OpenAI发布的证明中仍有42%未经过这一过程。
专家批评：缺乏责任归属与社区互动
目前尚不清楚 OpenAI 是否在发布证据时履行了 AGMAI 所要求的“确保人类理解的责任”。AGMAI 建议实验室应资助人类数学家的工作，以赋予这些解决方案实际意义。
著名数学家陶哲轩（Terence Tao）在社交媒体上批评了 OpenAI 的方法。他指出，这些问题是由人工智能提示者自主解决的，一旦达成目标，他们便对更广泛的领域失去兴趣，且不了解人工智能的输出是否足以回答相关问题、发表演讲或与其他领域互动。
哈佛大学数学教授梅拉尼·伍德（Melanie Wood）告诉 TechCrunch，当一个模型被要求解决难题并输出解决方案时，往往缺乏传统学术流程中的责任承担机制。数学家强调，人类发现新结果时会通过论文、演讲和研讨会与社区互动，这一过程不仅加深了对解法的理解，还能发现可复用的策略并推动知识在实际领域的应用。
形式化验证中的“翻译失败”风险
剑桥大学和伦敦国王学院的数学家本周发表了一篇论文，深入探讨了前沿实验室面临的挑战。当 AI 模型解决数学问题时，通常先生成“自然语言”解释，随后尝试将其转化为 Lean 语言——一种理论上可通过编译代码确认证明准确性的编程语言。
然而，将自然语言验证转化为代码的过程可能存在缺陷。该论文记录了至少两处差异，出现在 OpenAI 提供的从纳维埃-斯托克斯方程（Navier-Stokes equations）衍生出的流体行为复杂性问题解决方案中，即自然语言证明与其背后的 Lean 代码之间不一致。
虽然这些差异并不直接反驳解决方案的有效性，但它们引发了一个核心问题：我们是否可以依赖模型在没有人类参与的情况下自行制定形式化解决方案？这也是 AGMAI 要求 OpenAI “包括机器可读的元数据来关联自然语言和形式文物”的原因之一。
鉴于这种“翻译失败”现象，论文作者得出结论：在没有经过同等同行评审过程和审查的情况下，不应信任 OpenAI 的自然语言证明及其他自动形式化的 Lean 证明。
