OpenAI 更新数学仓库，新增形式化并撤回部分论文

OpenAI 已更新其在 GitHub 上的公共数学仓库，引入了六项新的 Lean 形式化内容和 19 项修改，同时撤回了三篇特定的数学手稿。据 OpenAI 科学家 Dan Roberts 称，该仓库目前约有 42% 的顶级结果已形式化。

撤回的数学手稿

OpenAI 已正式从仓库中撤回三篇手稿。撤回的作品聚焦于复杂的代数几何和 Hodge 理论：

公司表示，随着新形式化完成和勘误的识别，仓库将继续更新。

仓库中的结果主要使用未发布的内部 OpenAI 模型生成。该过程涉及向模型提出约 4,000 个问题，每个结果平均需要三小时的“ChatGPT Pro 思考计算”。

OpenAI 已发布这 4,000 个问题中约 700 个问题的结果。该项目的目标是使用 Lean（一个定理证明器和编程语言，旨在验证数学证明的正确性）逐步实现数学结果的完全形式化。

此次更新引发了技术和数学社区关于 AI 生成证明与传统同行评审交叉的广泛讨论。

观察者指出，OpenAI 正在将数学证明视为软件发布，利用 GitHub 进行版本控制和迭代更新。

“这就是软件工程实践遇上数学时的样子。‘openai/math 发布 1.3.42：撤回论文 139 和 140，修复论文 47 中的符号错误，恢复先前撤回的论文 85，重构论文 101 中的论证’。”

关于撤回的论文在初次发布前是否经过 Lean 检查，存在持续争论。由于 Lean 是一种形式化验证工具，通过 Lean 检查器的证明在形式化层面数学上保证正确。撤回和“符号错误”的存在表明，要么初始结果未在 Lean 中完全形式化，要么形式化未能准确反映预期的数学问题。

一些批评者认为，大量 AI 生成的数学声明可能在研究社区中产生“干扰”效应，浪费数学家的时间，因为专家们试图验证可能包含根本错误的“垃圾内容”。

“大规模认知卸载，且根据进展程度，可能在数学家时间和注意力方面深度净负。”

相反，一些用户称赞公开记录撤回的透明度，指出这种开放性在传统学术出版中很少见，并为 AI 生成的研究提供了更好的审计追踪。