【CNMO 科技消息】10 月 8 日，@danintheory 在 X 上宣布，openai/math 数学成果仓库上线后迎来首次修正：新增 6 项 Lean 形式化，修改 19 项内容，撤回 3 项成果。发帖人是 OpenAI 研究员 Dan Roberts，他表示目前约 42% 的主要成果已完成形式化，团队将持续补充新的形式化内容，并在发现错误时公布勘误。

OpenAI

10 月 7 日，OpenAI 发布一批内部前沿模型产生的新数学成果，共 722 篇手稿，按官方口径归入 372 个成果族，没有提前预告，也未走同行评审流程，一次性全部放入 GitHub。据科学网援引《自然》报道，不少数学家抱怨自己的在研课题被抢先发表，康涅狄格大学数学家 Alvaro Lozano-Robledo 在社交平台上询问，OpenAI 为什么要把数百个数学问题的答案集中对外发布。

OpenAI 与数学界的摩擦已持续两个月。据外媒披露，今年 8 月 OpenAI 曾召集约 40 位数学家闭门开会，学者给出的建议是逐篇按学术规范发表论文，给数学界留出消化和验证的时间。9 月，OpenAI 宣布内部模型给出千禧年难题纳维—斯托克斯方程存在性与光滑性问题的 Lean 验证证明，当时就有数学家质疑 AI 是在参考了研究者未发表的工作后才做出成果。10 月，规模变成了 722 篇。

Lean 是一个机器证明助手，证明写成 Lean 代码并通过编译后，才算机器可验证。Roberts 称约 42% 的主要成果完成形式化，仍有近 58% 的成果停留在人类可读的手稿阶段。本轮同时有 19 项内容被修改，说明已入库的证明代码还在调整，3 项撤回则是大规模发布后 OpenAI 公开撤下的首批成果。

OpenAI 在发布成果时曾表示，发布方式参考了普林斯顿高等研究院数学与人工智能独立咨询小组的建议。