知识卡片：Danus：基于事实图记忆的数学推理智能体编排系统

一句话结论： Danus 是一个利用共享事实图（fact graph）作为全局记忆，协调多个 LLM 驱动的工作智能体并行进行研究级数学证明搜索的系统，在代数几何、奇点理论和组合学的六个研究级案例中成功构建了长链条数学证明。

事件概述或研究问题： 现有基于大语言模型（LLM）的数学推理智能体已能处理研究级问题，甚至协助解决开放问题。但在扩展和编排这类智能体时，面临并行证明搜索协调困难以及中间命题难以组织和保持可靠性的挑战。本文提出 Danus，旨在通过事实图记忆机制解决上述问题。

方法/产品要点：

• 系统架构：由三个核心组件构成：
  • 主智能体（main agent）：负责全局规划与协调，定期总结进化中的证明状态，重定向工作智能体至有前景的方向，并通过进度报告支持与人类数学家的交互。
  • 多个工作智能体（worker agents）：并行执行证明搜索。
  • 无状态验证器（stateless verifier）：在数学命题被添加到事实图之前对其进行验证。
• 核心创新：共享事实图作为全局记忆管理机制。每个经验证的事实与其证明和逻辑依赖关系一同存储，使系统能够增量地构建长链条论证，同时保持共享证明状态的有序性。
• 开源状态：代码已开源在 https://github.com/frenzymath/Danus。

主要结果或产业意义： 通过在代数几何、奇点理论和组合学领域的六个研究级案例研究，Danus 展示了事实图记忆机制能够使其构建冗长且详细的数学证明。结果表明，基于事实图的编排为扩展面向长周期研究问题的数学推理智能体提供了一条有效路径。

为什么重要： 该工作直接应对了协调并行证明搜索与维护中间命题可靠性的核心挑战，为将 LLM 智能体应用于需要长时间推理和严格逻辑链条的数学研究领域提供了可行的系统框架。

局限与不确定性： 待核实（材料未明确讨论局限性，例如对复杂程度的上限、验证器的完备性、在不同数学分支的通用性等）。

可用于图书/PPT/简报的角度：

• “从数据记忆到结构记忆”：Danus 的事实图不仅是存储，更是一种可追溯依赖、可增量扩展的知识结构，适合说明笔记或记忆系统在复杂推理中的关键作用。
• “多智能体协作中的全局状态管理”：对比常见的无共享记忆的多智能体系统，Danus 展示如何解决信息碎片化与冲突问题。
• “数学证明自动化的一种新范式”：强调从“单一大模型直接生成证明”转向“编排多个小模型+验证器+记忆结构”的工程化思路。

英文标题： Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory

英文关键词： foundation-model, mathematical reasoning, fact-graph memory, orchestration system, LLM agent, proof search

原始材料：

• arXiv 论文：https://arxiv.org/abs/2607.06447v1
• 开放源代码：https://github.com/frenzymath/Danus