OpenAI开源math仓库：722篇AI数学手稿，平均3小时算力一篇

10月6日，OpenAI 在 GitHub 上线了一个名为 openai/math 的仓库。没有发布会，没有博客长文，仓库描述一栏甚至空着，但两天之内星标数就冲到九千以上。原因很简单：里面躺着 722 篇数学手稿，全部由一个尚未对外发布的内部模型产出，从命题到成稿几乎没有人类执笔。

按官方说明，这批手稿被整理成 372 个结果家族，家族之下再分主结果、配套论证、推论和备选证明，覆盖数论、分析、概率、数学物理等多个方向。产出流程相当标准化：同一套流程把大约四千个开放数学问题抛给模型，平均每个结果消耗约三小时的 ChatGPT Pro 思考算力，再把有效输出聚合成家族、按重要性筛选成稿。π 的无理性指数、对称与非对称 Mahler 猜想、量子 Heisenberg 铁磁体的自发磁化，这些听名字就头疼的题目都在清单里。官方还挑出十个家族发布了节选版的推理摘要，比如乘性函数的二点相关性、等差数列的拟多项式界、自旋玻璃的 Mézard–Parisi 公式，想围观模型"怎么想"的可以直接翻这几份 PDF。清单里另有两项被特别标注的例外成果：黎曼 ζ 函数零点自由区域的新结果，以及 CM 阿贝尔簇上 Hodge 猜想的证明——这两项走了不同的产出流程，后者的人写部分还经过人工编辑以保证可读性。

不过仓库页写得也很直白：并非所有结果都配了 Lean 形式化证明，未形式化的部分可能存在问题，官方会随形式化进度持续更新，目前也在探索把部分材料迁往社区托管的仓库。换句话说，这是一个"验证程度分层"的数学预印本库，机器验证过的和模型自己声称的，被明确分成了两类。

想把这批材料用起来，可以按三步走：

1. 先读根目录的 overview.pdf，了解 372 个家族按学科如何分类，挑自己看得懂的方向入门；
2. 打开 CONTENTS.md 手稿地图，按编号定位具体论文，preprints/ 目录里有每篇的 PDF、源文件和编译说明；
3. 最关键的一步：进 lean/formalization.yaml 查这项结果有没有对应的 Lean 机器验证，有的才算"硬结果"，引用时直接用论文目录里附的 BibTeX 块。仓库承诺保留公开发布史，修订版上线后旧版仍可访问，引用记得核对版本。

我的看法：这件事的看点不在"AI 写论文"，而在 OpenAI 把验证体系一起交了出来。Lean 形式化在这里不是装饰，而是护栏——机器能逐条检查的证明，和模型自称正确的证明，被放在不同可信层级上公开。这种做法对所有用 AI 干活的人都有参考价值：产出可以交给模型，验收标准必须自己立。做内容的站长体会最深，让 AI 写稿不难，难的是配一条能查出事实错误和编造引用的校验管线；直接引用而不查验证状态，是这个仓库最容易被踩的坑。

对数学圈来说，这更像一次研究范式的压力测试。预印本模式被 AI 加速到一次就能放出七百多篇的规模，同行评审怎么跟上、引用体系怎么标注"AI 参与度"，接下来几年都会有好戏看。更现实的忧虑是质量分层：官方自己都承认部分未形式化的结果可能有错，那这批材料对外行人的价值就高度依赖那份形式化目录的维护质量。仓库地址在 GitHub 的 openai/math，从 overview.pdf 入门最省力，不必一开始就扎进 Lean 代码。