10 月 6 日，OpenAI 将 719 篇由未公开内部模型生成的数学论文推送至 GitHub。此次发布发生在一周之前其顾问机构呼吁各 AI 实验室停止在专有模型上测试高难度数学问题之后。相隔一周的这一时间线，凸显了当前 AI 驱动的数学研究中存在的紧张关系：实验室利用公开问题来衡量模型进展，而数学界的部分人士则呼吁在 AI 生成的成果流传之前进行披露并经过常规同行评审。

超过 600 份问卷回应塑造了 IAS 小组 9 月 29 日的指导意见

设在新泽西州普林斯顿高等研究院的数学与人工智能咨询小组于 9 月 29 日发布了其建议，该建议基于超过 600 份问卷回应。"我们希望从一开始就明确表态：我们不认可这种做法，我们要求他们停止在专有模型上测试高难度数学问题，"该小组在其指导意见中写道。

同一份文件警告称，私下持有的内部模型有可能造成一个两级体系，使少数实验室超越该领域的其他所有人。

根据其代码库的说明，OpenAI 在模型开发过程中会在公开研究问题上测试其模型，并在其现有数学基准趋于饱和——即模型在现有测试中得分达到或接近最高水平的节点——之后扩展了这些测试。该公司表示，它已与咨询小组进行过商议，并在此次发布中参考了其建议。在 10 月 6 日发布的一份声明中，该小组表示，其顾问角色并不构成"对 OpenAI 获取这些结果之过程的认可"，并将合规判定权留给更广泛的数学界。

Navier-Stokes 的 Lean 代码所证明的结论弱于书面论文

OpenAI 将这 719 篇论文划分为 372 个数学家族，每个家族围绕一项主要结果及其相关证明构建。该专有模型被给予了约 4,000 个问题，每项结果平均需要约三个小时的 ChatGPT Pro 思考算力。

咨询小组已要求各 AI 实验室针对每项结果公布：模型名称、所使用的提示词、思维链摘要、所用时间以及计算成本。OpenAI 发布了 10 份推理摘要，其约 42% 的核心结果附带 Lean 形式化。此次发布在多大程度上符合这一针对每项结果的清单，是该小组留给数学界裁定的问题之一。

Lean 是一种可用于让计算机检查证明的编程语言。如果代码通过编译，并不意味着代码与书面论证完全一致；它只能确立该形式化命题为真。以这种方式将书面论证转换为机器可检验的代码，就是研究人员所称的自动形式化。

Alexander Bastounis、Fabian Circelli 和 Anders C. Hansen 在 10 月 6 日发布的一篇论文中检验了这一差距。他们发现，OpenAI 关于 Navier-Stokes 的书面论文所声称的内容强于其 Lean 代码所证明的范围，其中一处估计改变了输入导数的阶。作者们还在 OpenAI 的 Euler 证明中发现了类似的误译，并写道，OpenAI 的书面证明及其他自动形式化的 Lean 证明"在未经受与其他证明相同的同行评审流程和审查之前，不应被想当然地信任。"

OpenAI 于 9 月 8 日宣布了 Navier-Stokes 结果。该组是克雷数学研究所千年奖问题之一的研究对象，每个千年奖问题均设有 100 万美元奖金。纽约大学数学家 Tristan Buckmaster 随后对该公司在这一工作中所需人类投入极少的描述提出异议，Cryptopolitan 曾对此进行报道。该公司已承诺为与重大 AI 成果相关的研讨会、会议和特别项目提供资金。10 月 6 日，数学家 Terence Tao 写道，向 AI 系统输入提示词的人往往在解决问题后便对该领域失去兴趣，并补充说其中许多人无法就相关成果回答问题或作报告；他的帖子并未点名 OpenAI。

该公司曾表示，其顾问对研究进度没有发言权，Cryptopolitan 在 9 月曾报道。随着合规判定权如今掌握在数学界手中，值得关注的指标包括同行评审会维持还是质疑这些从书面到 Lean 的转换，以及未来的发布是否会逐项列出该小组要求每项结果披露的信息——模型名称、提示词、思维链摘要、用时和计算成本。