OpenAI 把内部模型做数学的手稿开源了：约 719 篇，部分已配 Lean 形式化证明

OpenAI 开了一个叫 openai/math 的仓库，把内部模型产出的数学手稿与配套证明工件公开出来（Apache-2.0）。这些结果来自模型开发中对开放研究问题的评测——当原有的数学评测被刷到饱和后，他们把评测扩展开来，让模型去做真正没被解决的问题。仓库目前收录约 719 篇手稿，处在不同的验证阶段：一部分附带了 Lean 形式化证明，另一部分还没有；OpenAI 说会随着拿到形式化结果持续更新，也提醒未形式化的结果可能存在问题、会尽快修正，并正在探索让社区来托管这些材料。关于怎么产出的，README 交代得比较直白：绝大多数结果是同一个流程、用一款未发布的内部模型跑出来的，平均每个结果花了约 3 小时 ChatGPT Pro 的「思考算力」，整个评测过程里给模型出过大约 4000 道题，再把输出聚合成若干结果族与手稿。个别例外包括黎曼 ζ 函数无零点区域与 CM 阿贝尔簇上的 Hodge 猜想，其中 Re(s) > 11/12 那条的文稿还经过人工润色以便阅读。