看看Danus怎么用事实图记忆帮多个推理智能体协作解数学难题，还能和数学家互动。
Danus是一个基于事实图记忆的协调系统，旨在提升研究级数学推理能力。系统包含一个主智能体进行规划和协调，多个工作智能体并行执行证明搜索，以及一个无状态验证器检查数学主张。每个验证的事实连同证明和逻辑依赖存储在事实图中，构建递增的长期论证。在代数几何、奇点理论和组合学的六个研究级案例中，Danus成功生成长而详细的数学证明。
Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory
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.