Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory
Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel 2026-07-08 05:29 UTCglm-5.2pith:UTV2I2Z5record.jsonopen to challenge →
The pith
Shared fact-graph lets many AI agents build one long proof
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
The paper's central claim is that organizing parallel proof search around a shared, verified fact graph is the mechanism that makes long-horizon mathematical reasoning tractable for LLM agents. Workers contribute small verified facts that accumulate into dependency chains up to 54 levels deep; the fact graph keeps each worker's context small and focused while letting the system as a whole build arguments spanning hundreds of facts. The controlled comparison in Section 3.6 isolates this claim: the same worker and verifier models that failed under single-line orchestration succeeded under fact-graph orchestration, suggesting the architecture, not the underlying model, drove the difference.
What carries the argument
The fact graph is a DAG of verified mathematical statements with edges recording proof dependencies. Around it sit three agent roles: a main agent (built on a coding-agent backbone) that reads global state and redirects workers, multiple worker agents (inherited from the predecessor system) that each prove one local claim at a time, and a stateless verifier that checks every submission before it enters the graph. The verifier can follow citations into the existing graph, and the graph supports revocation: if a fact is later found wrong, it and everything depending on it are removed.
If this is right
- If the architecture generalizes, research-level proof search could scale by adding more workers and longer run times rather than waiting for stronger base models, shifting the bottleneck from model capability to orchestration and verification.
- The fact-graph pattern could apply beyond mathematics to any domain where long chains of individually checkable steps must be assembled by parallel agents, such as formal software verification or multi-step scientific argumentation.
- The human's role shifts toward strategic intervention at impasse points and final expert review, suggesting a collaborative model where AI handles routine proof construction and humans supply missing ideas.
- The paper's acknowledgment that the system cannot invent fundamentally new ideas beyond what its models propose, and circles when no path exists, sets a concrete boundary on what orchestration alone can achieve.
Load-bearing premise
The entire architecture rests on the verifier being highly precise: if it accepts flawed proofs even at a low rate, errors compound through dependency chains that can reach 54 facts deep, and the accumulated graph becomes unreliable. The verifier is not formally certified; its reliability is empirical, scoped to the tested problems, and the paper acknowledges it occasionally accepts proofs with skipped steps or flawed cited references.
What would settle it
A single verified fact deep in a dependency chain that is later found to be wrong, causing cascading revocation that breaks the target theorem, would show that the verifier's precision is insufficient for the chain lengths the architecture requires.
read the original 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper introduces Danus, an orchestration system for research-level mathematical reasoning built around a shared fact graph that serves as a global memory for multiple parallel worker agents. The architecture consists of a main agent (Claude Code with Claude Opus 4.8) handling planning and coordination, multiple worker agents (Rethlas-based, running GPT-5.5) performing proof search, and a stateless verifier that checks claims before admission to the fact graph. The system is evaluated through six case studies in algebraic geometry, singularity theory, and combinatorics, each producing research-level mathematical results. The paper also provides a controlled comparison (Section 3.6) where Danus solved a problem that Rethlas failed on three times with the same underlying models. The code is open source.
Significance. The paper makes a genuine architectural contribution to the growing literature on LLM-based mathematical reasoning agents. The fact-graph design—where verified facts form a DAG that workers can reference without re-derivation—is a clean and well-motivated solution to the memory management problem in multi-agent proof search. The open-source release and the six case studies, several of which produced publishable mathematical results, demonstrate the system's practical capability. The controlled comparison in Section 3.6 (Rethlas vs. Danus on the same prompt) is the most informative experiment, isolating the contribution of orchestration from the underlying models. The paper is commendably transparent about human input in each case study and about the system's limitations, including verifier failures and the need for human hints. The honest reporting of failures (revocation in Section 3.5, incomplete Lemma 8.7 in Section 3.6) is a strength.
major comments (4)
- §4.3: The paper explicitly identifies verifier precision as 'the load-bearing assumption of the architecture' and states the verifier 'produced essentially no false positives on the problems we tested.' However, this claim is supported only by the six case studies themselves, with no independent or systematic measurement of the false-positive rate. The architecture requires near-zero per-fact error rates because errors compound through dependency chains—Section 3.6 reports chains up to 54 facts deep with 664 supporting facts. The paper's own evidence (revocation in §3.5, incomplete Lemma 8.7 in §3.6, the dimension misreading in §3.3) shows the verifier does miss errors that human experts subsequently catch. The authors should either (a) provide a quantitative estimate of the false-positive rate, even a rough one based on the number of verifier errors found by human review across all case
- §3.6 and §4.3: The controlled comparison between Danus and Rethlas is the strongest piece of evidence for the architectural claim, but it is limited to a single problem. The paper's central claim—that fact-graph orchestration enables longer and more reliable proofs than simpler agent systems—rests heavily on this one data point. Expanding the controlled comparison to at least 2-3 problems, or providing a clearer explanation of why this single comparison is representative, would substantially strengthen the central claim. At minimum, the authors should acknowledge this limitation explicitly in Section 4.5 and discuss what additional evidence would be needed to generalize the claim.
- §3: The evaluation rests entirely on case studies with substantial variation in human input (from none in §3.4 to multiple interventions in §3.2), problem domain, and fact-graph scale (100 to 3,157 facts). While each case study is individually informative, the absence of any systematic comparison across these dimensions makes it difficult to assess which components of the architecture are load-bearing. For instance, it is unclear whether the main agent's GPT-5.5-pro consultations, the number of workers, or the summarization frequency materially affect outcomes. The authors should discuss in Section 4 what can and cannot be concluded from the case study evidence, and ideally identify which architectural choices are essential versus incidental. A table summarizing the key parameters of each case study (number of workers, runtime, fact-graph size, number of human interventions, verifier rev
- §2.5: The verifier is described as 'the sole authority on correctness,' yet the paper documents multiple cases where human experts found errors the verifier missed (§3.3, §3.5, §3.6). This is not necessarily a contradiction—the paper acknowledges human review as a separate stage—but the framing in §2.5 could mislead readers about the verifier's actual reliability. The authors should clarify in §2.5 that the verifier is the sole automated authority, with human expert review serving as an additional layer, and that the verifier's precision is empirical rather than formally certified.
minor comments (7)
- §2.5: The phrase 'essentially no false positives' is vague. How many false positives were observed in total across all case studies? A concrete count would help readers calibrate the claim.
- §3.6, footnote 1: The reference [11] is listed as 'in preparation' with a note that the footnote will be replaced by a citation. This should be resolved before publication.
- §2.4: The choice of Claude Code with Claude Opus 4.8 for the main agent is stated as the result of evaluating several coding agents, but no details of this evaluation are given. A brief description of the evaluation criteria and results would help readers understand the design choice.
- §4.1: The paper mentions 'Fable 5 from Anthropic' as not yet evaluated. This reference may become outdated; consider removing or noting it as preliminary observations.
- §2.2, Figure 2: The fact graph visualization is informative but the caption could clarify what 'dependency depth' means operationally (distance from a leaf fact to the node?).
- §3.3: The misreading of 'dimension ≥ 3' as 'dimension > 3' from a PDF is an interesting failure mode that could be discussed more explicitly in §4.5 as a limitation of the literature retrieval pipeline.
- The paper uses model names (GPT-5.5, GPT-5.5-pro, Claude Opus 4.8) that may not be widely recognized. Brief context or citations for these models would help readers outside the specific community.
Simulated Author's Rebuttal
We thank the referee for a careful and constructive report. The referee recognizes the architectural contribution, the value of the controlled comparison, and the transparency of the case studies. The four major comments all concern the strength of the evidence for our central claims—verifier precision, generalizability of the controlled comparison, systematicity of the evaluation, and framing of the verifier's authority. We agree with the substance of all four and will revise accordingly. Below we address each in turn.
read point-by-point responses
-
Referee: §4.3: The claim that the verifier 'produced essentially no false positives' is supported only by the six case studies, with no independent or systematic measurement. The architecture requires near-zero per-fact error rates because errors compound through dependency chains (up to 54 deep, 664 supporting facts). The paper's own evidence (revocation in §3.5, incomplete Lemma 8.7 in §3.6, dimension misreading in §3.3) shows the verifier does miss errors. The authors should either (a) provide a quantitative estimate of the false-positive rate, or (b) qualify the claim.
Authors: The referee is correct that the claim in §4.3 is not supported by a systematic, independent measurement of the false-positive rate, and that the phrasing 'essentially no false positives' overstates what our evidence establishes. We will revise. Specifically, we will (i) replace the qualitative claim with a quantitative accounting: across all six case studies, the fact graph accumulated a total of approximately 4,400 verified facts (100 + 63 + 784 + 687 + 3,157 + the §3.1 total), of which human expert review identified verifier errors in a small number of cases—the flawed reference in §3.5 (affecting 23 revoked facts), the incomplete Lemma 8.7 in §3.6, and the dimension misreading in §3.3 (which was a reference-extraction error rather than a verifier error per se). We will present this as a rough per-fact error estimate with appropriate caveats about the denominator and the non-uniform depth of human review. (ii) We will explicitly state that this rate is empirical, not formally certified, and that it is measured on the specific problem classes in our case studies, not on an independent benchmark. (iii) We will add the discussion the referee requests about error compounding: at chain depths of 50+, even a per-fact error rate of, say, 0.5% would imply substantial cumulative risk, which is precisely why human expert review remains an essential layer. We acknowledge that we cannot provide a rigorous confidence interval on the false-positive rate from six case studies with non-uniform review depth; this is a genuine limitation, and we will state it as such. revision: yes
-
Referee: §3.6 and §4.3: The controlled comparison between Danus and Rethlas is limited to a single problem. The central claim—that fact-graph orchestration enables longer and more reliable proofs—rests heavily on this one data point. The authors should expand to 2-3 problems, or explain why this single comparison is representative, and acknowledge the limitation in §4.5.
Authors: We agree that a single controlled comparison is insufficient to establish the general claim and that this limitation should be stated explicitly. We will add a paragraph to §4.5 acknowledging that the controlled comparison in §3.6 is a single data point and that generalizing the claim—fact-graph orchestration enables longer and more reliable proofs than simpler agent systems—requires additional controlled experiments across multiple problems and domains. We will also explain why this single comparison is at least informative: Rethlas and Danus ran the same worker and verifier models on the same prompt, so the difference in outcome (three failed runs versus a complete verified solution) isolates the orchestration layer. However, we agree this does not establish representativeness. Regarding the request to expand to 2-3 problems: we are unable to run additional controlled comparisons before the revision deadline, as each case study required days of compute and weeks of expert review. We will state this as a standing limitation and identify it as the most important direction for future work. We will also note that the six case studies provide indirect corroborating evidence—Danus produced verified proofs at scales (hundreds to thousands of facts, chains up to 54 deep) that Rethlas's single-blueprint architecture was not designed to support—but we agree this is not a substitute for direct controlled comparisons. revision: partial
-
Referee: §3: The evaluation rests entirely on case studies with substantial variation in human input, problem domain, and fact-graph scale. No systematic comparison across these dimensions makes it difficult to assess which components are load-bearing. The authors should discuss what can and cannot be concluded, identify essential vs. incidental architectural choices, and provide a table summarizing key parameters of each case study.
Authors: This is a fair and important point. We will add the requested summary table to §3, with columns for: case study, number of workers, runtime, fact-graph size (total verified facts), supporting closure size, maximum dependency depth, number of human interventions (beyond common input), number of revoked facts, and verifier errors found in review. This will make the variation across case studies visible at a glance. We will also add a subsection to §4 discussing what can and cannot be concluded from the case study evidence. Specifically, we can conclude that the fact-graph architecture is capable of supporting proofs at the scales observed and that the system produced correct results across diverse domains with varying levels of human input. We cannot conclude from this evidence alone which specific architectural choices are essential versus incidental—e.g., the number of workers, the ratio of high to xhigh effort, the summarization frequency, or the role of GPT-5.5-pro consultations—because these were not varied systematically. We will state this explicitly and identify controlled ablation studies over these parameters as a key direction for future work. We agree that the current manuscript does not support strong claims about the necessity of individual components, and we will adjust the language accordingly. revision: yes
-
Referee: §2.5: The verifier is described as 'the sole authority on correctness,' yet the paper documents multiple cases where human experts found errors the verifier missed. The framing could mislead readers about the verifier's actual reliability. The authors should clarify that the verifier is the sole automated authority, with human expert review as an additional layer, and that the verifier's precision is empirical rather than formally certified.
Authors: The referee is right that the current framing in §2.5 is imprecise and could mislead. The phrase 'sole authority on correctness' is meant to convey an architectural fact—that within the system's automated loop, only the verifier can admit a fact into the fact graph, and neither the main agent nor the workers can do so—but it does read as a claim about the verifier's reliability, which the case studies show is not perfect. We will revise §2.5 to clarify that the verifier is the sole automated authority on correctness within the system, that human expert review serves as an additional and essential layer, and that the verifier's precision is empirical (observed on our case studies) rather than formally certified. We will cross-reference the revised quantitative accounting from §4.3 and the specific cases (§3.3, §3.5, §3.6) where human review caught errors the verifier missed. This change is consistent with the paper's existing honesty about failures; it is a correction of framing, not of substance. revision: yes
- We cannot provide additional controlled comparisons (Danus vs. Rethlas on 2-3 additional problems) within the revision timeframe, as each requires days of compute and weeks of expert review. We will acknowledge this as a limitation and identify it as the primary direction for future work.
- We cannot provide a rigorous confidence interval on the verifier's false-positive rate from six case studies with non-uniform depth of human review. We will provide a rough quantitative accounting with appropriate caveats, but a formally rigorous estimate would require a dedicated benchmark with systematic expert review of every fact, which is beyond the scope of this revision.
Circularity Check
Self-citations exist but are not load-bearing for the central architectural claim; no prediction reduces to its inputs by construction.
full rationale
The paper builds its workers and verifier from Rethlas [21] (overlapping authors) and cites its own case-study outputs [29], [30], [31], [34], [35], [11] (overlapping authors), but none of these self-citations create a circular derivation. The central claim—that fact-graph orchestration enables longer verified proofs than single-line agent systems—is tested independently in the controlled comparison of Section 3.6, where Rethlas and Danus run the same worker and verifier models on the same prompt. Rethlas failed three times; Danus produced a verified solution. This comparison isolates the orchestration layer and does not reduce to a self-citation. The verifier's reliability (Section 4.3) is stated as an empirical observation ('produced essentially no false positives on the problems we tested'), not derived from the case study outputs; the paper openly reports verifier failures (revocation in §3.5, incomplete Lemma 8.7 in §3.6). The case-study papers sharing authors with Danus are outputs of the system, not fitted inputs repackaged as predictions. No parameter is fitted to a subset of data and then 'predicted' on related data. No uniqueness theorem is invoked. The verifier reliability concern is a correctness risk (unmeasured false-positive rate across deep dependency chains), not a circularity issue. The minor self-citations (Rethlas for workers/verifier, Matlas for literature search) are standard prior-work references and do not raise the circularity score above 2.
Axiom & Free-Parameter Ledger
free parameters (4)
- Number of workers per project =
3-9
- Worker effort levels =
high and xhigh (split roughly evenly)
- Main agent consultation frequency with GPT-5.5-pro =
at most once per hour
- Summary interval =
every one to two hours
axioms (4)
- domain assumption The stateless verifier reliably checks mathematical claims with near-zero false positives
- domain assumption Workers can reliably identify and cite dependencies on existing facts
- domain assumption The fact graph DAG structure correctly captures logical dependencies
- domain assumption Cited references are correct
invented entities (2)
-
Fact graph
independent evidence
-
Main agent role
independent evidence
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.