拆开 openai/math 仓库：722 份手稿与 42% 的 Lean 证明意味着什么
10 月 6 日 OpenAI 在 openai/math 仓库（Apache-2.0 协议）公开了内部前沿模型产出的数学成果：722 份手稿，归为 372 组相关结果，附 Lean 形式化证明、十份模型推理摘要、算力估计与尝试问题统计。这不是第一次被报道的事件，但这次值得从工程角度拆一遍——因为仓库里的数字，定义了「AI 数学研究」接下来的生产流水线。 42% 的 Lean 覆盖率 截至 10 月 7 日的社区统计，719 份头条结果里约有 300 份附了 Lean 证明，覆盖率约 42%。这个数字比「AI 解决了千禧年难题」更有信息量。它说明：模型生成一篇可读的数学论文，与把每一步推理翻译成机器可检查的 Lean 代码，中间还差着一倍以上的工作量。 Lean 是一种定理证明编程语言，数学结论必须被编译器逐步验证才算数。OpenAI 同步咨询了普林斯顿高等研究院（IAS）的数学与 AI 独立顾问小组，制定修订与引用协议。换句话说，未来的 AI 数学产出会是「双轨」：手稿供人读，Lean 证明供机器审。 算力账单：每份结果约三小时 ChatGPT Pro OpenAI 披露，模型平均每份结果消耗的算力约相当于三小时 ChatGPT Pro 的思考时间；测试中一共尝试了约 4000 个研究问题。这个投入产出比意味着：数学 AI 不是凭空顿悟，而是在巨大搜索空间里暴力枚举、再用形式化工具筛出幸存者。对工程团队，这提示一条新范式——把「可验证」直接写进奖励函数，让模型自己学会先证给机器看。 不完美的一面 需要保留的怀疑是：即便 Lean 编译器通过，数学家仍要读懂证明本身。已有报道提到，部分声称解决 Unique Games 猜想的证明手稿写得极差，连专家都读不下去；OpenAI 自己也警告部分结果可能含错误。机器可检查 ≠ 人类可理解，这中间是数学界未来几年要补的课。 判断 openai/math 仓库的真正历史意义，是把 AI 推理从「分数竞赛」推进到「证据生产」。对做形式化验证、定理证明工具链的团队，这是今年最值得逐文件读的开源数据集。 去论坛讨论 这篇文章里的观点，欢迎到硅基AGI论坛讨论。按标题搜索：openai/math Lean ...