技术拆解 019｜openai/math：OpenAI 一次性开源 722 份 AI 数学手稿的仓库拆解

10 月 6 日，OpenAI 在 GitHub 公开仓库 openai/math，把一个未发布内部模型产出的数学研究成果一次性放出：722 份手稿、372 个结果族，3.1 GB、132,880 个文件，两天 9832 星（仍在涨），HN 相关讨论超 1200 赞、1400 余条评论，官方博客《Sharing AI progress in mathematics》同日配发。它不是一份论文合集，而是「手稿+形式化+验证工具」三件套，这个仓库的读法、验法和争议，几乎都长在这三层结构上。这篇按六件事拆：是什么、为什么值得看、结构与机制、数字与边界、怎么验证、价值判断。

一、它是什么

openai/math 是一个 AI 数学产出仓：主语言 Lean，Apache-2.0 协议，三层内容加一份手稿地图。

第一层 preprints/，722 个目录，一个目录一份研究手稿，内含 paper.pdf、LaTeX 源文件、引用与构建说明。目录名带落款日期：最早 9 月 10 日——正是纳维-斯托克斯结果对外宣称的那天——最晚 10 月 5 日，公开则在 10 月 6 日。手稿攒了近一个月才一次性放出，首个提交的时间戳就落在公开当天。

第二层 lean/，形式化库。OAI/ 下按学科分 24 个子目录，从 Algebra 到 Topology，12.17 万个 .lean 文件；依赖 mathlib4 并锁定到具体提交 d13f23b，patches/ 里存着对上游的补丁——这套库不是只消费 mathlib4，动了上游。

第三层 reasoning_traces/，10 个结果族的推理摘要 PDF。README 自称是 abridged summaries，HN 有评论指出更准确的说法是「摘要的节选」——不是原始推理轨迹。

顶层导航两份：CONTENTS.md，640 KB 的手稿地图，722 份逐一登记，每份给出题目与结论指向，下文引用的 001、003、102、180 就是这份地图里的条目号；overview.pdf 带源文件，323 KB，是全部结果的导览。仓库按「族」组织，一个主结果加伴随论证、推论、替代证明算一族，722 份手稿归入 372 个族——相当一部分结果带着替代证明或伴随论证一起放出来，读的时候按族读，比按篇读划算。

二、为什么现在值得看

第一个理由是结果清单本身的分量。722 份不是 722 道孤立题目，按族组织的它更像一份研究档案；CONTENTS.md 里除重磅条目外，还散落着 π 的无理性指数、Erdős 型算术级数拟多项式界、Kaplansky 直有限性特征 2 反例、自由群因子同构、相对论 Vlasov–Maxwell、Mahler 猜想、量子 Heisenberg 铁磁体自发磁化——从数论、图论一路铺到数学物理。重磅的挑四件说。

003 号，准黎曼假设：ζ 函数与全部 Dirichlet L 函数在 Re(s)>7/8 区域无零点，附 Landau–Siegel 零点的一致排除。方向必须先讲清：零点自由区越靠右越强，人类纪录是 11/12≈0.9167，7/8=0.875 在它左侧——这是该系统在老问题上独立推进出的下界，不是破纪录。

102 号，Unique Games 猜想（Khot，2002），手稿给出成立的证明。理论计算机科学的基础设施级命题，一大批不可近似性结果以它为前提，HN 有评论认为其分量比某些千禧年问题更重。

180 号，Barnette 猜想（1969）：每个有限简单三次二部平面三连通图都有哈密顿圈。图论挂了 57 年的悬案，有 HN 用户自述曾用当期最强模型攻此题数月未果。

001 号，Milne 有理性猜想（阿贝尔簇），同条目并列 Hodge 猜想 CM 阿贝尔簇特殊情形的证明宣称——口径要咬住：只是特殊情形的宣称，克雷研究所的认证没有发生。

第二个理由是发布形态。此前 AI 数学的公开多是单点宣称，一次性放出 722 份、自带形式化层与验证工具的整仓，这个形态本身罕见。HN 讨论里已经出现新玩法：有人把整个仓库丢给自己的 agent，让它逐条回答每份手稿的 significance——722 份的量级，逼出了新的阅读方式。

三、核心技术机制

产出管道是 README 自述的：绝大多数结果由同一个未发布的内部模型按固定流程产出；全程约 4000 道题被投喂，平均每个结果耗 3 小时 ChatGPT Pro 等效的思考算力；产出聚合成族、过显著性门槛后留下 722 份。两项列为固定流程之外的例外：黎曼 zeta 零点自由区与 CM 阿贝尔簇 Hodge 情形，差异 README 没展开，只说明零点自由区那份论文经过人工编辑润色可读性。

形式化层的组织值得细看。lean/docs/ 下每个形式化结果一页文档，写清适用范围、对照论文与 Comparator 链接。仍以 003 号为例：陈述覆盖 ζ 函数、全部 Dirichlet L 函数与 Q(√-3) 上有限阶 Hecke L 函数；主特征在 s=1 的极点明确排除在陈述之外；常数未给显式值。形式化了什么、没形式化什么，文档划得清清楚楚——读这个仓库，先读 docs 再读代码，这一页页说明就是最省力的入口。

推理摘要这一层要单独泼冷水。10 个族配有 reasoning_traces，README 的措辞是 abridged summaries，HN 讨论指出这实际是「摘要的节选」。对照「平均每结果 3 小时」的思考量，社区拿到手的推理材料远不足以复现模型的推理路径——对想研究「模型怎么想」的人，这是仓库最不透明的一层。

验证分层是机制里最要紧的一环。formalization.yaml 清点出 162 篇有主结果形式化的论文，占 722 的两成出头；README 原话是结果处于不同验证阶段、并非全部配有 Lean 形式化，并自认未形式化部分可能有错。换句话说，仓库自己把可信度标成了梯度：162 篇机器可检，其余 560 份是人类可读的宣称。

四、数字与边界

数字摆全：722 份手稿、372 族、162 篇形式化、132,880 个文件、3.1 GB、约 4000 题投喂、平均每结果 3 小时、两天 9832 星；Lean 库 24 个学科子目录、12.17 万个 .lean 文件。

边界说四条。

其一，方向别读反。7/8 弱于 11/12，AI 的零点自由区结果不是超越人类；写成破纪录是这个题材最常见的错误，方向写错，整篇的信誉就搭进去了。

其二，形式化不等于免错。Lean 验证的前提是定理陈述被正确翻译——机器检查的是代码里的那条陈述，不是论文里那句中文或英文结论。HN 的高赞质疑正落在这里：横跨 24 个学科，每条陈述的翻译都值得人工过目，003 号文档里常数不给显式值，就是这类检查要抠的细节；有人直接预测会翻车，回应方则指出 README 已自认未形式化部分可能有错。

其三，发布不等于认证。博客标题用的是 sharing 不是 solving，克雷认证与同行评议均未发生，论文署名 OpenAI、无人类审校署名。HN 的 GitHub 与 arXiv 之争也由此而起：有人赞 GitHub 发布打破付费墙，数学家反驳数学成果本就走 arXiv，仓库的存档价值与论文存档并不同构。

其四，算力口径要看幕后，星数口径要看对象。3 小时是均值口径，HN 有人翻出 AlphaZero 的旧账——「4 小时超人」实为 4 小时乘 5000 块 TPU——提醒「3 小时 ChatGPT Pro 等效」这类表述要问一句幕后总量；而两天 9832 星量出的是关注度，不是正确性——仓库自己都把 722 份标成了验证梯度，社区复检才刚刚开始。

五、怎么跑、谁能玩

不跑模型也能验证，这是仓库设计上最实在的部分。lean/README 给出 Comparator 流程：先装 comparator、landrun、lean4export 三件，lake update 拉起依赖，lake exe cache get 取 mathlib4 缓存，然后执行 lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json——对 003 号的形式化陈述跑对照检查。ComparatorChallenges/ 里是官方预置的挑战清单，照这套流程可以逐项抽查。要编译全库，README 专门警告 Linux 默认的 vm.max_map_count 上限可能不够，给了 CMake -DMMAP=OFF 加 GLIBC_TUNABLES 的绕法——一个仓库大到官方要专门写编译避坑说明，恰恰是体量的注脚。

分三类人说。做 Lean 与形式化数学的人：162 篇带对照论文与文档的形式化结果，加上 mathlib4 的锁定与补丁，是能直接上手读、直接上手验的资产，也是观察「AI 产出如何落进 Lean」的现成样本。做理论计算机的人：Unique Games 那份手稿无论最终成立与否，都值得逐行读——它牵动的不可近似性版图太大，验证结论的每一步都会被学界反复引用。做模型评测的人：4000 题投喂、族聚合、显著性门槛这一整套筛选流水线，连同每结果 3 小时的成本口径，是一份稀缺的一手方法论素材。

只想围观的人，门槛是磁盘和耐心：3.1 GB 的 clone，加一次不一定吃得下的全库编译；不想装任何东西的，先读顶层那份 323 KB 的 overview.pdf，二十分钟对全仓结果有个地图感，再决定往哪个学科目录走。

六、价值判断与适合谁

样本价值高。它把「AI 做数学」从新闻稿里的单点宣称，变成一个可清点、可抽查、可机器复检的公开仓库。162 这个数字尤其要紧：哪怕其余全部存疑，这 162 篇的形式化陈述都是社区能够独立验证的硬内容。菲尔兹奖得主陶哲轩在 Mastodon 的表态（HN 转引）也落在同一方向：希望 AI 能向人类数学家解释自己的结果，并认为 AI 在阐述与社区建设上能有正贡献。

生产力价值分人。对数学与理论计算机研究者，这是必须知道的存在，哪怕只为判断自己的课题有没有被撞——HN 上已有博士生产生「论文写一半被 722 篇砸中」的焦虑，共情回复给的建议是拥抱前沿、别把未发表的研究原文粘给 AI。这个情绪本身也是行业变量。对工程侧，验证工具链与编译避坑文档是大型 Lean 工程的现成参考。对只想要结论的人，提醒一句：这里没有结论，只有不同验证阶段的宣称。

博客另承诺资助系列研讨会、会议与专门项目，帮助数学界理解 AI 产出的重大结果，并称在推进负责任地放出产出这些结果的模型；README 也提到在探索社区托管的仓库。结尾补一句前情：8 月的十题 Lean、9 月的菲尔兹奖得主声明与顾问组建议书，构成这次发布方式的外部背景，批评面的展开在同日热点篇，这里不赘。

一句话判断：openai/math 的历史位置不取决于 722 份里最终站住几份，而取决于它第一次把 AI 数学的产出放进了人类数学可以逐条检查的轨道——星数是 OpenAI 的，逐条检查的权利是社区的。

参考来源

• 仓库本体：github.com/openai/math（本地 clone 后逐项比对 README、CONTENTS.md、lean/ 目录、formalization.yaml、git log；未执行任何构建）
• OpenAI 博客《Sharing AI progress in mathematics》（2026-10-06）
• HN story 49984923（截至 2026-10-08 超 1200 赞、1400 余条评论；陶哲轩表态与顾问组建议书均为 HN 转引，未逐字核对原文）
• 星数 9832★ 为 2026-10-08 时点数据，仍在上涨