Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory

Danus orchestrates mathematical reasoning agents with fact-graph memory. A main agent (Claude Code) steers a swarm of autonomous codex workers that prove; a cold-start verifier is the sole authority on correctness: a result becomes real only once it passes. Verified results accumulate in a content-addressed fact graph — the system's only source of truth — and a strategy loop (a strong reasoning model) decomposes the problem and steers the swarm. When you have the answer, Danus renders it into a human report or a publishable LaTeX paper.

Danus builds on the worker–verifier core of our earlier system Rethlas (arXiv:2604.03789). The paper and the technical report tell the full story: the system, six research-level case studies it resolved, and what we learned along the way.

See ARCHITECTURE.md for the layered design and the map of every module.

How it works

The design follows a strict separation of powers: the main agent performs the global planning and coordination, the workers carry out the detailed proof search, the verifier is the sole authority on correctness, and the fact graph holds every verified result and is the system's only source of truth.

Each kind of agent carries out its role through its own skills and its own role-gated set of tools, so the separation is enforced by construction, not by prompts: the main agent has no fact_submit (the agent that steers the search structurally cannot introduce unverified mathematics into the fact graph), and the verifier writes nothing at all.

Every claim enters truth through one cycle:

A worker typically focuses on one claim at a time — a lemma, a counterexample, a toy example — rather than an entire proof. It repeatedly submits the claim with a supporting proof and revises it under the verifier's feedback until it passes, at which point the claim enters the fact graph as a fact, with the facts its proof depends on as its incoming edges. The verifier is stateless: a fresh instance judges each submission and retains nothing afterwards. Because each worker draws on only the facts it needs for its current claim and submits one fact at a time, the working