OpenAI 公开内部模型数学成果与 Lean 证明

先了解这件事

OpenAI 于 10 月 7 日在 GitHub 发布 openai/math 仓库，公开由未发布的内部前沿模型产出的数学成果：722 份手稿，归为 372 个结果族，涵盖数论、代数几何、偏微分方程等方向。OpenAI 称许多证明已用 Lean 形式化以便计算机验证，并附论文修订与引用协议；发布前咨询了普林斯顿高等研究院的数学与人工智能独立咨询组，并按其建议和公开推荐决定发布方式。

据 The Verge 和 IT之家报道，独立咨询组织 AGMAI 称这批成果包含对数百个长期公开数学问题的解答。OpenAI 称绝大多数结果由同一流程、用未发布内部模型完成，平均每个结果约相当于 3 小时 ChatGPT Pro 思考算力，评估期间模型共被提出约 4,000 个问题。例外包括黎曼 zeta 函数零点自由区域和 CM 阿贝尔簇上 Hodge 猜想证明的相关工作，其中 Re(s) > 11/12 零点自由区域的文稿经人工编辑以提升可读性。

Rohan Paul 提到，部分结果尚无 Lean 形式化，可能存在问题，仓库将持续更新；其称矩阵乘法证明把两个 n×n 矩阵乘法的已证明成本从 AlphaEvolve 今年 8 月创下的约 n^2.371177 降至约 n^2.25，但这属理论界，尚未提供可用于真实 GPU 负载的更快例程。The Verge 后续报道称，数学家消化这批结果可能需要数年，且 OpenAI 称 719 份手稿中仅约 300 项顶层结果（约 42%）已在 Lean 中形式化，OpenAI 未披露所用模型、提示词及模型尝试的完整问题集。此前 9 月 29 日，agmai.org 发布《Responsible Release of AI-Generated Mathematics》，针对 AI 实验室发布数学成果提出建议，并明确反对在闭源模型上测试高难度数学问题。