小时候做数学作业，最怕的不是做错，是错在哪里没人告诉你。
如果一个老师能在一秒内指出你第几步算错，而且永不疲倦、永不看错——你的学习会变成另一种东西。
这篇论文所有的魔法，都长在这个前提上。
一、作者块，帖里一个名字都没给
【直引】一手记录里的作者是 George Tsoukalas、Anton Kovsharov、Sergey Shirobokov 等共 18 人，Google DeepMind 与 Aarhus University 合作，通讯作者 Pushmeet Kohli 与 Swarat Chaudhuri。
帖里写的是"DeepMind 的作者们——黄士杰、Thomas Hubert，这些 AlphaZero 王朝的缔造者"。Thomas Hubert 确实是 2024 年 AlphaProof 那篇的作者。这两篇别混。
【判断】把上一代的名字搬到这一代论文上，读者会以为同一批人在推进。实际是同一套机构，换了人。
二、9 题只是成果清单的六分之一
帖子把 9/353 讲透了。论文的自主成果单子比这长：44/492 个 OEIS 开放猜想；解决代数几何里一个 Hilbert 函数开放问题；在凸优化里发现一个新的算法参数调度，改进了已有界；识别出文献中的若干误形式化；协助推进 Ben Green 那张著名清单上的一个开放问题；还在量子光学与图论上做在研支持。
【推论】44/492 比 9/353 更能说明问题。Erdős 题是精挑的难样本，OEIS 是成批、结构化、成功率 9% 的流水线。前者是战报，后者是产能。
三、"对撞一"是事后分析
【直引】公开摘要的原话："We did a post-hoc analysis of the performance of the full-featured and basic agents..."
顺序是：全功能 Agent D 先解出 9 题，然后回头拿基本 Agent A 去试这 9 题，发现 A 全都能做。
【判断】这个结论的方向大概率站得住（成本曲线也支持），但它不是"A 与 D 同条件随机对照"。帖子把这段写成了角斗场对撞，叙事上更带劲，方法学上要降一格。
四、成本口径还有一层
帖子自己写了"几百美元是边际成本"，很诚实。再补两层：论文的成本只算被验证成功的解，不含中途放弃的分支；GitHub 仓库里也只放成功证明，不放失败轨迹。
至于"Codex 7/9、Claude Code 0/9"这两个数，我在论文摘要和二手转述里都没核到，先挂起来，不作结论。
五、和同一周那篇的关系
同一周还有 Stellar Colosseum（178634856），走相反路线：自然语言证明、重叠采样树聚合、明确承认不保证正确性。
Nexus 是一个裁判一票否决，Colosseum 是一群审稿人保留异议。
【判断】两条路的边界是 mathlib 覆盖到哪儿。Nexus 的能力上限就是 Lean 库里已有什么；Colosseum 不设这个限，代价是最后还得人看一眼。
下一根钉子
帖里的"编排折旧"这个说法我很喜欢，但它要能被测才站得住。
直接的测法：同一道题，把 A 的并发数从 1 加到 8，看成本曲线是否已经平了。如果 A 的 Pareto 前沿在低并发处就饱和，那"编排已折旧"才算落地；如果还在陡升，那重装系统只是在用更贵的机器换更短的墙钟时间。