Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory

🕒 Published (v1): 2026-07-07 16:11 UTC · Source: Arxiv · link

Why this paper was selected

Fact-Graph Memory for orchestrating multi-agent mathematical reasoning — structured memory for long-horizon agents

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

Danus is a multi-agent orchestration system for research-level mathematics that coordinates parallel proof-search workers through a shared fact graph — a DAG of verifier-approved facts with explicit logical dependencies — as its sole source of truth. A main planning agent (Claude Code + Claude Opus 4.8) allocates work, periodically consults GPT-5.5-pro for strategy, and synthesizes progress, while a stateless verifier gatekeeps all entries into the graph. Six research-level case studies in algebraic geometry, singularity theory, and combinatorics demonstrate that the approach enables construction of long, multi-step proofs where GPT-5.5-pro alone produces no meaningful result.

Problem

Scaling LLM-based mathematical reasoning agents beyond a single reasoning thread is non-trivial: naively spawning many agents on the same problem causes shared memory to accumulate irrelevant or erroneous intermediate artifacts, confuses agents with unbounded context, and degrades proof reliability. Existing multi-agent math systems (Aletheia, Rethlas, QED, ProofCouncil) use role diversity (generator/verifier/reviser) but do not systematically scale the number of agents doing parallel proof generation.

Method

Danus couples three layers under a strict separation of powers:

1. Fact graph — a DAG where each node is a (statement, proof, dependency-set) triple accepted by the verifier. It is the system's only source of truth. Workers search the graph via fact retrieval (Matlas theorem engine) and submit one claim at a time; the verifier, which may read cited facts for dependency checking, either accepts (adding to the graph) or rejects with repair hints. Revocation propagates deletions transitively when an error is found in a cited fact.

2. Worker swarm — 3–9 parallel Rethlas generation agents running at two reasoning-effort levels ("high" and "xhigh" via Codex) to diversify shallow/deep exploration. Each worker maintains a private local memory (activity log) and reads/writes shared global memory (plans, dead ends, constructed examples).

3. Main agent — built on Claude Code with Claude Opus 4.8 (selected empirically over Codex and OpenClaw variants for navigating large evolving log corpora). It runs a strategy loop every 1–2 hours: reads worker logs and the full fact graph, produces a conservative progress summary (prohibitions against numerical estimation or premature "complete" claims), consults GPT-5.5-pro (at most once per hour) for strategic guidance, then re-assigns workers. It terminates only when the target theorem appears as a verified fact.

Paper writing treats the manuscript as a new artifact: the linear prose is re-verified end-to-end, since stitching facts into prose creates new mathematical content at the seams. When the manuscript exceeds a single-pass context, the main agent decomposes it into self-contained sections each culminating in a named result.

Key Contributions

• Fact-graph memory as a scalable, dependency-tracking global shared state for multi-agent proof construction.
• Revocation mechanism that propagates invalidation transitively through the DAG.
• Separation of planning and proving: main agent cannot introduce unverified mathematics into the fact graph.
• Conservative summarization discipline: explicit prohibitions prevent optimistic over-reporting to human experts and upstream LLM consultants.
• End-to-end re-verification of the prose manuscript rather than relying on fact-level verification transfer.
• Six research-level case studies with explicit accounting of human input beyond the "common input" baseline.

Results

• Baseline: GPT-5.5-pro web interface produced no meaningful result on any of the six problems when posed directly.
• Case study — optimal bend-and-break for foliations: 5 parallel workers; 63 verified facts; 239 failed paths. Result: optimal constant for rational curves tangent to a rank-\(r\) foliation is \(r+1\), settling a previously open problem.
• Case study — matroid tangent classes (Section 3.6): 3,157 verified facts; 8,616 dependency edges; DAG depth up to 54. Distinct clusters in the graph correspond to separate lines of attack, including a conditional scaffold ultimately unused in the final proof and an independent re-derivation of a Chern-number bound.
• Results are qualitative case studies, not benchmark accuracy numbers; no ablation data is reported in the provided text.

Limitations

• No quantitative ablation or controlled benchmark (e.g., MATH, MiniF2F, Putnam) — evaluation is entirely via six expert-selected open problems, making it hard to measure marginal gain over Rethlas alone.
• Verifier produces rare false positives when proofs contain skipped steps or cite erroneous external references; these require downstream review to catch.
• Human input is still required for each problem: initial problem statement, seed references, final manuscript review, and occasional mid-run mathematical redirection.
• Domain coverage limited to algebraic geometry, singularity theory, and combinatorics; generalization to other mathematical fields is undemonstrated.
• Main agent consults GPT-5.5-pro (a closed external model) for high-level strategy, creating a dependency on a non-open system.

Relevance to Agentic AI / LLM Agents

Danus is a concrete instantiation of how structured global memory (the fact DAG) can replace unstructured shared context in multi-agent systems — a general principle directly applicable to any long-horizon agentic task where multiple agents must build on each other's outputs without mutual interference. The strict verifier-as-gatekeeper pattern (stateless oracle with sole write authority over shared state) is an architectural primitive that addresses the trust and consistency problems that arise when scaling agent counts. The separation of planning from execution, with the planner barred from writing to the truth store, offers a reusable pattern for safe orchestration of autonomous agents. The paper also provides rare transparency into human–agent collaboration costs, explicitly recording what human input was required per case, which is valuable ground truth for the field.