frenzymath/danus

Danus is a Python system that coordinates a team of AI agents to work through mathematical proofs together and keep track of what has actually been verified as true. A main agent, built on Claude Code, plans the overall strategy and directs a group of worker agents, each built on the codex tool, that attempt to prove individual pieces of a larger problem, such as a single lemma or example. The key design choice is a strict separation of roles. Workers submit a claim along with a supporting proof, and a separate verifier agent checks it and either accepts or rejects it with feedback for revision. Only the verifier can decide whether something counts as proven, and it does not keep memory between checks, judging each submission fresh. Once a claim passes, it is added to a shared fact graph, a structure that records every verified result and which earlier facts it depended on. The main agent itself has no ability to add unverified claims to this fact graph, so the separation between planning and truth checking is built into the system rather than relying on instructions alone. Because each worker only needs to load the specific facts relevant to its current claim, the amount of context any single agent has to hold stays manageable even as the overall proof grows very large. The README shows an example run that produced over 3,100 verified facts connected by more than 8,600 dependencies. Once a problem is solved, Danus can turn the accumulated fact graph into a written report or a formatted LaTeX paper. Setup involves running a bootstrap script to install dependencies, copying example configuration files and filling in your own API keys, starting a verification service, and then connecting Claude Code to the project directory. The system relies on the user's own API keys throughout and is licensed under Apache 2.0. Danus builds on an earlier project by the same team called Rethlas.