--- layout: post.njk source: https://yage.ai/share/ai-math-acceptance-staircase-20260812.html speaker: yage.ai title: |- 一份通过检查的证明，为什么在 5 天后补写了 4 页？当 AI 逼出做完的真相 date: '2026-08-12' summary: 文章探讨了在AI生成研究成果（如形式化证明代码）中，机器检查通过并不等同于任务完成的观点。作者通过数学界专家的反馈，阐述了从代码生成到人类理解、阐释和同行复用的多级验收阶梯，并提出了针对AI研发工作流的工程设计原则，强调需要建立清晰的解耦验收机制，以区分代码的语法正确性与逻辑的深度对齐。 area: tech-engineering category: ai-application tags: - ai-verification - agent-workflow - proof-verification - acceptance-criteria people: - Andreas Thom - Francesco Fournier-Facio - Henry Yuen - Terence Tao companies_orgs: - OpenAI products_models: - Lean media_books: [] draft: true status: evergreen --- 2026 年 8 月 1 日，OpenAI 发布了十组研究级数学成果，并附带由 Lean 4 编写的形式化证明代码。在固定提交版本上运行构建命令，终端顺利输出了成功日志，8666 个构建任务全部通过，主定理没有任何 sorry 占位或未完成标记。在计算机眼里，这些形式推导已经具备语法和逻辑规则上的严格性。 到了 8 月 6 日，一份不同寻常的更新出现了。Lean 证明代码本身没有发生任何改动，长达 249 页的自然语言预印本论文却扩展到了 253 页。作者团队在新增的 4 页内容里，重新梳理了前提条件，修复了一个在特定极限情况下可能导致推导失效的漏洞，并补充了与外部已知定理的接口说明。 机器确认形式步骤符合语法规则，并不代表论文已经向人类解释清楚逻辑，也不代表专家已经确认代码忠实对应了最初要解决的难题。当 AI 能够抛出形式代码时，一个过去常被忽视的问题摆到了面前：在 Agent 协助甚至主导的研发工作流里，一项复杂任务到底怎样才算真正做完？ ## 当 Lean 检查一次通过，论文却在 5 天后增加了 4 页 这十项成果发布后，数学与量子信息领域的专家给出了截然分化的反馈。在前置研究作者 Andreas Thom 发表针对非 sofic 群证明的技术解读后，数学家 Francesco Fournier-Facio 迅速利用其中的新机制构造出全新的数学对象，成功将一份代码证书转化为可被同行继续引用的有效工具。 但在另一项关于量子平行重复的成果前，量子信息专家 Henry Yuen 表达了完全不同的态度。他认可 Lean 证书的分量，但也坦诚表示，Lean 证明没有给他带来实质理解，自己尚未消化论文中关于矩阵熵的关键步骤。 这两种后续发展展示了一条清晰的时间线。一项成果被 AI 生成并通过机器规则检查后，还需要经过修稿、阐释、回归既有文献以及被同行复用等多个环节。之后的每一个动作，都在回答完全不同的问题。如果将机器检查通过当成终点，就会把代码跑通与人类理解混为一谈。 ## Terence Tao 的提案：数学界正在重写成果领用规则 面对 AI 产出研究成果带来的冲击，数学家 Terence Tao 提出了关于优先权与信用分配的规则建议。Tao 指出，如果希望为 AI 生成的证明申请学术信用，研究团队应当尽最大努力将其推进至发表与清晰阐释阶段。仅仅依靠系统跑出机器证明，随后便将整理、解释与同行评审工作丢给数学共同体去志愿清理，是一种对成果不负责任的遗弃行为。因此在具体的认定标准上，Tao 建议成果优先权不应当自动授予最早发布 AI 预印本或代码证书的人，而应当授予最先交齐公开阐释、可读论文以及形式证书整套完整材料的团队。 虽然这一提案尚未被期刊与研究机构正式写入管理政策，但它暴露出一个深刻的张力。AI 大幅压低了候选答案的生成成本，反衬出后续对齐、理解与吸收环节的昂贵。在这一背景下，核心价值转移到了能够被他人独立审查、理解和调用的高信度交付物上。 ## 剥离完成的迷雾：从 10 项数学成果看做完的 5 级阶梯 一份证明的 5 级验收阶梯 脱离简单的对错二元论，将任务完成拆解为清晰的阶梯，会发现一项复杂成果实际上需要通过五张不同的验收单。第一级是候选已生成，系统给出初步推导路线，表现为十组自然语言论证的出现。第二级是规则已检查，产物通过确定性检查逻辑，例如 Lean 4 代码通过编译，所有主定理构建成功。第三级是意图已对齐，形式命题忠实反映人类最初想要解决的难题，未发生概念偷换或条件简化。第四级是同行已理解，外部审阅者明确掌握逻辑有效的边界与关键机制。第五级是共同体已吸收，成果进入主干文献，其方法或组件被下游工作持续复用。 截至 2026 年 8 月 10 日，OpenAI 发布的那十项成果已经展现出成熟度的剧烈分化。关于非 sofic 群的证明已经迈入第五级，其机制迅速被后续学者继承并构造出新对象。量子平行重复的成果停留在第二级与第三级之间，关键推导步骤尚未被领域专家完全消化。剩余的五项成果甚至还没有得到具名领域专家的逐定义审阅。这种成熟度的分化表明，规则检查通过仅处于第二级，无法自动替代后续层级的验证与吸收。 ## 给 AI Builder 的系统启示：告别单点 success=true 的工程契约 源自数学形式证明的分层现象，对软件工程与 Agent 工作流设计构成了直接参考。在基于 Agent 的软件开发中，单元测试通过、Linter 零报错或编译器正常运行，直接对应着第二级规则已检查。如果将 Agent 返回的 success=true 直接判定为任务完成，相当于把测试通过误认为是业务需求完全对齐，或者误认为代码具备了可维护性。 在构建 Agent System 时，可以将这种分层提炼为三项工程设计原则。首先是在运行前定义目标层级，在任务启动前明确调用的终点：对于已严格审计的形式化任务，止于第二级符合效率要求；但对于核心业务功能，系统必须被要求推进至第三级与第四级。其次是每层保存独立证据链，避免使用单一布尔值混合测试日志、需求对照与人工确认，同时不允许生成 Agent 单方面宣布跨层级晋升。最后是实施变更驱动的状态回退，一旦输入条件或产物代码发生实质性修改，旧有层级的验证自动失效，系统必须重新触发对应层级的检查。 ## AI 没有削弱完成的价值，它只是拆穿了假装完成 AI 的普及并未降低完成任务的实际价值，反而清除了过去将生成、检查与理解混为一谈的模糊状态。工具越是能够快速抛出形式推导或代码片段，对定义与验收的清晰度要求就越高。 对于 AI Builder 而言，研发与竞争的焦点正在从如何让 Agent 吞吐更多代码，转向如何在系统中建立清晰的解耦验收机制。明确每一层由什么独立证据支持，才能在生成吞吐量爆发的背景下，维持交付产物的真实可靠。