OpenAI 公布 722 份数学手稿：AI 的下一道门槛，是可验证的证据

AI Math Needs Verifiable Proofs：英文发布海报

北京时间 10 月 7 日凌晨，OpenAI 的数学成果集合进入公开视野。GitHub 仓库的初始提交记录是 UTC 10 月 6 日 21:58:50，也就是北京时间 7 日 05:58:50。本文讨论的是这次公开材料，而不是把其中此前形成的研究结果全部算成“今天完成”。初始提交记录

最醒目的数字是 722 份手稿、372 个成果家族。但如果把新闻压缩成“AI 一口气攻克了数百道难题”，恰好会漏掉最重要的变化：外界现在可以查看论文、证明材料、形式化目录和部分推理摘要，不必只围着公司的结论讨论。OpenAI 仓库说明

我的判断是，这次发布的技术价值，不应主要由手稿数量决定，而应由它能否建立一条可复核的证据链决定。对于开发者，这比又一张模型排行榜更值得关注：当生成越来越容易，验证会成为产品设计的一部分，而不只是交付前的最后一道手续。

先把三个数字拆开

根据仓库 README，722 是手稿数量，372 是相关成果的分组数量。一个家族可以包含主要结果、配套论证、推论或者替代证明。因此，手稿与独立突破不是一一对应关系，成果家族也不能直接当作统一难度的测试题。目录与产生流程

同一份说明称，内部未发布模型在评估过程中被提出约 4,000 个问题；绝大多数成果采用相同流程产生，平均每项成果使用的计算量相当于该模型三小时的 ChatGPT Pro thinking compute。这是厂商提供的计算资源描述，不是普通用户可以购买的标准任务报价，也不是“每个问题三小时就能解决”的承诺。

更不能用 372 除以 4,000，宣布得到了模型的科研成功率。分子是聚合并经过重要性筛选后的成果家族，分母是尝试的问题，两者单位不同；一些结果还建立在模型此前的结果之上。缺少逐题对应关系、失败定义和统一验收标准，这个除法只有数字，没有稳定含义。

README 还列出固定流程的例外，包括黎曼 zeta 函数无零点区域，以及 CM 阿贝尔簇的霍奇猜想相关工作；其中 Re(s) > 11/12 无零点区域的写作经过人工可读性编辑。这里必须保留对象和条件，不能把受限命题替换成更广泛的著名猜想，也不能把人工参与藏起来。原始披露

这些限定不是对成果的否定，而是让后续评价有共同的计量单位。技术团队评估代码助手时，也不应把生成的文件数、通过测试的函数数和交付的业务需求数混在一起。

Lean 检查的是证明，不是新闻标题

这次发布值得认真对待的部分，是一些自然语言手稿配有 Lean 形式化材料，以及关联论文与形式化结果的目录。但官方也明确表示，集合中的成果处于不同验证阶段，并非所有手稿都已形式化，部分未形式化结果可能存在问题。Lean 目录；形式化清单

这意味着，“公开了 Lean 文件”“在特定环境中成功检查了某项形式化证明”“形式化命题准确对应论文主张”“专家认可其新颖性与意义”，是四件不同的事。

可以用一个假设例子理解：你希望证明某算法适用于所有合法输入，但形式化时增加了一个更强的输入限制。证明检查器即使接受了证明，也只说明形式系统中那个带限制的命题成立，不能自动替你删掉限制。问题不一定出在推理步骤，而可能出在最初写下的规格。

From Output to Evidence：模型输出、形式化命题、证明检查与专家审查的概念流程

*概念图：证明检查针对被明确指定的逻辑命题；命题是否对应原问题、结果是否新颖以及适用范围如何，仍需另行审查。图中不是实验数据，也不是官方验证状态图。*

因此，形式化材料带来的进步，是把一部分争论从“这段文字看起来对不对”转向可明确检查的对象。它并没有取消专家工作，而是改变了专家最该花时间的地方：定义、假设、依赖关系、命题对应和数学意义。

真正的独立回应，没有替全部结果背书

独立的数学与人工智能顾问组 AGMAI 在 10 月 6 日的回应中，称此次发布是重要事件，同时明确表示：它的顾问角色不应被理解为对成果影响的判断，也不是对 OpenAI 获取成果过程的认可；评估应由数学共同体展开。该组织强调，公开只是人类理解并将成果纳入数学知识过程的开始，而非结束。AGMAI 当日声明

这份材料比“又一家媒体报道了同样的数字”更有交叉核查价值。它提供的是独立的评价边界，而不是独立复现了全部证明。将“咨询过独立顾问”改写成“独立专家验证通过”，会制造并不存在的信任。

AGMAI 在此前 9 月 29 日发布的建议中，还要求披露模型、提示词、推理摘要、计算时间和成本，并解释尝试失败的问题与问题选择方式；它也主张材料进入不由 AI 实验室控制、具备持久标识和修订记录的学术仓库。负责任发布建议

这些是建议，不是此次发布已经满足的检查清单。OpenAI 当前 README 提供了总体流程、计算量描述以及十个成果家族的简略推理摘要，但不能因此推断每份手稿都附有完整过程记录。模型被称为内部未发布模型，也不能据此认为相同能力已经能通过公开 API 获得。推理摘要与模型说明

开放成果，不等于复现生成过程

这里至少有三种不同的可复核性：别人能否拿到材料，能否重新检查证明，能否在同样条件下重新生成成果。

公开仓库主要改善第一层；形式化材料和检查说明为第二层提供条件；第三层还依赖模型可用性、提示、工具环境、计算预算和过程记录。三者不能相互代替，但也不能因为第三层不完整，就认定前两层没有价值。

仓库提供了 Comparator 检查说明，需要安装 comparator、landrun 和 lean4export，并在 Lean 工程中执行相应命令。Lean README 同时建议小范围编译，指出整体编译可能受 Linux 的 vm.max_map_count 影响。Comparator 说明；构建提示

这些细节说明，可验证不等于零成本。本文没有实际运行这些证明，也没有逐篇核验数学结论。合理的工程姿态，是先固定提交版本、选择一个对应关系清楚的案例、记录环境与结果，再逐步扩大范围；不是把“仓库里存在验证命令”写成“我们已经复现”。

给 AI 产品团队的四个具体建议

第一，把生成器与验收器拆开。假设你在做自动修复代码的代理，模型提交补丁后，应由独立的测试、静态检查和权限规则验收。不要让同一次生成顺带写一句“任务已完成”，就成为任务成功的唯一依据。

第二，先审查规格，再庆祝通过。数学里的命题对应，在软件里就是需求对应。测试全绿仍可能因为漏测了错误输入；格式合法的 JSON 仍可能包含错误业务决定。检查器越强，团队越需要明确它究竟检查了什么。

第三，记录失败与人工介入。除了成功案例，还应保留尝试次数、失败类型、重试成本、依赖版本以及人工修改。一次成功演示可以说明可能性，稳定生产则需要知道成功背后付出了什么。

第四，把审核与理解纳入预算。建议用“模型调用、工具执行、自动验证、人工审核、维护修订”这几个成本桶做核算，而不是只比较 token 单价。这是管理框架，不是本文测得的成本比例。任何模型都可能输出得很快，却把大量后续工作留给接收结果的人。

这四点并不要求所有业务都使用形式化证明。普通内容任务可以采用来源检查，数据任务可以加入约束和抽样核对，涉及付款、权限或生产变更的任务则需要更强的独立验收。关键是让验证力度与错误后果匹配。

下一步该追踪什么

我更关心后续修订、具体命题的独立检查记录，以及专家能否把复杂证明解释成可继续使用的数学工具，而不是下一次发布是否再增加一百份手稿。OpenAI 承诺保留公开版本历史，把更正作为新版本记录，这为持续追踪提供了起点，但承诺本身仍要通过后续执行来检验。版本政策

这次事件给技术社区的启发不是“AI 已经不需要人类”，也不是“没有完整公开模型就一无所获”。更扎实的判断是：AI 研究正在提出一种新的交付要求——不只交答案，还要交可以审查的命题、证据、环境和边界。

生成能力决定我们能提出多少候选结果；验证与理解能力，决定哪些结果值得进入知识体系和生产系统。

参考资料

*本文为技术评论，分析与建议仅代表作者观点，仅供参考；不代表已独立验证全部数学成果。*

评论

发表评论