用事实图记忆协调多个智能体,解决数学研究级证明的长链条推理问题。
Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory

- 以共享事实图为全局记忆,统一管理中间结论与逻辑依赖。
- 在代数几何等6个高阶课题中成功构建复杂证明,验证了系统可扩展性。
- 适合研究型数学家与AI协同攻关长期难题,开源可复现。
基于大模型的数学推理智能体已开始挑战研究级问题,并在若干案例中促成开放问题的解决。然而,有效扩展和协调这些智能体仍具挑战,主要在于难以并行化证明搜索的同时保持中间命题的组织性与可靠性。本文提出Danus,一种以共享事实图为全局记忆机制的研究级数学推理协调系统。Danus由主控智能体负责规划与调度,多个工作智能体并行执行证明搜索,以及一个无状态验证器,在将数学命题纳入事实图前进行校验。每个经验证的事实均关联其证明过程与逻辑依赖,支持系统逐步构建长链条论证,同时维持共享证明状态的有序性。主控智能体定期总结进展,引导工作智能体聚焦有潜力的方向,并通过进度报告支持与人类数学家的交互。我们在代数几何、奇点理论和组合数学领域开展六个研究级案例研究,展示事实图记忆机制如何使Danus构建出详尽而复杂的数学证明。结果表明,基于事实图的协调策略为应对长周期研究问题提供了有效的数学推理扩展路径。Danus已在GitHub开源:https://github.com/frenzymath/Danus。
原文摘要 · Abstract (English)
Recent LLM-based mathematical reasoning agents have begun to tackle research-level problems and, in several cases, have contributed to the resolution of open problems. However, scaling and orchestrating such agents effectively remains challenging, due to the difficulty of coordinating parallel proof search while keeping intermediate claims organized and reliable. In this paper, we propose Danus, an orchestration system for research-level mathematical reasoning centered on a shared fact graph as a global memory-management mechanism. Danus consists of a main agent that performs planning and coordination, multiple worker agents that carry out proof search in parallel, and a stateless verifier that checks proposed mathematical claims before they are admitted into the fact graph. Each verified fact is stored together with its proof and logical dependencies, allowing the system to build long arguments incrementally while keeping the shared proof state organized. The main agent periodically summarizes the evolving proof state, redirects workers across promising directions, and supports interaction with human mathematicians through progress reports. We evaluate Danus through six research-level case studies in algebraic geometry, singularity theory, and combinatorics, illustrating how the fact-graph memory mechanism enables Danus to construct long, detailed mathematical proofs. Our results suggest that fact-graph-based orchestration provides an effective route toward scaling mathematical reasoning agents for long-horizon research problems. Danus is open source at https://github.com/frenzymath/Danus.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。