AI 的数学时刻：719 篇机器手稿与「证明」的可信度问题
为什么值得读：这不是又一篇「AI 刷榜」快讯。10 月 6 日 OpenAI 一次性公开了 719 篇由内部未发布模型写出的数学手稿，第一次把一个硬核工程问题摆上台面——当机器产出的证明多到没人读得完，「被验证」到底意味着什么？两篇独立深度解读（一篇拆验证机制，一篇盘点数学界的震荡）把这件事讲透了。 事件时间：2026 年 10 月 6 日发布，10 月 7 日修订，10 月 15 日官方博客追加 500 万美元后续计划；深度解读文章时间为 10 月 8 日与 10 月 9 日。
2026 年 10 月 6 日，OpenAI 在官方博客宣布：把一个内部未发布的前沿模型 在约 4000 道数学问题上的产出，全部放进公开 GitHub 仓库。首日 722 篇手稿，第二天因一处符号错误撤回 3 篇代数几何手稿并修订其余，最终定格为 719 篇手稿、372 个结果族 。按 OpenAI 的口径，其中约 42% 的顶层结果配有 Lean 形式化证明；每出一份结果，平均消耗相当于 ChatGPT Pro 思考约 3 小时的算力；仓库还附带 10 份模型推理过程的摘要。名单里不乏几十年无人攻克的硬骨头：准黎曼猜想的零点自由区、有理数域上的希尔伯特第十问题、CM 阿贝尔簇上的有理霍奇猜想、唯一博弈猜想、矩阵乘法指数的新上界。约一个月前，OpenAI 已经用同一模型公布了 Navier–Stokes 问题的解法预热。这次发布真正值得细读的，不是结论清单——而是它暴露的两个问题：机器证明的可信度到底由什么保证？以及，一个学科被 AI「撞」一下之后会发生什么？
一、发布了什么：从「全认证小批量」到「半认证大批量」
先理清时间线。10 月 6 日上线时仓库有 722 篇手稿；10 月 7 日，OpenAI 发现一处符号错误，撤回 3 篇相互关联的代数几何手稿并修订了其他论文，剩下 719 篇。这个「上线第二天就撤稿」的插曲本身就是看点：仓库带有正式的修订与引用协议，旧版本保留可查——OpenAI 把数学论文当成软件版本在管理。
关于「有多少被机器验证过」，口径需要小心。OpenAI 官方说法是约 42% 的顶层结果有 Lean 形式化证明；但独立复核者的计数并不一致（有人算出 24%，有人算出 36%），因为「顶层结果」本身就没有统一定义。README 倒是写得很坦白：仓库里的结果「处于不同的验证阶段」，未形式化的部分「可能存在问题」。值得注意的是策略的转变：今年早些时候 OpenAI 曾发布过一个小批量版本——十个「十年未解」的问题，每个 都带 Lean 证书。这次则是用「全认证」换「大批量」，而这个取舍，正是整个故事的核心。
还有两个关键事实：模型本身不公开，论文里没有训练配方，也没有点名任何新的推理算法或 agent 框架——OpenAI 披露的「结果」远多于披露的「系统」。这意味着外界无法分离三者的贡献：更好的训练、解题时的算力投入、以及 prompt 与工具编排的基础设施。另外，10 月 15 日官方博客追加了一条更新：OpenAI 向 Simons 基金会捐赠 500 万美元，资助数学家们审查、理解这些 AI 产出的结果，并向受资助的研究者开放模型与算力——算是对「只管生不管养」批评的一种回应。
二、Lean 证明到底「证明」了什么：验证设计的深挖
这是整件事技术上最有营养的部分，来自开发者社区一篇逐行对照仓库 README 的深度拆解。先说背景：Lean 是一个证明助手，证明只有每一步都通过类型检查才能编译。OpenAI 的仓库里藏着一个精巧的验证设计：每道题的 challenge 文件用sorry（Lean 里「此处未证明」的占位符）固定命题陈述，而证明写在别处；配套的检查工具保证每个 sorry 都被覆盖，模型没法悄悄改写它要证明的命题。一位 Hacker News 评论者点破了这个设计的妙处：它堵住了第一种作弊——模型改题。
但它堵不住第二种：证明可以完美对应一个「比真实猜想稍弱」的命题 。Lean 认证的是「证明对形式化命题成立」，而形式化命题是否等同于论文宣称的猜想，仍然是人类的阅读工作。拆解文章举了两个实例：Hadwiger 猜想的手稿里，Lean 只覆盖了普通染色的反例，没覆盖论文中更强的分数染色断言；Erdős 倒数和猜想，Lean 覆盖的是定性命题，而非论文里的定量加强版。换句话说，「带 Lean 证明」不等于「猜想被证明了」，它等于「某个精确表述的命题被机器检查通过了」——而这两个命题之间的缝隙，恰恰是最需要数学家的地方。至于那 58% 未形式化的手稿，则是完全没有任何机器检查的。
给做 agent 工程的人的三条可迁移经验 （原文作者的总结，转述如下）：
- 固定 spec，让 agent 写证明。 把不可变的命题陈述和 agent 生成的解法分开存放。对应到编码 agent：测试套件或契约是 agent 不许碰的；如果 agent 能改它自己的评分标准，那就是自己给自己打分。
- 给每个产出标注验证等级。 README 诚实地写了「结果处于不同验证阶段」。同理，agent 的 PR 也该分级：「测试通过且有人读过 diff」和「只是测试通过」是两种完全不同的断言。当所有产出看起来一样可信时，评审瓶颈只会更糟。
- 为 checker 做预算，而不只是 generator。 每份结果约 3 小时 Pro 级算力只是生成成本；真正的贵的部分，是仓库量级的验证层。Anthropic 做费马大定理 Lean 形式化时遇到的是同一道坎。
一句话：这次发布的真正主角不是定理，而是**「当 agent 的产出多到没人读得完时，信任应该放在哪里」** 的工程答案。
三、数学共同体的震荡：敬畏、失落与规则之争
另一篇独立长文梳理了数学界的反应，读起来像一场小型地震的灾情记录。斯坦福的 Jared Duker Lichtman 称这是「按任何客观标准都绝对历史性的」产出；2022 年菲尔兹奖得主 Hugo Duminil-Copin 写道：「震惊是巨大的，我瘫痪了」——他职业生涯中公开强调过的每个重大开放问题，如今都被宣称解决了；在 Anthropic 做数学家的 Levent Alpöge 称之为「数学史上最重要的时刻」，同时对研究优先权和利益冲突表示担忧。陶哲轩则欢迎其中的新想法，但强调了对研究者的冲击——尤其是研究生和博士后，以及一个更尖锐的问题：这些证明背后没有「人」可以向社区解释和发展它们 。他提出的「Math 2.0」呼吁的是阐释、社区建设和新的研究方向，而不是抢先解题。
Hacker News 上 1400 多条讨论大致分成三派，值得细看：
- 敬畏与失落。 一位断断续续研究 Barnette 猜想 24 年的评论者写道，看到它被列为「已解决」像一场「安静的哀悼」——而那篇论文恰好没有 Lean 证明，他还在逐行读。
- 权力集中。 模型不公开、不可复现，「普通人用不到的技术取得的进步」被指为权力集中问题。普林斯顿高等研究院下设的数学与 AI 咨询组（AGMAI）在 9 月 29 日发布过三条建议：披露模型名称、prompt 与算力成本；不要把数学成果当营销工具；停止在学术界无法访问的私有模型上测试前沿难题 。前两条 OpenAI 照做了一些，第三条显然没被执行。
- 开采还是生长。 有人讽刺这是「开放问题的 strip mining（露天开采）」；反驳者认为解完的问题依然给人类留下工作——阐释、替代证明、新方向；再反驳者指出，消失的恰恰是做这些工作的职业激励。
还有一个容易被忽略的细节：有评论者指出，这些模型写的形式化证明没问题，但英文阐释写得不好——Unique Games 那篇论文的开头 dense 到难读。形式化证明让这点变得可以忍受；但对未形式化的多数结果，可读性直接决定了社区能以多快的速度检查它们。
也有积极的独立验证信号：一位读者用两套不同的 Lean 内核独立复检了准黎曼猜想（结果族 003）的形式化证明，双双通过。这说明验证层本身是可用的——问题从来不在工具，而在覆盖率。
四、为什么这件事值得技术人认真读一遍
把视线从数学移开一格：数学只是第一个被「产出淹没」的领域。当编码 agent 一天能提上千个 PR、当法律文档和财报分析也能被批量生成时，每个领域都会撞上同一堵墙——生成成本趋零之后，验证成本决定一切 。OpenAI 这次无意中给全行业做了一次公开实验：719 篇手稿、部分机器验证、版本化管理、社区复检，恰好是一套「超大规模 agent 产出治理」的雏形。
短期看，最大的变量是那个「负责任地发布」的模型。OpenAI 说正在推进，Simons 的 500 万美元和算力开放是第一步。如果模型最终开放，社区就能复现「解题过程」而不仅是检查「解题结果」，那才是真正的 Math 2.0。但即使不开放，这次发布已经立了一个标杆：以后任何实验室宣称「AI 解决了 X」，第一个问题都应该是——你的验证分级是什么？spec 被固定了吗？形式化命题和自然语言断言之间的缝隙由谁来填？
对个人而言，结论也很实在：别再只问「AI 能做什么」，开始问「我凭什么相信它做对了」。这套验证思维——固定不可变的验收标准、给产出分级、为检查者留预算——在你下一个 agent 工作流里就能用上。数学界用 719 篇手稿交的学费，不必每个人都重交一遍。
原文链接
1. 深度拆解（验证机制篇）：OpenAI Math Repo: What the Lean Proofs Do and Don’t Verify — Developer Digest，2026-10-08
2. 深度分析（数学界反响篇）：Another Turning Point for Mathematics? — A Silicon Valley Insider，2026-10-09
3. 事件源头：Sharing AI progress in mathematics — OpenAI 官方博客，2026-10-06（10-15 更新 Simons 基金会 500 万美元计划）
本文为中文深度解读，以上观点经转述与交叉核实；关键数字（719 篇 / 372 结果族 / 约 42% Lean 形式化 / 约 4000 题 / 每结果约 3 小时 Pro 级算力）来自 OpenAI 官方博客与仓库 README，多家独立报道口径一致，个别计数（如形式化比例）存在统计口径差异。