agent 产出的东西谁来验收，是我搭工作流最头疼的一环。OpenAI 昨天端出 722 篇模型写的数学论文，附一整套验收方案。
本周 Top5：Agent-Reach（+6,454）、OpenShell（+5,228）、hyperframes（+3,614）、openrig（+3,327）、openGym（+3,318）。
本期主角不在上面这张表里，它太新了，周增统计还没算到它。openai/math 创建于 10 月 6 日深夜，到本文写作时不到一天，3,615 星、320 fork，Apache-2.0 协议。仓库里是 722 篇数学手稿，出自 OpenAI 一个还没有名字、没有 API、没有定价的内部模型，按 372 个结果家族组织，横跨 17 个数学分支。其中 162 篇的主结果有 Lean 形式化证明，机器能逐行核验，剩下 560 篇只有论文本身，README 原话说部分未形式化的结果可能有问题。这篇讲三件事，这条数学产线怎么跑，机器验收到底验了什么，数学社区为什么盯得这么紧。
图 openai.com 公告页官方横幅
它是什么
打开仓库先看到的是一批研究档案。preprints/ 目录下每篇论文一个文件夹，装着 PDF、LaTeX 源码和引用用的 BibTeX，论文落款日期从 9 月 10 日排到 10 月 5 日，第二天整包发布。lean/ 目录是一个 Lean 4.34.1 形式化库，另附 10 篇推理摘要 PDF，节选模型解特定题目时的思考过程，合计约两百页。整库 5.8 万个文件。
产线流程 README 写得很直白。先给模型出了约 4,000 道开放研究题，理由是原有数学评测已经考不出差距；平均每道题花约 3 小时 ChatGPT Pro 档位的思考算力；产出按显著性筛选后聚成家族，一个家族收主结果、伴生论证、推论和另证。4,000 道题出 722 篇论文，这个比例别读成解题率，筛选标准没有公开，OpenAI 自己也承认哪些结果够格是它自己判的。固定流程之外有两个例外，zeta 函数零点自由区域的工作和 CM 阿贝尔簇上的 Hodge 猜想证明；zeta 那篇 Re(s)>11/12 区域的行文还经过人工润色。
为什么有意思
机器验收只覆盖一小半，但验收方式是新的
162 篇有 Lean 形式化的论文是这批材料里唯一的硬通货。Lean 是证明助手语言，证明写成代码后由内核逐行检查，通过与否机器说了算。OpenAI 配的核验工具叫 Comparator，配置里只放行 propext、Quot.sound、Classical.choice 三个标准公理，证明不许引别的。外部评测 kingy.ai 逐条看过配置后提醒了一个关键区分，Lean 核的是形式化陈述，形式化陈述跟论文里那句话是不是一回事，仍然要人对照。好在这两者都被摊开了，每篇论文的 PDF 和对应 Lean 文件并排放着，引用条目和版本修订全部留档，改过的旧版本不删。
跑一遍验证本身是个工程活
lean/README 特意提醒，整库编译会撞上 Linux 的 vm.max_map_count 上限，建议只编小局部；要全量编译得用 -DMMAP=OFF 重编 Lean，再加一组 glibc 环境变量。换句话说，想亲手核验这批证明，先得过一道系统调优的门槛。这个细节比任何宣传语都诚实，形式化验证到今天仍然是有成本的活。
治理是这次发布的另一半
8 月 1 日 OpenAI 发过一批十大数学进展，当时数学圈火气不小，有数学家指出模型的关键论证与他 2016 年的论文撞车而发布稿没有标出处，科学美国人把研究不端写进了标题。9 月 29 日，设在高等研究院的数学与人工智能顾问组发布行为准则，要求实验室别拿数学发布当模型营销，别在专有模型上刷开放难题，发布后要出钱资助人类数学家去理解这些结果。这次 722 篇的发布被普遍读作对那份准则的照做，问题数、算力开销、推理摘要、版本制度都按建议给了，还承诺出钱办研讨班。两条没做到，产生结果的模型没放出，仓库还挂在 OpenAI 自己账下而准则希望社区托管，OpenAI 说还在找。另外这个仓库的 issue 区是关闭的，外人发现证明有问题，没有公开入口提交。
边界与局限
这批材料的可信度分三层看。最硬一层是 162 篇 Lean 主结果，机器核过，但陈述与论文的对应关系还等着人工抽查。次一层是其余 560 篇纯论文，README 明说可能有错。推理摘要只覆盖 10 个家族，372 分之 3 都不到，想看模型怎么想的，基本只能从证明文本反推。
头条级结论全部未经同行评审。π 的无理数指数恰为 2、自由群因子全部同构、有理数上的希尔伯特第十问题无解，这几个大结论都还没有 Lean 形式化。有个所有狄利克雷 L 函数在 Re(s)>7/8 无零点的结果倒是形式化了，外部给它起名叫准黎曼猜想，但它离真正的黎曼猜想还差半个平面，别读成黎曼猜想被证明。想自己跑验证的除了 mmap 那道坎，还要有版本意识，OpenAI 说在找社区托管方，这个仓库地址将来可能变。
对谁有价值
数学和理论计算机方向的研究者现在就值得深读，从 10 篇推理摘要和 162 个 Lean 文件下手，那是全部材料里能独立核验的部分。做 AI 基础设施的人可以把这份发布当验收流程的参考设计读，问题集、显著性筛选、形式化、版本制度、外部顾问，链条齐全，直接能抄。写论文想引用结论的人，只认有形式化的那 162 篇，其余当普通预印本对待。等模型放出再玩的人可以再等等，OpenAI 说了会负责任地放，没给时间表。
我的用法很明确，引用只认有 Lean 形式化的那 162 篇，其余 560 篇当预读材料。AI 产出怎么验收，这个仓库是目前最完整的一份公开答卷。
数据截至 2026-10-07，来源 GitHub API（openai/math 元数据、formalization.yaml 逐条计数、lean/README 与 lean-toolchain）、openai.com 公告页、外部评测（CellCog 2026-10-06、kingy.ai 2026-10-06、theclarity.today 2026-10-06、orcarouter 2026-10-07、Scientific American 2026-08-06）
GitHub 仓库 https://github.com/openai/math
