北京时间 10 月 7 日凌晨OpenAI 的数学成果集合进入公开视野。GitHub 仓库的初始提交记录是 UTC 10 月 6 日 21:58:50也就是北京时间 7 日 05:58:50。本文讨论的是这次公开材料而不是把其中此前形成的研究结果全部算成“今天完成”。初始提交记录最醒目的数字是 722 份手稿、372 个成果家族。但如果把新闻压缩成“AI 一口气攻克了数百道难题”恰好会漏掉最重要的变化外界现在可以查看论文、证明材料、形式化目录和部分推理摘要不必只围着公司的结论讨论。OpenAI 仓库说明我的判断是这次发布的技术价值不应主要由手稿数量决定而应由它能否建立一条可复核的证据链决定。对于开发者这比又一张模型排行榜更值得关注当生成越来越容易验证会成为产品设计的一部分而不只是交付前的最后一道手续。先把三个数字拆开根据仓库 README722 是手稿数量372 是相关成果的分组数量。一个家族可以包含主要结果、配套论证、推论或者替代证明。因此手稿与独立突破不是一一对应关系成果家族也不能直接当作统一难度的测试题。目录与产生流程同一份说明称内部未发布模型在评估过程中被提出约 4,000 个问题绝大多数成果采用相同流程产生平均每项成果使用的计算量相当于该模型三小时的 ChatGPT Pro thinking compute。这是厂商提供的计算资源描述不是普通用户可以购买的标准任务报价也不是“每个问题三小时就能解决”的承诺。更不能用 372 除以 4,000宣布得到了模型的科研成功率。分子是聚合并经过重要性筛选后的成果家族分母是尝试的问题两者单位不同一些结果还建立在模型此前的结果之上。缺少逐题对应关系、失败定义和统一验收标准这个除法只有数字没有稳定含义。README 还列出固定流程的例外包括黎曼 zeta 函数无零点区域以及 CM 阿贝尔簇的霍奇猜想相关工作其中 Re(s) 11/12 无零点区域的写作经过人工可读性编辑。这里必须保留对象和条件不能把受限命题替换成更广泛的著名猜想也不能把人工参与藏起来。原始披露这些限定不是对成果的否定而是让后续评价有共同的计量单位。技术团队评估代码助手时也不应把生成的文件数、通过测试的函数数和交付的业务需求数混在一起。Lean 检查的是证明不是新闻标题这次发布值得认真对待的部分是一些自然语言手稿配有 Lean 形式化材料以及关联论文与形式化结果的目录。但官方也明确表示集合中的成果处于不同验证阶段并非所有手稿都已形式化部分未形式化结果可能存在问题。Lean 目录形式化清单这意味着“公开了 Lean 文件”“在特定环境中成功检查了某项形式化证明”“形式化命题准确对应论文主张”“专家认可其新颖性与意义”是四件不同的事。可以用一个假设例子理解你希望证明某算法适用于所有合法输入但形式化时增加了一个更强的输入限制。证明检查器即使接受了证明也只说明形式系统中那个带限制的命题成立不能自动替你删掉限制。问题不一定出在推理步骤而可能出在最初写下的规格。概念图证明检查针对被明确指定的逻辑命题命题是否对应原问题、结果是否新颖以及适用范围如何仍需另行审查。图中不是实验数据也不是官方验证状态图。因此形式化材料带来的进步是把一部分争论从“这段文字看起来对不对”转向可明确检查的对象。它并没有取消专家工作而是改变了专家最该花时间的地方定义、假设、依赖关系、命题对应和数学意义。真正的独立回应没有替全部结果背书独立的数学与人工智能顾问组 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 研究正在提出一种新的交付要求——不只交答案还要交可以审查的命题、证据、环境和边界。生成能力决定我们能提出多少候选结果验证与理解能力决定哪些结果值得进入知识体系和生产系统。参考资料OpenAI数学成果仓库与 READMEOpenAI初始公开提交记录OpenAILean 形式化与构建说明AGMAI关于此次发布的声明2026-10-06AGMAI负责任发布 AI 数学成果的建议2026-09-29Interesting Engineering此次发布的新闻报道媒体补充不视为独立证明验证AceDataCloud相关平台链接不作为数学结论的证据来源本文为技术评论分析与建议仅代表作者观点仅供参考不代表已独立验证全部数学成果。