Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory
Jihao Liu, Guoxiong Gao, Zeming Sun, Bin Wu, Shurui Liu, Jiedong Jiang, Haocheng Ju, Leheng Chen, Ronnie Cheng, Xiping Zhang, Bin Dong
Why It Matters
What makes this one worth your time
This work is relevant for AI researchers interested in scaling mathematical reasoning capabilities, potentially aiding in solving complex research-level problems.
Danus orchestrates mathematical reasoning agents with a fact-graph memory to manage complex proofs.
Summary
The paper introduces Danus, a system for orchestrating mathematical reasoning agents using a shared fact graph for memory management. It features a main agent for planning, worker agents for parallel proof search, and a verifier for checking claims. The system is evaluated through case studies in algebraic geometry, singularity theory, and combinatorics, demonstrating its ability to construct long mathematical proofs.
Key contributions
- Introduction of Danus, a system for orchestrating mathematical reasoning agents.
- Implementation of a shared fact graph for global memory management in mathematical proofs.
- Evaluation through case studies in various mathematical domains.
Notable insights
- The use of a shared fact graph as a global memory-management mechanism is a novel approach to organizing and verifying intermediate claims in mathematical proofs.
- The orchestration of multiple agents with a stateless verifier allows for parallel proof search while maintaining reliability.
Possible limitations
- Not stated in the abstract
Abstract
arXiv:2607.06447v2 Announce Type: replace Abstract: 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.