OpenAI 的数学解决方案尚未达到该领域的标准

不明白的是，数学家建议证明应该形式化——但 OpenAI 发布的证明中只有 42% 没有经过这个过程。

最终，仍不清楚 OpenAI 在发布其证明时是否根据 AGMAI 原则承担“确保人类理解能够遵循的责任”。 AGMAI 建议 OpenAI 应该帮助资助人类数学家的工作，他们需要使实验室的解决方案真正有意义。

“问题是由人工智能提示者自主解决的，一旦他们的初始目标被‘解决’，他们对更广泛的领域本身不感兴趣，并且对人工智能输出的理解不足以回答有关结果的问题、发表演讲或以其他方式与该领域的其他人互动，”批评 OpenAI 方法的著名数学家陶哲轩在发布后在社交媒体上写道。

剑桥大学和伦敦国王学院的数学家本周发表的一篇论文就说明了这个问题，该论文质疑前沿实验室应对这些挑战的方式。

当人工智能模型解决数学问题时，它们首先创建一种“自然语言”

解释，然后尝试用 Lean 表达结果，Lean 是一种编程语言，理论上可以通过将其编译为代码来确认证明的准确性。

然而，模型将自然语言证明转化为代码的方式可能存在问题；本文记录了 OpenAI 为从描述流体复杂行为的纳维-斯托克斯方程导出的问题提供的解决方案背后的自然语言证明和精益代码之间至少存在两个差异。

这些差异并不一定反驳任何一个解决方案，但它们确实提出了一个问题：我们是否可以简单地依靠模型来形式化自己的解决方案，而无需人工参与。这就是 AGMAI 要求 OpenAI“包含与自然语言和形式工件相关的机器可读元数据”的原因之一，而前沿实验室在这些版本中没有这样做。

“由于误译现象——正如本文所强调的——OpenAI 和

如果没有相同的同行评审流程，其他自动形式化的精益证明从表面上看不应被信任

其他证据也要接受审查”，《迷失翻译》的作者

论文得出结论。

数学家强调，当人类发现新结果时，他们会对此负责，并通过论文、演讲和研讨会与更广泛的社区互动。这个过程增加了对解决方案的理解，找到可用于解决其他问题的策略，并允许新知识应用于实际领域。

哈佛大学数学教授梅兰妮·伍德 (Melanie Wood) 告诉 TechCrunch，当一个模型被提示解决一个难题并给出一个解决方案时，“在发布时人类还无法理解它们，但现在工作就开始了”。