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