Source-linked AI summary
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
TL;DR
Danus addresses the challenge of coordinating parallel mathematical proof search while keeping intermediate claims organized and reliable. It orchestrates a main planner, parallel workers, a stateless verifier, and shared fact-graph memory. Across six research-level case studies, the system constructed long, detailed proofs, while the authors report that human mathematicians remained essential for guidance and review.
Problem
Scaling mathematical reasoning agents requires coordination and memory management because shared intermediate artifacts can become confusing, irrelevant, or erroneous.
Method
Danus uses a shared fact graph with a coordinating main agent, parallel proof-search workers, and a stateless verifier that admits verified claims with their dependencies.
Results
Across six research-level case studies, Danus constructed long and detailed proofs, decomposed difficult problems, repaired flawed dependencies, and produced mathematical manuscripts.
Takeaways & Limitations
Fact-graph orchestration provides an effective mechanism for extending LLM-based mathematical reasoning to long-horizon research problems while keeping human mathematicians involved.
Takeaways & Limitations
Danus sometimes needs human hints to find a proof route, and its generated papers require manual adjustment for citation and notation issues.
Abstract
from arXiv · showhide
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.
1 Introduction
Danus addresses the challenge of scaling research-level mathematical reasoning by coordinating parallel proof search through a shared fact graph. The system combines agent orchestration, human interaction, and case-study evaluation to support long mathematical proofs.
- Motivation: Existing mathematical reasoning agents use generate–verify–revise workflows, but scaling proof generation across more agents requires careful memory management and coordination.Poorly managed shared memory can confuse agents and propagate irrelevant or erroneous intermediate artifacts.
- Contribution: Danus uses a shared fact graph as global memory while a main agent coordinates multiple workers performing parallel proof generation.The graph organizes intermediate informally verified facts so the system can construct long, elaborated proofs.
- Human interaction: Danus supports human mathematicians through progress reports, high-level guidance, and paper-style exposition generated after the target statement is proved.The system also uses reports to consult advanced external reasoning systems when additional mathematical guidance is needed.
- Evaluation: The paper evaluates Danus on six research-level case studies in algebraic geometry, singularity theory, and combinatorics.The evaluation examines how fact-graph memory contributes to producing long, detailed, and correct proofs.
2 Methodology
Danus separates planning, parallel proof search, verification, and memory management across specialized agents and a shared fact graph. Workers submit claims for stateless verification, while the main agent periodically summarizes progress and redirects the search.
- Architecture: Danus coordinates a swarm of proof-search workers and a stateless verifier through a main agent, with the fact graph as the system’s sole source of truth.The main agent plans globally, workers conduct detailed searches, and the verifier alone determines which mathematics enters the graph.
- Workflow: Workers explore different lemmas, counterexamples, and toy examples in parallel, making longer multi-step arguments more tractable than single-line search.Parallel exploration broadens the search but requires the fact graph to combine contributions without interference.
- Fact graph: The fact graph is a directed acyclic graph whose nodes are verified facts and whose edges record logical dependencies between proofs.Workers retrieve relevant facts, submit dependency references, and add verified statements until the target theorem is represented.
- Fact graph: Compared with a single blueprint, the graph keeps worker contexts focused and lets separate lines of attack accumulate in one shared structure.This design supports parallel editing and preserves contributions from multiple proof directions.
- Reliability: The graph supports revocation by removing an incorrect fact and every fact that depends on it, directly or transitively.Revocation addresses erroneous references and, more rarely, conceptual confusion or flawed proofs; it was needed only very rarely in the reported runs.
- Memory: Danus separates verified truth from shared contextual memory, which stores plans, dead ends, examples, counterexamples, and consultation records.Workers also maintain private activity logs, while global memory is readable and writable by all workers and the main agent.
- Coordination: The main agent periodically reads logs, memory, and the fact graph, summarizes the evolving state, and obtains strategic guidance for the next search step.This cycle runs at regular intervals and helps identify stalled directions and reallocate effort.
- Verification: Workers repeatedly submit individual claims for verification and revise them under verifier feedback until they pass into the fact graph.The verifier is stateless but can inspect cited graph dependencies when checking a submission.
3 Results
Across six research-level case studies, Danus helped establish results spanning algebraic geometry, singularity theory, and combinatorics, including new optimal bounds, index theorems, asymptotics, and geometric characterizations. The cases also show varied human–system collaboration, from human-supplied strategies to fully autonomous proof construction and self-correction.
- Human–system collaboration: Human involvement ranged from supplying the strategy in the foliated bend-and-break case to providing brief hints, while Danus independently handled other decompositions, proof searches, and literature repair.In the Cartier-index case, Danus also repaired a writing-stage compression error through verification; another case involved correcting a flawed literature dependency.
- Optimal bend-and-break for foliations: Danus’s foliated bend-and-break case establishes the optimal constant r + 1 for rational curves tangent to a rank-r foliation.The resulting bound is H · Σ ≤ (r + 1) H · C − K_F · C, and the constant is optimal.
- Foliated global index theorem: The foliated index theorem proves a uniform index in dimension at most three and allows I ≤ 30 for canonical, non-algebraically-integrable foliations with B = 0.For coefficients in a DCC set Γ, some I = I(Γ) satisfies I(K_F + B) ∼ 0.
- Total Cartier indices in families: In families over a finite-type characteristic-zero base, every normal projective pure-dimensional fiber with rational singularities has total Cartier index dividing one common positive integer.This answers affirmatively the question of whether rational singularities suffice for boundedness in families.
- Factorial asymptotics of the Matryoshka numbers: The Matryoshka-number case proves the factorial asymptotic conjecture and rigorously encloses its constant in an interval of width less than 10^-9.The enclosure is obtained from explicit bounds and is meaningful because the constant has no known closed form.
- Weighted homogeneity via logarithmic vector fields: For isolated hypersurface germs, weighted homogeneity is shown equivalent to two geometric conditions involving logarithmic vector fields, extending the algebraic characterization with geometric ones.The result applies to reduced isolated hypersurface germs under the stated dimensional and irreducibility conditions.
4 Discussion
Danus combines specialized agents, verification, and a shared fact graph to scale mathematical proof search in width and depth. The experiments show substantial capabilities, while also revealing dependence on expert guidance and review, especially for difficult ideas and readable, faithful exposition.
- Writing faithfulness: Readable manuscripts remain difficult because compressing verified facts can introduce incorrect written reasoning even when the underlying results and route are correct.More rigorous writing can push the manuscript toward an unreadable fact-by-fact transcript, so the released versions retain a balance rather than a complete resolution.
- Architecture: Danus assigns planning, proof search, verification, and memory management to separate components, with the fact graph serving as the system’s source of truth.The verifier independently checks submitted text, while workers perform detailed derivations and the main agent coordinates globally.
- Verification: Verification reduces the human-checking bottleneck by rejecting and routing flawed writing back for machine repair before expert review.Results produced in one or two days typically took experts one or two weeks to check.
- Scaling in width: Seven workers built 3,157 verified facts in five days, demonstrating how the fact graph lets parallel contributions accumulate without colliding.Only 664 facts supported the theorem; the remainder recorded the breadth of the search.
- Scaling in depth: The fact graph extends reasoning beyond a single context window by allowing agents to handle small tasks while the system advances on a larger proof.Long chains depend on trusting previously verified facts, making verifier precision the architecture’s load-bearing assumption.
- Strengths: Across the experiments, Danus sometimes completed proofs with little or no human assistance and could automatically repair verifier-rejected manuscript drafts.Its reported strengths include sustained synthesis, long parallel searches, and unprompted decomposition into constructive and refutational routes.
- Limitations: The system still needs expert intervention when it cannot find the correct route, when references are flawed, and when notation, citations, or compressed exposition require correction.Reference errors can propagate into dependent facts until experts identify and revoke them.
5 Conclusion
Danus combines parallel proof search with fact-graph memory and verification to organize long mathematical arguments. Across six case studies, it constructed substantial proofs and supports the conclusion that fact-graph orchestration can extend mathematical reasoning agents to long-horizon research problems.
- Danus separates global planning, parallel proof search, and verification through a main agent, multiple workers, and a stateless verifier.Proposed claims are checked before admission to the shared fact graph.
- The fact graph stores each verified fact with its proof and logical dependencies, enabling incremental construction of long, organized mathematical arguments.
- Six case studies covered algebraic geometry, singularity theory, and combinatorics.
- Across the case studies, Danus constructed long and detailed proofs, decomposed difficult problems, repaired flawed dependencies, and converted verified fact graphs into manuscripts.Human input ranged from no mathematical guidance to a small number of high-level hints or corrections, while Danus carried out substantial proof construction in all cases.
- The results suggest that fact-graph orchestration can extend LLM-based mathematical reasoning agents to long-horizon research problems by organizing parallel local search into cumulative proof building.The paper also states that human mathematicians remain essential for choosing meaningful problems.