OpenAI数学解未达标准且存在形式化差距

OpenAI 本周发布的数百个数学问题解决方案未完全达到由普林斯顿高等研究院指导的 AGMAI 组织制定的标准，特别是缺乏人类对数学结果的理解和形式化验证。尽管 OpenAI 遵循了尽快发布结果和提供推理链的原则，但仅有 10 份稿件包含思维链释放，且仅 42% 的证明经过了形式化处理。 关键证据来自剑桥大学和伦敦国王学院数学家发表的新论文，该论文在 OpenAI 针对纳维 - 斯托克斯方程问题的解中发现了至少两处分歧：模型生成的自然语言解释与其试图编译为代码以确认准确性的 Lean 形式化表达之间存在不匹配。这种“翻译丢失”现象表明，不能单纯依赖模型将自然语言证明转化为机器可读的形式化代码而不经过人工审查。AGMAI 建议应包含关联自然语言和形式化产物的机器可读元数据，但 OpenAI 此次并未执行。 事实层面，OpenAI 确实发布了大量解并声称咨询了专家顾问团；推断层面，这反映出当前前沿实验室在解决数学问题时，AI 代理可能无法承担后续社区交流、知识应用及责任归属的角色；猜测层面，若缺乏人类理解介入，这些解可能难以被数学界真正采纳或用于解决其他问题。文章强调，当新结果由人类发现时，研究者需承担责任并通过论文、讲座等方式与社区互动，而目前 AI 输出尚不具备这一机制。