数学 Agent 的双循环协议：把开放探索与可信知识分开

让一个数学 Agent 连续工作十小时并不难。真正困难的是十小时之后，你能不能分清三样东西：已经成立的引理，只被原作者反复自证的推导，以及换了记号后重新出现的失败路线。

如果这三类内容都混在同一个上下文里，增加推理时间只会放大不确定性。数学 Agent 真正需要扩展的单位不是尝试次数，而是后续 Agent 可以安全复用的结论。

Chao Xu 在 AI Agents for the Working Mathematician 中给出了一套很具体的长时数学工作流，配套的 Coverify 项目又把其中一部分变成了工具。把两者放在一起看，可以抽象出两条相互制约的循环：

1. 探索循环负责扩张搜索面，记录失败路线，产出候选结论。
2. 验证循环负责攻击候选、独立重构，并把少量通过门槛的结论晋升为可信知识。

本文把它称为数学 Agent 的双循环协议。这是本文为了便于分析提出的编辑抽象，Chao Xu 的原文没有把 dual-loop protocol 当作正式名称。这个抽象的价值在于划清边界：探索可以开放，知识晋升必须严格。

真正的瓶颈是可信复用

大模型生成证明草稿的成本正在下降。一个 Agent 很快就能产出一批猜想、分解、计算实验和看起来像证明的文字。人类和系统都很难以同样速度完成验证。

直接增加 Agent 数量会扩大搜索面，也会同时增加三种债务：相关性错误、重复路线和审核积压。十个 Agent 可能同时爱上同一个漂亮但缺一座桥的证明。几十页推导也可能共同依赖一句未经证明的全局兼容性断言。

因此，系统设计首先应该回答：

一个结论需要携带什么证据，后续 Agent 才能在它上面继续推理？

这比判断一份证明是否顺眼更严格。测试、形式化检查器、敌意审计、独立重构、依赖记录和人工复核，本质上都是验证接口。它们把这看起来没问题，转化为我们知道它通过了哪些检查。

此前的单位距离问题案例展示了同一瓶颈：AI 产生数学结果之后，外部数学家的检查决定了结果能否进入共同知识。双循环协议把这个验证边界前移到日常研究过程中，而不是等最终定理出现后再补审核。

第一条循环：允许探索，隔离污染

探索循环追求路线多样性，但它产生的所有内容默认都是临时状态。

先冻结问题

第一步是写一份固定的 STATEMENT.md。它需要包含完整命题、量词、约定、已知条件、成功标准，以及哪些结果不算完成。

这份文件专门阻止一种高频失效：Agent 证明了一个特殊情形，或者把问题归约到另一个尚未解决的猜想，然后在多轮对话中逐渐把它当成原问题已经解决。研究者可以修改目标，Agent 不能为了适配现有结果而悄悄改题。

按数学机制分路线

探索的多样性来自不同数学机制，不来自 Agent 数量本身。可以并行尝试极值论证、代数重述、嵌入、结构归纳、分解、归约、反例构造，以及能产生小型证书的有限计算。

路线应该按机制和最终缺口归组。三个 Agent 虽然用了不同术语，但都停在同一个未证引理上，它们属于同一条路线。

每次开始前，Agent 都要查阅失败记录，并说明这次尝试的新意。换一个 prompt、变量名或模型采样不构成新路线。新的不变量、来源定理、反例、证书或适用范围才可能构成实质差异。

探索 Agent 的交付物也要具体：一个已证明的引理、显式构造、反例、证书或精确障碍。进展良好、方向有希望这类状态汇报无法被验证，也无法被复用。

失败也要压缩成知识

失败路线值得保存，是因为它能阻止未来再次支付同一笔成本。有效记录需要回答：具体尝试了什么，卡在哪个精确断点，什么证据关闭了这条路线，以及出现什么新条件才值得重开。

这不等于保存所有对话。原始 transcript、重复总结和草稿会消耗上下文，却不会增加知识密度。Coverify 的 Atomic Attempts 设计把边界划得很清楚：原始尝试留在本地审计包里，一次尝试最终只允许零个或一个紧凑、经审核的变更进入持久知识库。

四类文件组成最小状态机

Chao Xu 的原始工作流使用四个持久文件。它们已经足够构成一套最小的数学研究状态机。

这四类内容需要分开。REGISTRY.md 记录正在发生的工作，FAILED.md 保存可复用的负面知识，PROVED.md 只保存通过晋升门的结论。把它们混在一起，很容易让有人试过因为位置接近而变成已经证明。

一条最小路线记录可以使用这些字段：

编号 | 数学机制 | 精确目标 | 剩余缺口 | 最小障碍 | 下一项测试 | 状态

一条失败记录至少需要写清四件事：

尝试了什么？
在哪一步精确失败？
什么证据关闭了这条路线？
什么变化会让重试具有实质新意？

一条晋升记录则要包含命题、假设、证明或证书、依赖项、审核历史和当前证据标签。依赖项尤其关键，因为任何结论的可信度都不能高于它最弱的前提。

第二条循环：先验证，再晋升

当探索循环产出一份完整候选证明后，验证循环才开始。它的任务不是润色，而是判断数学内容能否脱离作者上下文独立成立。

第一关：敌意审计

一个新的 Agent 同时拿到原命题和候选证明。它的目标是推翻证明，重点检查量词偷换、隐藏假设、引用范围错误、分类遗漏、递推不成立，以及被轻描淡写为显然的兼容性断言。

普通审稿容易沿着作者的路线逐步检查局部合理性。敌意审计则寻找最便宜、最决定性的断点。它关心哪里能击穿整份证明。

第二关：盲重构

另一个新 Agent 只拿到原命题和极少量关键思路，不读取候选证明。它需要从头构造一份端到端论证。

盲重构解决的是另一类问题。一份证明可能经受住逐行挑错，因为审计者已经接受了作者的框架和记号。新 Agent 无法独立重构时，往往意味着原证明依赖隐藏桥梁、上下文暗示或只有在已知结论后才显得自然的步骤。

两种检查不能互相替代：

一份证明通过攻击，仍可能离不开作者没有写下来的假设。另一个 Agent 能独立写出证明，也可能复制同一模型家族的共同盲区。

第三关：跨模型或人工复核

同一模型家族的不同采样可以降低上下文污染，但无法消除共同训练分布和推理模式带来的相关性错误。Chao Xu 的标签体系明确区分了新上下文检查与不同模型家族或人类的外部检查。

如果环境中只有一个模型家族，诚实的结论应该是已晋升，尚未完成跨模型审计。对于准备公开的重要结果，领域专家仍然是最强的最终检查者。搜索和审核可以大量委派，发表责任仍由人承担。

五级证据标签防止可信度膨胀

只有已证明和未证明两个状态，无法表达一份结论究竟经历了什么检查。Chao Xu 的工作流定义了五级标签：

关键分界在 self-audited 和 verifier-backed 之间。自我反思可以改进草稿，但它仍然共享作者的上下文、前提和失效方式，无法自动产生独立证据。

证据标签还需要沿依赖关系传播。如果一个已晋升定理依赖一条仍处于 candidate 状态的引理，那么整个定理必须降级。可以把它理解为可信度的类型系统：系统不能把不确定输入静默转换成可信输出。

这个思路与AI Agent 什么时候需要自己的 DSL相通。受约束的表示方式之所以有用，是因为它能让非法状态更容易被检测。证据标签和晋升规则，正是一套描述数学信任边界的最小语言。

形式化验证是额外一层

双循环协议既可以处理自然语言证明，也可以接入计算工具和形式化证明助手。几类验证需要分开描述。

Lean 证明提供一种很强的保证：在声明的基础和依赖下，编码后的形式命题可以由内核检查。Prover Agent 一类系统把自然语言策略、形式化证明生成和 Lean 反馈组合起来。它在形式化竞赛题 benchmark 上报告的结果，与对自选开放问题进行长时搜索属于完全不同的评测场景，不能直接比较。

形式化证明仍然存在规格边界。人或系统需要核对形式命题是否忠实表达了原始自然语言问题，包括量词、定义域和所有附加条件。Lean 内核可以证明编码后的命题，无法替你确认编码的就是原题。

一套完整验证链可以这样分层：

1. 自然语言审计检查数学含义和适用范围。
2. 盲重构检查证明是否能脱离作者上下文成立。
3. 有限计算检查明确的小问题，并保存小型证书。
4. 条件允许时，证明助手检查形式推导。
5. 人类审核意义、规格一致性和发表责任。

这些层可以相互补强，但每一层都只能授予自己实际完成的证据等级。

一套可以直接运行的协议

采用这套方法无需先开发一个大型 AI4Math 平台。目录、规则和现有 Agent 已经可以跑出第一版。

1. 启动前定义完成

写好 STATEMENT.md，明确特殊情形、有限规模验证和归约到未证猜想是否算完成。由人类研究者确认目标。

2. 初始化三类状态

创建 REGISTRY.md、FAILED.md 和 PROVED.md。把字段定义和五级标签写入 AGENTS.md 或可复用 Skill，让不同 session 使用同一份契约。

3. 分波次探索

第一波优先覆盖不同数学机制。多个 Agent 汇聚到同一个终点缺口后，立刻把多余算力转向其他路线。并发量要服从路线注册和验证吞吐，而不是服从模型平台允许的最大线程数。

4. 只接收决定性工件

每个 Agent 返回一个紧凑工件并更新路线表。计算任务需要有明确问题、源文件、超时、日志、输出位置和小型证书。有限计算可以推翻引理或发现构造，无法单独证明无穷命题。

5. 自动触发两类验证

完整候选出现后，用新上下文依次执行敌意审计和盲重构。记录 prompt、输出、模型家族、结论和未消除风险。

6. 只晋升紧凑知识

把通过门槛的结论、依赖、证书和审核记录写进 PROVED.md。原始草稿、对话和未解决分支留在隔离区。

7. 用报告门控制打扰

只有出现完整证明、认证反例、消除明确依赖的已证引理，或者关闭路线的精确障碍时，才打断研究者。新记号、另一轮有限计算和方向乐观都留在工作记录里。

这可以看作 Harness Engineering 三维扩展框架在数学研究中的具体版本。时间、并发和交互能够扩展的前提，是状态管理和验证能力一起扩展。

3/10 和数百 Agent 能说明什么

Chao Xu 在原文附录中自述：过去几天的多个 orchestrator 累计调用了数百个 subagent，典型工作波次是六个 Agent 推进前沿，再换一批新的六个 Agent 审核结果。他还自述测试了十个开放问题，每题至少运行十小时，提前解决的除外，最终解决三个。

这些数字可以帮助理解工作量，无法作为方法有效性的实证。

原文没有公开完整的十题清单、全部运行日志、成本明细、每个成功结果的独立评审，以及单 Agent 或普通聊天的对照组。因此，3/10 只能描述一位操作者的个人运行结果，不能证明双循环协议提高了开放问题求解成功率。

可以站住的结论更克制：长时数学 Agent 需要显式状态、独立验证和诚实的证据标签。这个结论来自架构和失效边界，而不是那组成功率数字。

还有一个容易写错的细节：至少十小时指每个问题的运行时间，不是每个 subagent 都运行十小时；数百个 subagent 是几天内累计数量，也不是同时并发。

六种常见失效

审核者变成第二个作者

审核 Agent 一边找错一边重写证明，可能会把原漏洞藏起来。审计和修复应该分开：先固定阻塞问题，再由作者产生新候选。

把新窗口当成独立验证

同一模型家族的新实例属于新上下文检查，仍然保留相关性风险。标签需要如实反映这一点。

知识库变成 transcript 仓库

保存全部内容会降低信息密度。持久知识只保留可复用命题、精确障碍、小型证书和影响未来路线的决策。

失败路线通过改写复活

每次重开都要求一份实质新意说明，明确新的机制、证据、证书、反例或适用范围。

计算代替证明搜索

编程 Agent 天然倾向于写程序。每次计算都要回答一个有限数学问题，并留下可以独立检查的证书。

证据标签沦为装饰

条件允许时，应该把晋升门写进工具权限。Danus 就采用更强的角色隔离：规划者、证明 worker 和冷启动 verifier 拥有不同权限，只有 verifier 接受的事实才能进入事实图。Prompt 可以规定行为，权限边界能进一步阻止结论自行升级。

FAQ

AI Agent 能产生有效数学证明吗

可以，但有效取决于证明经历了什么验证。看起来像证明的回答只是 candidate。形式化检查、独立重构、跨模型审核和人类审核提供的是不同类型的证据。

一定要使用 Lean 吗

不一定。自然语言数学可以使用敌意审计、盲重构、计算证书和人工评审。Lean 适合能够形式化的命题，并额外要求检查形式命题与原题是否一致。

同一个模型问两次算独立验证吗

它算新上下文检查，不算完整独立审计。同一模型家族可能共享盲区。最终重要结论应再交给不同模型家族或人类。

应该同时运行多少个 Agent

取决于路线表、算力预算和验证吞吐。只有 Agent 在探索实质不同的机制，并且结果有能力被审核时，增加并发才有价值。六个 Agent 只是 Chao Xu 的一个运行实例，不是通用最优值。

什么内容可以进入 PROVED.md

只有通过既定门槛的紧凑、可复用结论：精确命题、假设、证明或证书、依赖项、证据标签和审核记录。原始 transcript 与未解决草稿继续留在隔离区。

参考资料

• Chao Xu：AI Agents for the Working Mathematician，2026。
• Chao Xu：Coverify 与 Atomic Attempts，2026。
• frenzymath：Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory，2026。
• Kaito Baba 等：Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs，2025。
• OpenAI：CDC Prompt。
• Google DeepMind：AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems，2024。