Danus：把数学智能体从“单线做题”变成“事实图协作”

有一个细节比“AI 证明了某个数学定理”更值得盯住：在 Danus 最大的案例里，系统最后留下了 3,157 个经过验证的事实、8,616 条依赖边，最长依赖链深到 54 层；但真正支撑目标定理的，只是其中 664 个事实。其余大量事实不是废料，而是探索留下的脚手架、旁路、失败路线和独立重推。

这听起来不像一次普通的模型回答，更像一群研究生围着同一个开放问题工作了五天：有人找反例，有人证明局部引理，有人翻文献，有人把旧路线否掉。区别在于，Danus 不让这些尝试散落在聊天记录里。每个被接受的数学声明，都必须带着证明进入一张共享的事实图；每条边都说明“这个事实依赖哪些更早的事实”。最后，定理不是从一次灵光一现的长答案里冒出来，而是从这张图上长出来。

这篇论文的核心问题也因此很具体：如果 LLM 已经可以在局部证明、查文献、写草稿上提供一些有用能力，怎样把这种能力扩展到真正的研究级长推理？Danus 的答案不是再把 prompt 写长，也不是简单多开几个模型，而是给智能体系统加一套类似数学实验室的制度：分工、验证、记忆和审稿。

先把几个概念放在桌面上

事实图（fact graph） 可以理解成一张“只收录已验收结论”的白板。白板上每个点是一条数学声明加证明，每条箭头表示后一个证明用了前一个事实。它不是灵感笔记，而是系统的唯一真相来源。

工人智能体（worker） 像同时推进不同支线的研究者：一个去证明引理，一个尝试构造反例，一个研究玩具模型。它们不能直接把想法写进最终证明，只能反复向验证器提交“声明 + 证明”。

验证器（verifier） 是独立裁判。论文强调它是无状态服务：每次只看当前提交、相关事实和引用，不记住自己之前的偏好。这样做的目的，是避免“自己证明自己检查”的乐观幻觉。

全局记忆（memory） 则放那些还不是事实、但值得保留的东西：计划、死路、反例、GPT-5.5-pro 咨询记录、各个工人的进展。事实图负责“什么是真的”，记忆负责“我们试过什么”。这一区分，是 Danus 能并行又不互相污染的关键。

为什么“多开几个智能体”本身不够

最自然的想法是：既然一个数学智能体能推一条路线，那就同时开十个，让它们更快碰到正确方向。论文说，这个直觉只对了一半。Rethlas 这类上一代系统已经有生成—验证—修订循环，但它更像一个人不断编辑同一份 Markdown 蓝图。多个人同时改一份蓝图，很快会变成上下文爆炸和互相干扰：每个工人都要背着整份证明，任何局部修改都可能影响别人。

Danus 的变化，是把“整份证明”拆成可以独立验收的事实节点。工人当前只需要检索与自己目标有关的事实，而不是把所有历史都塞进上下文。通过验证的新声明进入图；如果后来发现某个事实错了，就撤销它以及所有直接或间接依赖它的事实。论文说这种撤销很少发生，但机制必须存在，因为一旦上游事实错了，54 层依赖链就会把错误放大。

这种设计的另一个好处是边界清楚。主智能体负责规划、分配、读日志、总结状态、必要时低频咨询 GPT-5.5-pro；工人负责具体证明搜索；验证器拥有正确性裁决权；事实图是唯一真相来源。论文把这叫严格的 separation of powers。它不像产品宣传语，而是一个很现实的工程约束：负责指挥的人不能顺手把未经验证的数学写进事实库。

一个运行循环：从问题到事实，再到论文

Danus 的一次运行从人类数学家给出自然语言问题开始。主智能体先形成初始计划，必要时向 GPT-5.5-pro 请求高层策略，然后把方向分配给多个工人。论文中的实际项目通常运行 3 到 9 个工人，并把它们大致分成 “high” 和 “xhigh” 两种推理强度；保留一部分较低强度工人，是为了增加浅层但多样的搜索，而不是让所有计算都押在最昂贵路径上。

工人每次只围绕一个 claim 工作：一个引理、一个反例、一个玩具例子。它提出证明，交给验证器；验证器指出问题后，工人修订；直到通过，claim 才进入事实图。主智能体每 1 到 2 小时重读工人日志、全局记忆和事实图，总结当前证明状态，再重新分配任务。停止条件也很硬：不是跑满固定轮数，而是目标定理或其反驳已经作为已验证事实出现在图里。

这里有个容易被忽略的细节：主智能体本身用的是 Claude Code + Claude Opus 4.8，而工人和验证器跑在 Codex agents + GPT-5.5 上。原因不是“哪个模型总是最强”，而是角色不同。论文说 GPT-5.5 数学更强，适合证明和验证；Claude Code + Claude Opus 4.8 更擅长读大量日志、文件和不断演化的事实图；GPT-5.5-pro 数学能力最强但成本太高，只能作为低频专家参考，主智能体最多每小时咨询一次。

这不是一个“单模型能力榜”的故事，而是一个 harness 如何把不同能力拼起来的故事。论文还给了一个清晰基线：六个案例都单独问过 GPT-5.5-pro 网页界面，没有一个产生 meaningful result。在最后的 matroid 案例里，Rethlas 用同样的工人和验证器模型跑了三次也没通过；Danus 则完成了验证解。差异主要来自编排方式，而不是底层模型突然换代。

六个案例里，数字说明了系统真正做了什么

论文没有只给一个 benchmark 分数，而是报告六个研究级数学案例。它们跨代数几何、奇点理论、组合数学和数学物理相关组合结构，人工参与程度也不同。

第一个案例是 foliations 的 optimal bend-and-break。人类给了问题和两篇初始参考，Danus 自己判断其中一篇记号不合适，换成 Kebekus–Solá Conde–Toma 的工作，最后完成证明。这个搜索用了 5 个工人，产生 63 个验证事实和 239 条失败路径。论文对它的定位很克制：策略由人类提供，Danus 的贡献主要是持续执行、迁移技术、补齐连接论证。

第二个案例是三维 foliations 版 Shokurov global index conjecture。这里 Danus 主动把问题按 foliation 的 rank 和 algebraic rank 分成五类；其中三类用人类没预料到的 Lie-theoretic 方法解决，剩下两类在得到人类关于 foliated minimal model program 的提示后完成。这个项目有 7 个工人，第一波运行约 8 小时，事实图长到 784 个验证事实，其中 77 个构成目标定理的支撑闭包。

第三个案例是 rational singularities families 的 total Cartier indices。问题一开始被当成找反例来问，但 Danus 的构造路线最后收敛到肯定答案：先把代数几何问题降到交换代数，再降到实代数几何，并用 Hadamard inequality 等工具处理。这里最有启发的是失败原因：Danus 因为拿不到某篇参考的 TeX 源，从 PDF 里误读了一个维度假设，卡在 codimension three 情况；人类指出误读后，它自行修复。写作阶段第一稿还把一个实代数几何关键引理压缩错了，整稿提交验证器后被拒，再自动修订通过。

第四个案例是 Matryoshka numbers 的阶乘渐近。它是最接近“全自动”的例子：人类只给问题，没有数学指导。Danus 用 5 个工人，约 90 分钟到达已验证目标定理；事实图有 100 个验证事实，依赖链最深 15 层，其中 37 个支撑最终定理；全局记忆只记录一次证明尝试，没有死路。这个案例说明 Danus 不只会在代数几何里沿着专家提示补证明，也能在组合数学物理相关问题上完成从题目到稿件的完整管线。

第五个案例是 logarithmic vector fields 刻画 weighted homogeneous singularities。Danus 给出了一条和人类专家独立证明不同的路线，但后来人类发现它依赖的一篇文献里 “nilpotent” 定义本身有问题，错误传播进了证明。Danus 随后撤销受影响事实，找到正确参考，重建证明。这个项目有 7 个工人、两波搜索、687 个验证事实，修复中又撤销 23 个事实；全局记忆记录 91 次证明尝试和 49 个反例。

第六个也是最大案例，是 matroids 与 wonderful compactifications 的 tangent classes。题目在相关论文上 arXiv 之前提出，并故意不让系统访问那篇后来相关的工作。GPT-5.5-pro 网页界面没有解，Rethlas 三次也没产出通过验证的结果。Danus 用 7 个工人并行约 5 天，得到 3,157 个验证事实、依赖链最深 54 层，其中 664 个支撑定理；全局记忆记录 636 次证明尝试、151 个反例、25 个死路。人类后来指出系统完成的是 rational 版本，而原题要 integral class；Danus 继续工作，补出 integral 版本。不过人类最终也发现一个局部 lemma 的书面论证不完整，虽然该 lemma 为真且不影响主要构造和恒等式。

真正的扩展轴：宽度和深度

这篇论文最重要的概念不是“多智能体”，而是它把 test-time scaling 拆成了两个方向。

宽度 是同时探索多条路线。Danus 可以让工人分别做 constructive 和 refutational 搜索：一边试着证明，一边试着找反例；一边沿某个引理推进，一边研究玩具模型。第六个案例中，3157 个事实里只有 664 个最终被定理引用，正说明宽度带来的不是一条干净直线，而是大量旁支探索。

深度 是把已经验证的台阶保存下来，让后来的工人可以站在上面继续走。没有验证，深度会变成风险：越往上，错误越难发现。事实图的价值就在这里——每个事实入图前已被检查，后续工人可以信任它，不必重证。记忆则负责把五天日志压缩成可读摘要，让一个新任务继承前九个任务的经验，而不是继承一整座日志山。

论文说得很清楚：宽度能找到入口，深度能把论证带远，但它们不保证创造缺失的关键想法。当解法路径存在、只是需要被发现和展开时，Danus 有优势；当问题需要任何单次模型调用都提不出的新概念时，更多工人可能只是更久地绕圈。第二个案例中，卡住的两类最终靠人类给出 foliated minimal model program 的提示解开，这就是边界。

写成论文，不等于证明已经安全落地

一个很诚实的部分，是论文没有把“事实图正确”偷换成“最终稿正确”。事实图里的每个节点可以通过验证，但把几百个节点重排成一篇人类能读的数学论文，本身又是在做数学。压缩、改写、“显然可得”、把两个 nearly matching 的事实粘起来，都会制造新错误。

所以 Danus 把写作也放进验证循环：先生成可读稿，再把完整稿件提交给验证器，直到“按写出来的文本”通过为止。论文特别强调，长稿不能随便切碎给验证器看；每一部分都要是自包含的，带着它依赖的已建立结果。第三和第六个案例都出现过写作阶段错误：底层事实没错，但线性稿件在压缩处出错，后来靠整稿验证—修订循环修复。

这点对 AI 科研系统很关键。很多演示只展示“模型发现了证明思路”，但真正占用专家时间的，往往是检查稿件是否在每个缝合处都严密。Danus 的验证器在这里像第一轮 referee：机器能先修掉的，不要送到人类专家桌上。论文也给了一个很现实的观察：机器搜索一两天产出的结果，人类专家通常要花一两周检查。加速科研协作的瓶颈不只是生成速度，而是把可疑内容挡在专家审阅之前。

论文证明了什么，没有证明什么

这篇工作证明得比较扎实的，是一种编排结构在研究级数学任务上的有效性。它展示了：共享事实图可以让并行工人的贡献累积成长期证明；无状态验证器能作为事实入图的关口；主智能体通过日志、记忆和低频专家咨询，可以把多条支线重新分配到一个整体策略里；在六个案例中，Danus 确实产出了人类专家检查过的数学稿件，且多次完成了非平凡的路线发现、文献替换、错误修复和问题分解。

但它没有证明“AI 可以独立替代数学家”。首先，六个案例都在 Danus–human collaboration 模式下完成。人类给问题，最终逐项检查证明；某些关键点还需要人类提示或纠错。第二，验证器并非形式化证明检查器。论文称实验中几乎没有 false positives，但少数错误来自跳步、引用假设不精确或参考文献本身错误；这些最终仍靠人类 review 兜底。第三，系统的文稿能力还不等于数学写作能力完全成熟：引用格式、记号选择、动机解释和压缩粒度仍需人工修订。第四，案例数量只有六个，而且是与数学家合作挑选和运行的研究问题，不能直接外推成通用科研自动化结论。

因此，Danus 最合理的位置不是“自动数学家”，而是“可审计的证明施工队”。它把 LLM 擅长的局部搜索、改写、查找、试错，放进一个能记录依赖和撤销错误的结构里；把人类擅长的问题选择、关键直觉和最终判断，保留在系统外层。

Big Picture：智能体系统需要的不只是更强大脑，而是可累计的制度

如果只从模型能力看，Danus 似乎没有神秘之处：工人用 GPT-5.5，主智能体用 Claude Opus 4.8，偶尔问 GPT-5.5-pro，验证器也还是 LLM。真正的变化，是这些模型不再作为孤立回答器出现，而是被放进一套有组织的制度里。

事实图让局部正确性可以累计；验证器让累计不至于变成错误堆叠；全局记忆让失败路线也有价值；主智能体让并行搜索不是一盘散沙；整稿验证让“写得像论文”重新服从“按文本可检查”。这套制度把数学推理从一次长上下文输出，改造成一个可追踪、可撤销、可审计的工程过程。

这也是它对更广泛 AI agent 研究的启发。很多复杂任务失败，并不是因为模型完全没有能力，而是因为系统没有可靠机制保存中间真相、区分猜测和事实、让多人并行而不互相污染。Danus 给出的答案很朴素：不要把所有东西都塞进同一个上下文，不要让生成者自己决定什么是真的，不要把草稿当证明。先建立事实，再建立依赖，再让证明从依赖里长出来。

它离“自动解决最深开放问题”还很远。论文自己也承认，当缺少关键新想法时，宽度和深度都可能停在原地。但它已经把一个重要问题讲清楚了：如果未来的 AI 真的要参与研究，最先扩展的也许不是单次回答的长度，而是系统保存、验证、组织和修复事实的能力。Danus 的事实图，就是这个方向上一个很具体的雏形。