Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory

• URL: http://arxiv.org/abs/2607.06447v2
• Date: Wed, 08 Jul 2026 12:23:39 GMT
• Title: Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory
• Abstract summary: Danus is an orchestration system for research-level mathematical reasoning centered on a shared fact graph.<n>Each verified fact is stored together with its proof and logical dependencies, allowing the system to build long arguments.
• Score: 7.10978537067254
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent LLM-based mathematical reasoning agents have begun to tackle research-level problems and, in several cases, have contributed to the resolution of open problems. However, scaling and orchestrating such agents effectively remains challenging, due to the difficulty of coordinating parallel proof search while keeping intermediate claims organized and reliable. In this paper, we propose Danus, an orchestration system for research-level mathematical reasoning centered on a shared fact graph as a global memory-management mechanism. Danus consists of a main agent that performs planning and coordination, multiple worker agents that carry out proof search in parallel, and a stateless verifier that checks proposed mathematical claims before they are admitted into the fact graph. Each verified fact is stored together with its proof and logical dependencies, allowing the system to build long arguments incrementally while keeping the shared proof state organized. The main agent periodically summarizes the evolving proof state, redirects workers across promising directions, and supports interaction with human mathematicians through progress reports. We evaluate Danus through six research-level case studies in algebraic geometry, singularity theory, and combinatorics, illustrating how the fact-graph memory mechanism enables Danus to construct long, detailed mathematical proofs. Our results suggest that fact-graph-based orchestration provides an effective route toward scaling mathematical reasoning agents for long-horizon research problems. Danus is open source at https://github.com/frenzymath/Danus.

Related papers

• VALG: An Agentic System for ML Theory Research [35.29223690479372]
  We develop VALG, an agentic system that combines multi-level Verification, Adaptive formulation of Learning-theory problems, and Graph-structured proof development.<n>We evaluate VALG on nine subproblems from five COLT 2026 open problems.
  arXiv  Detail & Related papers  (2026-08-13T10:23:11Z)
• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilot is a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research.<n>MathCoPilot unifies three core capabilities: an interactive proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and topic-driven paper retrieval and automated formalization into a verified Lean knowledge base.
  arXiv  Detail & Related papers  (2026-07-16T05:22:40Z)
• From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
  We argue that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents.<n>We provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis.
  arXiv  Detail & Related papers  (2026-07-08T17:46:36Z)
• MechMath Agent Team: LLM Driven Agents for Mathematical Research [17.23955320294417]
  MechMath Agent Team (MMAT) is a large language model driven agent designed to serve as a co-pilot throughout the full cycle of mathematical research.<n>We design a tripartite Harness Architecture that decouples system responsibilities into Control, Execution, and Augmentation planes.<n>We evaluate MMAT on open problems in Number Theory, Algebraic Complexity Theory, Differential Algebra, Operator Algebra, and Inequalities.
  arXiv  Detail & Related papers  (2026-07-05T16:37:40Z)
• Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery [3.9943798586374784]
  This survey provides a unified account of the field's evolution.<n>We organize the landscape along four axes: (i) informal reasoning over text and diagrams, spanning MWP solving, multimodal geometry, and RLMs; (ii) formal reasoning in proof assistants, including autoformalization, tactic prediction, compiler-guided repair, and proof search; (iii) mathematical discovery, where systems propose constructions, improve bounds, or assist attacks on open problems; and (iv) the inference and training-time techniques, including CoT prompting, tool use, process reward models, and VLVR, that increasingly connect generation with
  arXiv  Detail & Related papers  (2026-06-07T16:50:07Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization.<n>Four contract-scoped agents construct, audit, prove, and repair this blueprint.<n>We evaluate LeanMarathon on two recent research papers spanning four Erds problems.
  arXiv  Detail & Related papers  (2026-06-03T20:09:39Z)
• Discovering mathematical concepts through a multi-agent system [3.820195410658766]
  We present a new multi-agent model for computational mathematical discovery.<n>Our system, conceived with research in mind, poses its own conjectures and then attempts to prove them.<n>We claim that the optimisation of the right combination of local processes can lead to surprisingly well-aligned notions of mathematical interestingness.
  arXiv  Detail & Related papers  (2026-03-04T19:13:36Z)
• Towards Autonomous Mathematics Research [48.29504087871558]
  We introduce Aletheia, a math research agent that iteratively generates, verifies, and revises solutions end-to-end in natural language.<n>Specifically, Aletheia is powered by an advanced version of Gemini Deep Think for challenging reasoning problems.<n>We demonstrate Aletheia from Olympiad problems to PhD-level exercises and most notably, through several distinct milestones in AI-assisted mathematics research.
  arXiv  Detail & Related papers  (2026-02-10T18:50:15Z)
• Stationary Processes, Wiener-Granger Causality, and Matrix Spectral Factorization [0.3626013617212666]
  We provide a detailed overview of Granger causality, trace its historical development, and explore how recent computational advancements can enhance its application in various fields.<n>We discuss potential future directions for the method, particularly in the context of largescale data analysis.
  arXiv  Detail & Related papers  (2024-12-25T13:29:39Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)
• GeoQA: A Geometric Question Answering Benchmark Towards Multimodal Numerical Reasoning [172.36214872466707]
  We focus on solving geometric problems, which requires a comprehensive understanding of textual descriptions, visual diagrams, and theorem knowledge. We propose a Geometric Question Answering dataset GeoQA, containing 5,010 geometric problems with corresponding annotated programs.
  arXiv  Detail & Related papers  (2021-05-30T12:34:17Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.