Agent 写出 46 页的证明：什么时候该拆，意见该退回哪一节 (2026)

9 月 14 日，一篇论文提交到了 arXiv，9 月 15 日更新到第二版，题目是《Stellar Colosseum：面向长周期数学研究的多智能体系统》，作者是 Honghao Lin、David P. Woodruff、Yuan Deng、Jieming Mao、Song Zuo 和 Vahab Mirrokni。这套流程后来被装进 Google Antigravity 的 Teamwork 框架，作为 Long Proof 模式。1 2

它回答的不是「模型能不能做数学」，而是一个更工程的问题：一个循环要跑到几十轮、产出几十页的时候，什么时候才该把任务拆开，验证发现的问题应该回到哪一节。这套设计的四个判断点，独立于数学领域，可以被搬到任何长周期 Agent 循环上。

本期听什么

为什么「什么时候拆」是一个需要判据的决策，而不是默认动作：论文用一道就绪闸门代替「先认定一条路线再走到底」。1
拆开之后，文档顺序和依赖顺序被分成两张图；局部失败只重跑受影响的那一节，不重启整条流水线。1
为什么每一节都通过审查，拼起来仍然可能是错的；全局验证给出的不是分数，而是把缺陷定位到具体章节，跨章节错误同时指出提供方和使用方。1
候选旁边永远站着一个专门找茬的审查者，批评意见跟着候选一起被汇总，汇总不投票、不平均。1
两组数字的真正含义：两个跑法各自的准确率都不到 56%，选对候选之后才到 71%，而两个里至少有一个做对的上界是 77.3%。1

论文说了什么

论文把长周期研究拆成四个难点：路线不确定、技术难点分散、输出太长导致错误累积、以及失败里仍有部分进展。四个难点分别对应四个机制。1

第一道是策略探索和就绪闸门。系统先并行生成一批候选策略，每条策略要交代机制、需要的引理、预期的瓶颈，以及一个可以被证伪的测试。闸门放行的条件不是「证明已经完成」，而是：核心的归约或机制已经稳定，还没拿下的结论已经精确到可以派给某一节，没有一座可能改变目标或论证结构的桥还悬着。中央引理可以仍然很难，但它是什么、起什么作用、预期怎么被证明或验证，都必须是明确的。1

第二道是分解和并行构建。分解器把选中的路线变成一份编号的分节框架，每一节对应一个子问题，子问题之间用依赖边连成有向无环图。文档顺序控制叙述，依赖图控制工作能进行的顺序。依赖完成的子问题才可开工，因此互不相干的章节可以并行。每一节提交前有局部审查；未通过时，这一节带着失败版本和审查意见重跑，依赖图其他部分已完成的工作被保留。1

第三道是全局验证与反馈定位。经过局部审查的章节拼起来仍可能失败：依赖被用错了假设、定义和符号在相隔很远的章节之间漂移、漏掉一个分支，或者最终结论与原始目标不匹配。全局验证本身也是多份独立审查加树状汇总，而且它不是多数投票：一条具体的致命缺陷就足以否决整篇。验证给出的判定附着在具体章节或论断上；跨章节的依赖错误会同时指出提供方与使用方，使反馈可以直接落到需要修改的地方。1

第四道是每个阶段内部共享的推理模式。系统生成一批候选，为每个候选配一个或多个对抗审查者，专门找反例、边界情况、被悄悄加强的假设、循环论证、对已证明结论的误用，以及证明的结论与目标不符。证伪记录始终附着在候选上，候选和批评意见一起通过重叠随机采样的树向上汇总：同一层的每个汇总节点独立地随机抽取若干候选，不同节点之间可以重叠，重叠层级的期望复用率大致在两到三次之间。汇总不是投票或排名，而是建设性的：它可以合并兼容的部分、保留仍在竞争的方案、就地修好一个局部缺陷，或者直接声明冲突尚未解决。根节点返回的是一个合成产物，外加尚未解决的反对意见。1

两个案例研究把这件事落到实处。在 Knuth 的循环问题上，这套流程产出了 46 页和 75 页两份证明草稿，把一次远超单次模型输出的论证变成一份可以持续修改的文档。另一个是单位距离问题：在关闭联网的条件下，系统跑了 15 轮探索，产出一份 22 页草稿，独立走到了另一套解法相同的核心归约上，那份草稿公开在仓库里。1 3

工程上的关键判断

拆解是一个准入决策。这套系统不把「拆」当作默认动作，而是要求先证明路线已经足够确定：机制稳定、未解决的问题可以局部化、没有会推翻架构的未知桥。判据写清楚，拆解才有意义；否则拆出来的子问题会在中途重排。1

验证的价值在于定位。一个总分或者一句「通过」不产生行动。论文把每条缺陷绑到具体章节，跨章节的问题同时指出两侧，这样修复可以局部进行，而不是重跑整条流水线。1

批评意见必须跟着候选走。如果汇总时把候选压成一个答案、把意见丢掉，失败证据就消失了。这套做法把候选和它的证伪记录当做一个整体往上汇总，允许保留互相冲突的分支。论文也明确写着，找不到缺陷不等于正确——没有找到问题，只说明这一轮的攻击不够。1

跨轮记忆分两层。一层是被否决的草稿连同验证意见，整份带进下一轮，让下一轮不必从原始问题重新开始；另一层是知识目录，由专门的整理者记录四类内容：搜索中得到的定理与引理及其假设、失败的路线与精确的失败点、相关文献、以及结构性的观察。每条记录都带着来源与成立条件。1

选择规则是下一个瓶颈。在 TCS-Bench 上，单跑 Gemini 3.1 Pro 是 54.0%，单跑 Gemini 3.7 Flash 是 55.0%，用交叉模型选择后是 71.0%，而「两个跑法里至少一个做对」的上界是 77.3%。两个单跑准确率接近，但错误互补，选择规则把成绩拉高了 48 道题。评分用的自动评审器在 100 道人工标注证明上准确率超过 90%，且只用于计分，不参与选择。1

今天的落地清单

给「什么时候拆」写一条可检查的准入判据：核心机制稳定、未解决的问题能局部化、没有会推翻架构的未知项，三条都满足才分解。
拆解后同时维护两张图：读者看到的顺序，和工作实际允许进行的依赖顺序，不要用文档顺序代替依赖关系。
局部失败只重跑受影响的部分，保留依赖图其他位置已完成的结果。
让验证输出定位到具体章节或论断，跨部分的错误同时指出提供方与使用方，而不是只给一个分数。
批评意见与它针对的候选绑定存储，汇总时不要用投票把不同意见平均掉。
保留失败的中间产物和被否决的草稿，连同当时的原因，作为下一轮的输入。
给候选之间留一条可复用的选择规则，并单独度量它：如果上界和执行结果之间还差很多，瓶颈就在选择，而不是生成。
注意成本口径：论文明确说明，部分开放问题使用了高于默认的并行度，产品化的版本要在成本和能力之间做平衡；论文建议的推理分配自适应、以及用研究轨迹做后训练，都还缺少算力对齐的评估。1

本期事实与数字均来自上述论文及其引用的公开材料。论文的评测结论限于它的实验设置：TCS-Bench 的 300 道题来自 2020 至 2026 年 FOCS、STOC、SODA 的论文，计分依赖一个自动评审器；竞赛编程的 222 道题取自 52 场比赛，按该评测语料自带的难度估计口径计算，不是参赛选手的官方评分。论文也把部分开放问题使用了更高并行度这一事实写在正文里。1

References

1
Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science
arxiv.org
2
Teamwork: When AI Becomes a Research Partner
antigravity.google
3
dpwoodru/erdos
github.com

本期听什么

论文说了什么

工程上的关键判断

今天的落地清单

References

Related content