Researchers propose Danus, an orchestration system for research-level mathematical reasoning that utilizes a shared fact graph as a global memory-management mechanism. The system coordinates a main agent for planning and multiple worker agents performing parallel proof search, using a stateless verifier to check claims before they enter the graph.
- Danus stores verified facts with their proofs and logical dependencies 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.
- Evaluation through six research-level case studies in algebraic geometry, singularity theory, and combinatorics illustrates how the fact-graph mechanism enables the construction of long, detailed mathematical proofs.
The results suggest that fact-graph-based orchestration provides an effective route toward scaling mathematical reasoning agents for long-horizon research problems.