A new open-source orchestration system called Danus tackles one of the harder problems in AI-assisted mathematics: keeping parallel proof-search agents from contradicting each other.
Published on arXiv (2607.06447) by the FrenzyMath team, Danus organizes mathematical reasoning around a shared "fact graph" — a global memory store where each entry must pass a stateless verifier before it is admitted. The system runs a main agent that plans and coordinates, multiple worker agents that search for proofs in parallel, and that verifier acting as gatekeeper. The main agent periodically summarizes the evolving proof state, redirects workers toward promising directions, and can surface progress reports for human mathematicians to review. The team evaluated Danus across six research-level case studies spanning algebraic geometry, singularity theory, and combinatorics.
The fact-graph approach directly addresses a real scaling bottleneck: when multiple agents work on a long proof simultaneously, unverified intermediate claims can silently corrupt downstream reasoning. By requiring each fact to carry its proof and logical dependencies before entering shared memory, Danus gives the system a foundation it can actually build on — rather than a pile of plausible-sounding steps that may not connect. That human-interaction layer also matters: it positions Danus as a collaborator rather than a black box, which is likely a prerequisite for adoption by working mathematicians.
For context, this sits alongside a small but growing cluster of LLM-based math systems — including DeepMind's AlphaProof — that are pushing into research-level territory rather than competition benchmarks. Danus is open-source at github.com/frenzymath/Danus, which is either a sign of genuine confidence in the approach or a smart move to get mathematicians stress-testing it for free.