论文链接：Cogentic: Multi-Agent Orchestration for Automated Proof Discovery（arXiv:2609.40324v1，2026-09-30） 结果索引：sites.google.com/view/cogentic（含五篇配套论文链接） 机构：Google Research（七位作者；Yang Cai 兼 Yale University，Vineet Gupta 兼 Google DeepMind） 领域标签：cs.AI，多智能体、自动定理发现、在线学习、拍卖理论

题目区：当 AI 开始「自己写数学论文」

2026 年 9 月 30 日，Google Research 的七位研究者放出一篇论文，标题相当克制——「Cogentic: Multi-Agent Orchestration for Automated Proof Discovery」（多智能体编排的自动证明发现）。但内容毫不克制：

一个多智能体系统，只接收问题的自然语言陈述，不需要任何专家提示或暗示，自动产出了五个研究级数学定理的完整证明，每个证明由领域专家独立验证，并分别写成配套论文。

五个问题覆盖在线学习（online learning）、拍卖理论（auction theory）、机制设计（mechanism design），难度对标 STOC/FOCS 旗舰理论计算机科学会议的开放问题。这不是「AI 做出奥赛题」——竞赛题有答案钥匙，开放问题没有。

更扎眼的是预算：大多数问题只用了 O(100) 次 Gemini 调用，最难的问题 O(1000) 次。对照同月 OpenAI 攻克 Navier-Stokes 千禧难题动用的约一万个并发 agent、八十八小时、数百万美元，Cogentic 走的是一条「低预算、高可信、专家可验证」的路线。

两天后（10 月 2 日），Meta 发布了 Muse Spark 辅助的六篇数学论文，走的是完全相反的路线——「无脚手架对话式」。这两条路线的对照，恰好构成了 2026 年秋天「AI 做数学」争论的两极，本文第二部分会展开。

先看 Cogentic 到底做了什么。

一、论文背景：从竞赛级到开放问题，单次生成的天花板

1.1 LLM 数学能力的三级跳

大语言模型的数学能力演进可以粗略分三级：

• 第一级：竞赛数学。IMO 金牌级表现已被多个前沿模型拿下，这一层的标志是题目有已知答案、有标准解法、视野短（一道题一次推理就能走完）。
• 第二级：辅助研究。模型作为工具嵌入人类研究流程——帮忙计算、找反例、起草片段，人类数学家选题、掌舵、验证。
• 第三级：自主发现开放问题的解。问题没有答案钥匙，可能需要探索多个相互竞争的猜想、绕过微妙的技术障碍、在极长的视野里积累进展。

第三级是公认的硬骨头。论文的立论正是从这里切入：单次生成（single-shot generation）在结构上不足以应对第三级任务。

1.2 单次生成的三个结构性缺陷

论文对「开放问题」给出了三个关键特征刻画，每一个都直指单次生成的软肋：

1. 需要探索多个相互竞争的猜想（competing conjectures）。开放问题往往同时存在几个看似都成立的方向——界是 O(d) 还是 O(d log d)？常数能不能收紧？反例存在吗？单次生成只能押注一个方向，押错了整次调用报废。
2. 需要克服微妙的技术障碍（subtle technical obstructions）。证明卡住往往不是全盘皆错，而是某一步过不去。单次生成没有「卡住后换工具」的机制。
3. 需要在长视野内保留中间进展（retaining intermediate progress over a long horizon）。一次尝试里可能有三条引理是对的、只有最后一步崩了。单次生成用完即弃，对的引理下次还得重新发明，错的坑下次还会再踩。

一句话总结：单次生成没有纠错回路，也没有累积机制。 而 Cogentic 的整个架构，就是围绕补上这两个东西设计的。

二、论文定位和关联工作：四条线上的位置

Cogentic 在 Related Work 里把自己放进了一个已经很拥挤的地图。把地图画全，大致四条线加一个同期对照。

2.1 形式证明线：Lean / Isabelle / Coq

交互式定理证明器提供机器可查的正确性保证，近年被 LLM 大幅降低使用成本：LeanDojo 做前提检索和 tactic 生成，Draft-Sketch-Prove 把非形式证明转成形式草图，RL 训练的模型已能做奥赛级形式推理，Tsoukalos et al. 2026 进一步把 AI 驱动的形式证明搜索推向开放研究问题。

Cogentic 的对照点：它用自然语言工作，产出领域专家可直接验证的数学散文。Discussion 部分说得很坦诚——可以用 Lean 形式化来机械地解决正确性问题，但「人类对解的理解可能滞后」：机器说对了，人没看懂。Cogentic 选择人类可读作为第一优先级。

2.2 搜索数学对象线：FunSearch / AlphaEvolve / AlphaGeometry

DeepMind 的 FunSearch（Nature 2023）首次用 LLM 在开放问题上做出可验证新发现——cap set 问题的新构造；AlphaEvolve（2025）把「进化 + 自动评估器」推广到整个代码库，改进了 Strassen 矩阵乘法算法、接吻数下界，甚至回收了 Google 全球 0.7% 的算力。再加上测试时学习的 ThetaEvolve、神经符号搜索的 AlphaGeometry 系列。

Cogentic 的对照点：这类方法的命门是需要廉价、忠实、机器可算的分数（score oracle）——程序跑一遍就能打分。组合构造和算法搜索天然满足，但定理证明不行：一份 30 页的证明没有「跑一遍打分」的接口。确实有些定理可以归约为「找具特定性质的数学结构」（AlphaEvolve 配 oracle 证过不可近似性），但并非每个问题都适用。Cogentic 的对抗性 verifier 就是为「没有 score oracle 的世界」设计的替代品。

2.3 Agentic 系统线：co-scientist / ProofCouncil / Stellar Colosseum

Google 自己的 AI co-scientist（Nature 2026）用生成-反思-排名-进化的多智能体锦标赛做科学假说发现，在药物重定位上拿到了体外实验验证；此外还有 ProofCouncil、Stellar Colosseum、AI co-mathematician 等一批研究级数学 agentic 系统。

Cogentic 的对照点：co-scientist 产出的是假说（可以拿去实验室验证），Cogentic 产出的是证明（验证内置于系统内部——至少设计意图如此）。这一步之差使 Cogentic 必须把「验证」做成一等公民，而不是留给外部。

2.4 大型里程碑对照：OpenAI Navier-Stokes

2026 年 9 月 8 日，OpenAI 宣布内部系统（万级并发 agent、88 小时、数百万美元）解决了 Navier-Stokes 千禧难题的一个表述，并给出 Lean 形式化。同期还有 Anthropic 侧的 Riemann-zeta 相关工作与离散几何猜想的否定。

Cogentic 的对照点：聚焦作者专长领域、STOC/FOCS 级别难度，但推理预算低两个数量级以上。如果说 Navier-Stokes 展示的是「暴力规模上限」，Cogentic 展示的是「一个研究组量级的预算能走多远」。

2.5 同期对照：Meta Muse Spark 的「无脚手架」路线

2026 年 10 月 2 日——Cogentic 发布两天后——Meta Superintelligence Labs 发布六篇数学论文，其中五篇回答了此前开放的问题。关键差异在于过程声明：

• Muse Spark 路线：数学家通过普通 meta.ai 聊天界面使用 Muse Spark 1.1/1.2 的 Thinking Mode，没有定制研究脚手架；数学家选题、引导、论证，第二个数学家小组审查；每篇论文标注哪些段落由人起草、哪些由 AI 起草；多个问题存在独立的并行解答。
• Cogentic 路线：系统自主运行到产出论文，运行中无人类数学干预，验证由系统内部的对抗性 verifier 完成，事后人类专家独立复核。

两条路线其实是同一个问题的两种回答：「验证瓶颈该放在哪里？」Muse Spark 把它留给人类专家（模型起草、人选择并拥有），Cogentic 把它内化成系统组件（对抗验证 + 专家事后复核）。Meta 那边的实践证据（模型生成的 GAP 搜索程序找到 384 阶反例、人类完成验证）说明聊天界面 + 专家也能推进开放问题；Cogentic 则证明脚手架本身可以自动化掉「探索组织 + 中间进展管理」。孰优孰劣没有定论——但 Cogentic 论文里的一个细节值得注意：它的五个结果是系统在无人干预下得到的，且其中一个定理（PoA 第二部分）作者从未研究过、未给任何提示，机制和分析完全由系统独立想出。

三、问题定义：把「做研究」形式化

Cogentic 的任务定义一句话可以说完：

给定一个开放研究问题的自然语言问题陈述（无需任何专家提示或暗示），自动发现可由领域专家验证的、人类可读的数学证明，以论文形式输出。

拆开看有四个要件：

注意「无专家暗示」的实际强度可以从附录 A 的提示词看出来：五个问题里有四个只给了问题形式化或目标方向（比如「能否设计 regret 关于 d 多项式且与 T 无关的算法」）；最直接的一个（双边市场）干脆把目标定理本身写了出来（「证明加 2 个卖家足够」）；最间接的一个（autobidding n≥2 部分）只要求「先理解下界，再设计机制逼近 2−Ω(1/n)」——而系统最终给出的机制是作者从未研究过的。

这个任务定义故意不要求「机器可验证」——这是与形式证明路线的根本分野，也是后面一切架构选择的源头。

四、问题解法：像研究小组一样分工

Cogentic 的设计灵感来自作者自己做理论研究的经验：像一个研究小组那样分工——导师决定做什么，学生并行起草证明，审稿人挑毛病，账本记录什么已经被证明过了。所有 agent 共享磁盘上的 workspace，按轮次（rounds）推进，直到某个草稿通过全部验证或预算耗尽。

4.1 组件总览

几个组件的细节值得单独展开，因为它们是第六节「为什么有效」的直接证据来源。

4.2 对抗性双验证：两道关卡

每份草稿要过两道独立的对抗关卡：

1. 单独审：每份草稿配一个专属 verifier，逐步检查正确性，立场是假定每一步都错、每条引用都假，直到被论证或核查。
2. 并排审：另一个 verifier 把该轮所有草稿放在一起读——发现共同盲点（所有证明都在同一处偷懒）、比较各证明强弱。

这个设计的深意在于：「看起来对」是 LLM 证明最危险的失败模式。对抗性立场把筛选阈值抬高到「每一步都被单独论证过」。并排审则是单草稿验证做不到的——它审查的不是一份证明，而是「这一轮的证明群体」的系统性弱点。

4.3 Verified ledger：棘轮机制

这是全文我认为最漂亮的设计。开放问题研究里最常见的挫败是：整证失败，但里面有几块是对的。人类研究者的对策是把这些块抽出来变成引理，下次直接用。

Cogentic 把这个过程制度化了：轮末 auditor 从被拒证明里抽取被 verifier 确认过的引理片段，改写为自包含引理并隔离地重新验证，存活者进入 ledger，供后续所有 prover 复用而无需重证。死胡同同样入账——比如被已验证反例排除的 bound 会被记为「已排除」，防止后续轮次重蹈覆辙。

效果是一个单调只增的已验证知识库——棘轮（ratchet）：进展只能积累不能倒退，每一轮都站在已验证资产上出发。对照单次生成「对的引理下次还得重新发明、错的坑下次还会再踩」，这是针对「长视野进展保留」的直接机制回答。

4.4 角色分权：流程与数学判断分离

Orchestrator 和 advisor 被显式禁止持有数学观点：不能猜测答案、不能推荐技术、不能宣布某方向有希望或已死。数学判断只来自两个渠道——prover 的草案和 verifier 的对抗检验。

这条约束初看奇怪（编排者见多识广为什么不让他发表意见？），实则是对「裁判兼球员」式立场污染的防御：一旦管理者持有数学偏见，探索空间就会被过早封闭，剩下的 prover 都在验证管理者的直觉而非探索猜想空间。advisor 单设一个 agent 的原因也很实际：orchestrator 要同时照看多个 agent，没有多余的上下文窗口去审查综合日志趋势。

4.5 一轮的完整运转

把组件串起来，一轮的流程是：

1. 开局：问题陈述 → 文献综述 → planning，orchestrator 分配研究方向。
2. 轮内：summarizer 为每个 prover 写独立简报 → provers 并行起草 → 每份草稿单独验证 + 全轮并排验证（双关卡）。
3. 轮末：写下三样东西——尝试记录及失败原因（record）、已验证中间结果（ledger）、advisor 维护的常设指令。
4. 终止：草稿通过验证后 orchestrator 还可继续探索可能给出更好结果的剩余方向，穷尽后终止 → comparator / formal writer / 最终审计 → 已验证手稿。

扩展性的答案也在这里：更难的问题主要映射为更多轮次和更多 prover，而不是更长的单次上下文——长上下文恰恰是单次生成的瓶颈。简报机制保证上下文按需压缩：只给最相关的历史，长文档给路径按需读取。

五、评估指标与实验证据：五个定理

论文的评估不是跑基准，而是「解开放问题」本身。Table 1 汇总五个问题，所有结果均由领域专家独立验证并写成配套论文。逐一过一遍（技术细节做了压缩，完整版在配套论文里）。

5.1 定理一：在线逆线性优化的 O(d) regret

问题：在线学习者在未知切平面序列上做线性优化，regret 能不能既高效又 proper 地做到关于维度 d 多项式、且与视野 T 无关？

此前格局：高效界 O(d ln T)；T 一致的界要么指数级要么需要额外结构；Dewasurendra (2026) 证出有限 poly(d) 界可行但该规则既不 proper 也不高效。高效 + proper + T 一致三者兼得是空白。

Cogentic 结果：首个同时高效且 proper 的 O(d) regret 界，对视野 T 一致，每轮 O(d²) 次算术运算加一次线性优化，确定性、anytime。距已知下界 Ω(√d) 差 O(√d) 因子。

技术要点：基于 variable-metric 框架做两处改动去掉对数——把度量更新按对偶长度自归一化；用 trace power 势函数替换 log det 势函数（后者增长如 d log T，正是以往所有体积分析中 ln T 的来源），使累计平方和对数有界，与视野无关。附加成果还包括首个对抗非优化专家的 O(d) 界、corruption-robust 与 rank-adaptive 变体。后续 Sakaue (2026b) 得到紧的 O(√d) 界但算法非高效——高效 O(√d) 仍是开放问题。

5.2 定理二：双边 Bulow-Klemperer，20000 → 2

问题：竞争复杂度（competition complexity）问：要让简单机制达到最优机制的收益，需要往市场里加多少参与者？

此前格局：单侧加约 n(m+4√m) 个买家可以（Babaioff et al. 2020）；同时扩两侧 O(1) 个就够但常数巨大——每侧至少 20000（Cai et al. 2024）。两个开放问题：常数能否改进？是否只需单侧招聘？

Cogentic 结果：两个问题同时解决——买家分布一阶随机占优卖家分布时，只需在较小的一侧（卖方）加恰好 2 人即可让 Seller Trade Reduction 的期望 GFT 达到原市场 first-best：STR(m, n+2) ≥ OPT(m, n)。且紧：即使 m=n=1，多招 1 个卖家对任何 prior-independent 机制都不够。

意义：常数从每侧至少 20000 降到单侧 2。机制设计者只需再找两名本就稀缺类型的参与者。这是五个结果里对比最悬殊的一个。

5.3 定理三：证明 anytime regret 猜想

问题：不知视野 T 的 anytime 算法，regret 前导常数是否必然比固定视野算法差 √2 因子？

此前格局：固定视野下 multiplicative weights 的 1/√2 前导常数不可改进；anytime 最好保证 √(t ln n)，差 √2。Harvey et al. (2023) 给出 n=2 最优 anytime 算法并猜想 n→∞ 时 anytime 与固定时间前导常数一致；Harvey et al. (2024) 在连续时间布朗运动专家模型下证明了一致。

Cogentic 结果：证明该猜想——存在不知视野的算法，对所有 t≥1、所有损失序列同时满足 R_t ≤ (1 + O(√(ln ln n / ln n)))·√(t ln n / 2)。anytime 有效性没有前导阶代价，前导常数最优。

技术要点：证明初等——在几何网格上每个视野跑一个 multiplicative-weights 实例，用主 multiplicative-weights 聚合。难点在活跃实例数随 t 增长而主算法 regret 随跟踪实例数增长；解法是让实例按窗口唤醒退役，使同时活跃数与 t 无关，退役留下的未覆盖前缀递归贡献几何级数。参数取 ε、δ 使三项开销合计 1+O(ε)。证明一个别人明确陈述的猜想——这在 AI 数学发现里是标志性事件。

5.4 定理四：分开卖 vs 打包卖，5.2 → 3.52

问题：单买家可加估值下，分别卖（SRev）与打包卖（BRev）的组合能逼近最优收益 OPT 到什么程度？

此前格局：OPT ≤ 6·max(SRev, BRev)（Babaioff et al. 2020）；Ma & Simchi-Levi (2021) 改进到 5.2；下界 2（Rubinstein 2016）。最优常数未知。

Cogentic 结果：3.52·max(SRev, BRev) ≥ OPT。

技术要点：基于对偶框架，以往分析在 SRev 处截断并分 Core/Tail 分别界；此处改在联合尺度 M=max{SRev, BRev} 处截断，直接证明非最爱物品福利的上界，完全去掉 Tail 分析；再从二阶矩的极端分布推出 E[V_M] ≤ 常数倍 M。

运行细节（附录 A.4，很能说明系统行为）：提示词要求证 factor-3，并指示「证不出 3 先证 4 再加强」——最终系统给出 3.52。系统没有机械执行「先证 4」的降级路线，而是直接找到了介于 3 和 4 之间的证明。

5.5 定理五：autobidding 拍卖的 PoA 紧界

问题：自动出价者（value-maximizing bidders）参与拍卖时，机制的无政府价格（PoA）——均衡社会福利距最优的最坏比值——能好到什么程度？

此前格局：第二价格拍卖 PoA 紧为 2；确定性机制破不了 2 的屏障；随机化第一价格拍卖到 1.8（n=2）；匿名机制下界 2−4/(n+4)。两个开放问题：n=2 的精确 minimax 最优 PoA？一般 n 能否破 2 并匹配下界？

Cogentic 结果：通过 r-比例第一价格拍卖族 pFPA_r 同时解决两个：(1) n=2 时 pFPA_1 的 PoA ≤ 1.5 且紧（温和假设下任何匿名双出价者机制 PoA ≥ 1.5）；(2) 一般 n≥2 时 pFPA_{2n} 的 PoA ≤ 2 − 1/(4n+1) = 2 − Ω(1/n)，与下界在 1/n 项常数因子内匹配。

人机关系细节：作者此前已猜到比例第一价格拍卖会优于 rFPA、猜想界为 1.5 但没有证明——Cogentic 证出了上界和任意机制的下界，把作者的直觉变成了定理。而第二部分（一般 n 的机制设计）作者从未研究过、未给任何提示，系统独立想出了机制和分析。这是五个结果里「自主性」含量最高的一个。

5.6 预算与可信度

• 推理预算：大多数问题 O(100) 次 Gemini 调用，最难的问题 O(1000) 次。论文称调用次数仍有优化空间，系统也自然支持扩大规模解更难的问题。
• 可信度闭环：每个证明由领域专家独立验证，并写成配套论文（arXiv:2609.13440 / 2609.27206 / 2609.28873 / 2609.27304，autobidding 一篇 forthcoming）——不是「系统说自己对了」，而是「专家复核 + 独立成文」。

六、效果优势的根源解释：机制层面的因果链

第五部分的事实是「它 work 了」；这一节回答「为什么 work」——单次生成缺什么，Cogentic 的哪个组件补上了什么。逐条建立因果。

6.1 对抗性双验证 → 可靠筛选信号

单次生成的缺陷：没有纠错回路，输出直接消费。 Cogentic 的机制：每个草稿过两道对抗关卡（单独审 + 并排审），verifier 立场是「每一步皆错直到论证、每条引用皆错直到核查」。 因果链：对抗立场把「看起来对」挡在门外 → 只有真正通过的才进入 ledger → 累积的是已验证资产而非幻觉。并排审额外覆盖了单草稿验证够不着的失效模式：一轮证明群体的共同盲点。

6.2 Verified ledger → 棘轮效应

单次生成的缺陷：进展不累积，错误会重犯。 Cogentic 的机制：auditor 从被拒证明中抽取已确认引理、隔离重验、入账复用；死胡同入账防重访。 因果链：已验证知识库单调只增 → 每一轮站在已验证资产上出发 → 「长视野进展保留」从指望变成机制。这是针对第三节问题定义里第三个特征（长视野保留中间进展）的直接结构回答——不是靠模型变强，而是靠架构保证。

6.3 方向并行 + 独立简报 → 猜想空间的结构化探索

单次生成的缺陷：一次押一个方向，押错整次报废。 Cogentic 的机制：orchestrator 把 prover slots 分到不同方向（不同 bound/常数/构造/反例/修复），每个 prover 收到由不同 summarizer 独立写的同一历史的不同解读。 因果链：方向划分覆盖竞争猜想 → 独立简报保证同轮 provers 带着不同视角出发（而不是同一提示的 N 次采样）→ 比采样多次独立回答更接近研究组对竞争猜想的系统探索。prover 只被告知方向不被规定做法，保留策略自由度。

6.4 失败信息结构化复用 → 错误变成训练信号

单次生成的缺陷：错误只浪费一次调用。 Cogentic 的机制：record 记录每次尝试的方法与失败异议；advisor 跨轮审查日志，发现重复错误、论证共性缺口、验证盲点，据此调整指令（对反复错误发警告、对易偷懒步骤提高论证标准）。 因果链：失败模式被识别为模式（而非孤立事件）→ 以常设指令形式注入后续轮 → 同类错误的发生率下降。相当于在推理时做了一个「无梯度的课程学习」。

6.5 角色分权 → 防立场污染

单次生成的缺陷：（不存在此问题，但朴素多智能体会引入此问题——编排 agent 若持有观点会封闭探索。） Cogentic 的机制：orchestrator 与 advisor 显式禁止持有数学观点，流程控制与数学判断分离。 因果链：管理者的偏见无法封闭探索空间 → 数学判断只来自 prover 草案与 verifier 对抗检验 → 竞争猜想得到公平探索。这条约束在多智能体系统里并不常见，值得抄。

6.6 小结：一张缺陷-机制对照表

七、必要知识反推：读懂这篇论文需要什么

按阅读顺序列出前置知识，读者可以按需补课。

数学侧（读懂五个定理大概需要）：

• 在线学习：regret 的定义、multiplicative weights / 在线梯度下降、anytime 算法的概念。定理一还需要 variable-metric / 在线牛顿步的直觉（势函数怎么控制 regret）；定理三需要知道「固定视野 vs anytime」的 √2 gap 问题背景。
• 拍卖与机制设计：第一/第二价格拍卖、truthfulness、prior-independent 机制、first-best vs 机制实现的福利差距（GFT）、Seller Trade Reduction 机制、bundling vs separate selling（SRev/BRev）、price of anarchy、value-maximizing（autobidding）出价者模型。
• 一般：big-O 与下界的语言、紧界（tight bound）的含义、「猜想被证明」在数学社区的意义。

AI 侧（读懂系统设计需要）：

• 多智能体系统的基本概念（角色分工、消息传递、共享 workspace）。
• 单次生成 vs agentic workflow 的区别；为什么 CoT/self-consistency 等推理时扩展方法仍然没有纠错回路和累积机制。
• 形式证明工具链（Lean/Isabelle）能提供什么、不能提供什么——机器可查 vs 人类可读的权衡。
• FunSearch/AlphaEvolve 的「LLM + score oracle」范式——理解 Cogentic 为什么需要另起炉灶（证明没有廉价 oracle）。

八、通用性灵感：超出数学之外的三点

1. Verified ledger 是一个可迁移范式。「从失败的尝试中抽取被验证的片段、隔离重验、入账复用；死胡同也入账防重访」——这个模式不限于数学。代码评审里被拒的 PR 中被确认正确的工具函数、科研实验中失败的整体假设里被单独证实的子现象、产品设计里被毙方案中通过用户验证的组件——都可以进入各自的 ledger。核心是把「失败」从二值事件变成可分解的资产流。任何长视野、多轮次的 agent 系统都值得问一句：我的 ledger 在哪？

**2. 对抗性验证 + 角色分权是「没有 score oracle 的领域」的通用配方。**凡是没有廉价机器评分的领域（论证、分析、设计、法律推理），可靠筛选都可以靠「假定每步皆错直到论证」的对抗 verifier 加「并排审发现共同盲点」的群体审查来近似。而「编排者不得持有领域观点」这条约束，对所有多智能体系统都是廉价的防腐剂——它防止管理层的偏见悄悄变成整个系统的偏见。

3. 低预算高可信的证明发现流程有工程复制价值。O(100)-O(1000) 次调用解 STOC/FOCS 级问题，意味着这套流程不是巨头专属：一个研究组量级的预算就能跑。配方已公开：轮次结构、方向并行、双重验证、ledger、consolidation。可以预期的应用：理论组用它攻坚堆积的 conjecture、工业实验室用它自动化技术报告里的引理证明、甚至用同样的框架做「带证明的算法分析」。与 Muse Spark 的「无脚手架对话式」路线相比，Cogentic 证明的是脚手架本身可以被系统化——当 scaffold 的设计知识沉淀为可复用的架构，它的边际成本会趋近于零。

最后一个开放的问题留给读者：当 Cogentic 这样的系统把「探索组织 + 中间进展管理 + 验证」都自动化之后，人类数学家的不可替代部分还剩什么？论文的答案藏在它的设计里——问题陈述、以及最终的独立验证。陶哲轩在 Navier-Stokes 事件后警告「好问题正在变成稀缺资源」；Cogentic 把问题选择和结果检验留给人，或许不是谦虚，而是对这件事的准确判断。

一句话总结：Cogentic 用「对抗性双验证 + verified ledger 棘轮 + 角色分权」把研究组的证明发现流程系统化，在五个 STOC/FOCS 级开放问题上以 O(100)-O(1000) 次 Gemini 调用的预算得到专家验证的定理——它证实的不是模型变强了，而是架构可以补齐单次生成的结构性缺陷。