Danus: orchestrating math-reasoning agents behind a verifier and a fact graph

What Danus is built to do

Danus orchestrates mathematical reasoning agents to search for proofs. A main agent decomposes a problem and steers a swarm of autonomous worker agents that do the proving, while a cold-start verifier decides what is true: a result becomes real only once it passes verification. Verified results accumulate in a content-addressed fact graph, which the system treats as its only source of truth. The audience is researchers in automated reasoning and AI-for-math who want a structured, auditable way to push large proof searches with language-model agents rather than a single model reasoning in one long context. Danus is a research engine with a paper and a technical report behind it, and it notably reports having solved a specific open problem on the branch documented in the README, which frames the ambition.

Separation of powers enforced by tools

The design's distinctive claim is that roles are enforced by construction, not by instructions. The main agent handles global planning and coordination, the workers carry out detailed proof search, the verifier is the sole authority on correctness, and the fact graph holds every verified result. Crucially, each agent has its own role-gated set of tools: the main agent has no fact-submit tool, so the agent that steers the search structurally cannot inject unverified mathematics into the graph, and the verifier writes nothing at all. Every claim enters truth through one cycle: a worker submits a statement with a proof citing existing facts, a fresh verifier instance accepts it into the graph or rejects it with repair hints, and the worker revises until it passes. Because the verifier is stateless and each worker draws only the facts it needs, the working context stays small even as the proof grows to many pages.

Running it on Codex or Claude Code

Danus ships in two variants that differ only in what runs the orchestrating main agent. On the codex branch, the workers, the verifier and the main agent all run on Codex, so you install nothing beyond Codex: the runtime is an AGENTS.md entry contract, MCP wiring in .codex/config.toml, and skills under .agents/skills. A separate main branch runs the orchestrator on Claude Code instead, with a CLAUDE.md, .mcp.json and .claude/skills runtime, sharing the same worker-verifier proof core. The Danus engine itself is a Python package requiring Python 3.10 or newer on Linux, wired to the agent host through MCP. The repository lays out the engine and its CLI verbs:

danus/                 the engine (installable Python package)
  core/                truth layer: content-addressed fact graph + typed memory + schema
  execution/           worker swarm: the autonomous per-worker round loop + scaffolding
  orchestration/       the `danus` CLI verbs (list/new/assign/start/status/stop)

Adoption is therefore a matter of choosing the branch matching your agent host and connecting the MCP configuration, rather than running a standalone binary; the README points to its architecture and operator documents for the exact steps.

What verification does and does not guarantee

The most important limitation is what the verifier is. Correctness in Danus means a claim passed a cold-start language-model verifier, not that it was checked by a formal proof assistant such as Lean. That is a real and useful gate, and the fact graph makes every accepted result traceable to the facts it depends on, but it is a model judging a model, so a verifier error can admit a wrong fact, and the guarantee is weaker than machine-checked formal proof. Beyond that, Danus is early, its package classifiers mark it alpha, it is Linux-only, and it depends on a capable agent host running Codex or Claude Code with the associated model costs of a whole swarm. It is a research system for pushing proof search, not a turnkey theorem prover you point at arbitrary problems.

Danus versus single-agent reasoning or formal provers

Two alternatives bracket it. A single model reasoning in one long context is the common approach, but it accumulates everything in one place, has no independent correctness gate, and degrades as a proof grows; Danus's difference is the separation of powers, a verifier that gates each fact and a graph that keeps the shared structure small and auditable. At the other extreme, a formal proof assistant like Lean gives machine-checked certainty, but it requires formalizing the mathematics and cannot freely explore in natural language; Danus trades that certainty for the ability to search broadly with language-model workers, accepting a model verifier instead of a formal kernel. Choose a formal prover when you need guaranteed correctness and can formalize; choose single-agent prompting for small problems; reach for Danus when you want structured, auditable, large-scale proof search with the honest caveat that its verifier is a model.

Apache-2.0 and current status

Danus is Apache-2.0 licensed, so it is freely reusable, and it is backed by an arXiv paper and a technical report, which is a reason to trust the method's description even as the code sits at an alpha stage. The last push was on 2026-08-27, and the release notes describe parallel codex and Claude Code variants that share one proof core, so the project is actively developed across both agent hosts. The README also reports a concrete run, thousands of verified facts and dependency edges in a real research search, which illustrates the scale it targets. Weigh it as research infrastructure: read the architecture and operator documents first, pick the branch for your agent host, and treat its verified facts as verifier-accepted rather than formally proven.

Editorial conclusion

Adopt Danus if you research automated mathematical reasoning and want structured, auditable, large-scale proof search with a swarm of agents, a verifier gate and a fact graph, on Codex or Claude Code with Python 3.10+ on Linux. Do not mistake its verification for formal proof: correctness means a language-model verifier accepted a claim, not that Lean checked it. Choose the codex or main branch to match your agent host, wire up the MCP configuration, and read the architecture document before a first run.

Frequently asked questions

Official sources

1. frenzymath/Danus on GitHub
2. Issues
3. License: Apache-2.0
4. README
5. Releases