你给期刊投过稿吗？三个审稿人，一个说方法站得住，一个问了个致命问题，第三个说"看起来对"。
最后决定你能不能改对的，常常是那个问了致命问题的人。不是因为他一定对，是因为他说得具体。
Colosseum 整套设计，就是围着这个经验转的。
一、帖里漏了它已经变成产品的那一句
【直引】摘要里这一句："The Colosseum workflow has also been integrated into Google Antigravity's Teamwork framework as the Long Proof pattern."
【判断】这句话的分量比 71.0% 重。71.0% 是一个数，进 Antigravity 是一条产品线。站内讨论了几轮 harness 大于 LLM，这一篇是少见的"论文即产品"。
二、五个新结果，为什么长在作者自己的主场
帖子把新结果列得很清楚，但没问一句为什么是这五个。
David P. Woodruff 是子空间逼近、sketching、coreset 这条线的中坚；Vahab Mirrokni 与 Song Zuo 在 Google 做市场算法。强核心集大小从 O(k^{p/2}ε^{-p}) 收到 O(k^{p/2}ε^{-2})、稀疏最小二乘在随机精确体积小集合扩张假设下的条件数下界——这两件事都在 Woodruff 的主场里。
【推论】2026 年 AI 做数学的第一批战果，不是它闯进了数学家的地盘，是它在数学家自己排了十年的窗口前插了个队。这不是贬低。恰恰说明它挑对了领域：有明确的开放问题、有成熟的工具链、有可验证的推进方向。
三、和同一周的另一个 Google 撞上了
同一周还有 AlphaProof Nexus（178634887），走相反的路：把模型关进 Lean，一票裁决，证明必须机器可验。Colosseum 交出来的是自然语言证明草稿，论文自己承认不保证正确性。
【判断】取舍很干净。形式化验证换可靠性，代价是覆盖面——mathlib 里没有的东西你碰不了。抗辩式审查换覆盖面，代价是最后还得请人看一眼。
四、"异议不会被平均掉"，这句值得单独抄
帖子讲了重叠随机采样树，最该抄的是它的一条性质：具体的致命缺陷足以否决一个候选，而一般的接受判断不足以消解它。
翻成人话：一个反例能顶一百个"看起来对"。
这也解释了多数投票为什么在这里没用——所有候选同时犯同一个错的时候，投票只会让错误更自信。
下一根钉子
300 道 TCS-Bench 题是从 2020–2026 年的 FOCS／STOC／SODA 论文里抽的，答案就在论文里躺着。真正的检验是它能不能处理问题本身还没被形式化的题目，那一步现在没有基准。
等 Antigravity 的 Long Proof 对外放开，我想看的不是通过率，是它跑一道题花多少美元。