Danus Orchestrates AI Agents for Complex Math Proofs

Researchers have introduced Danus, an orchestration system designed to scale and coordinate large language model (LLM)-based agents for tackling complex mathematical reasoning problems. The core of Danus is a shared fact graph that acts as a global memory, organizing intermediate claims and proofs. The system comprises a main agent for planning, multiple worker agents for parallel proof search, and a stateless verifier that validates claims before they are added to the fact graph. This architecture allows Danus to construct long, detailed mathematical proofs incrementally, maintaining an organized and reliable shared proof state. Evaluated across six research-level case studies in various mathematical fields, Danus demonstrates its effectiveness in scaling mathematical reasoning for long-horizon problems.