OpenAI 公开 722 篇 AI 生成的数学论文，约 160 篇附 Lean 形式化证明

OpenAI 一次性公开 722 篇 AI 写的数学论文 OpenAI 把一个内部未发布模型做出的数学成果整体公开了：722 篇论文，归成 372 组结果，全部放在 GitHub 仓库 openai/math 里，谁都能看。 这个模型就是上个月宣称解决了纳维-斯托克斯方程问题（千禧年七大数学难题之一）的那个。它从 8 月 28 日开始训练，能力比 OpenAI 已发布的 GPT-6 Astra 更强，目前还没对外开放。 OpenAI 说，原有的数学测试题已经难不住模型了，所以改拿真实的未解数学问题来考它。前后一共给了模型大约 4000 道题，筛掉分量不够的，剩下这 372 组。平均每个结果花的算力，相当于在 ChatGPT Pro 里思考三个小时左右。 论文覆盖数论、代数几何、组合、数学物理等大部分数学分支。标题里能看到不少有名的问题，比如证明 π 的无理性测度（衡量一个数能被分数逼近得多好）等于 2，证明卡塔兰常数是无理数，还有黎曼 ζ 函数零点分布、特殊情形下的霍奇猜想。后两项 OpenAI 特别说明，用的流程和其他结果不同，其中黎曼 ζ 那篇的文字还经过人工润色。 这些结论可信吗？OpenAI 自己的说法是“处在不同验证阶段”。约 160 篇的主要结论附带了 Lean 形式化证明。Lean 是一种能让计算机逐步检查数学证明的编程语言，过得了 Lean，基本可以排除证明里的逻辑漏洞。剩下的论文还没形式化，OpenAI 承认其中可能有错，说会尽快修正，所有修订都保留历史版本。另外还附了 10 份模型推理过程的摘要，让人能看到模型是怎么想出来的。 发布方式本身也是这次的重点。9 月下旬，OpenAI 在普林斯顿高等研究院（爱因斯坦待过的那个研究所）支持成立了独立的“数学与人工智能顾问组”，成员是 Timothy Gowers、Edward Witten、Martin Hairer 等 9 位数学家，不拿 OpenAI 的钱。此前 25 位菲尔兹奖得主联名发公开信，批评 AI 公司抢着宣布破解名题的做法。 顾问组 9 月 29 日发布了一份建议，征集了 600 多位数学家的意见。核心要求有三条：AI 写的证明要按正规论文格式重写，并引用相关的已有文献；成果要放进不受 AI 公司控制、可长期引用的学术存档平台；AI 公司要出钱支持数学界去真正理解这些成果。顾问组还明确表示，不赞成 AI 公司在外界用不到的私有模型上攻数学难题，希望它们停下来。 OpenAI 这次回应了其中一部分：先放 GitHub，同时在找符合顾问组标准的社区托管平台；承诺资助一系列研讨会、学术会议，帮数学界消化这批成果；也表示正在推进“负责任地发布”这个模型。至于停止在私有模型上测试，OpenAI 没有回应。 对数学专业的人来说，接下来最实际的变化是：自己研究方向上的某个猜想，可能已经在这 722 篇论文里了，值得去仓库里翻一翻。 原文：https://openai.com/index/sharing-ai-progress-in-mathematics/ 仓库：https://github.com/openai/math