{"id":"1f582bdb-5307-4b1e-ba38-17f9b02529f4","arxiv_id":"2607.06447","paper_version":2,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.5,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"Danus uses a main planner, parallel workers, and a shared verified fact graph to construct long research-level mathematical proofs across six case studies.","lead":"Danus coordinates multiple LLM proof agents with a shared fact graph that stores only verifier-checked claims and their dependencies. It offers a concrete way to scale AI systems that attempt research-level mathematics over long horizons.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"The central claim rests on informal LLM verification of long dependency chains, with residual gaps already admitted in the case studies.","rationale":"The paper is a careful systems contribution: open-source release, transparent human-input accounting, and a clear architectural separation of planning, parallel search, and verification. The reader’s weakest assumption is exactly the load-bearing one—the reliability of the non-formal verifier for deep fact graphs. I agree with the CONDITIONAL verdict and the medium correctness risk; no stronger downgrade is warranted because the authors already document residual gaps, do not claim formal guarantees, and show that human experts ultimately checked the manuscripts. The concrete test above would settle whether the concern is merely theoretical or already material at the scale of the largest case study. If the sample re-verification is clean, the claim strengthens; if not, the fact-graph premise needs tighter verification or formal backends before the scaling claim can be taken as demonstrated rather than promising.","tokens_in":19126,"tokens_out":583,"duration_ms":7098,"concrete_test":"Independently re-verify a random sample of 30–50 non-leaf facts from the §3.6 fact graph (depth ≥10, including the supporting closure of the Chern-number bound and the integral lift), using a second LLM verifier or human experts blind to the original accept/reject labels; if more than ~5% are found to contain skipped steps, citation errors, or incomplete justifications, the sole-source-of-truth premise fails at the scale of the headline claim.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The strongest claim is that fact-graph orchestration is an effective route to long-horizon research-level proofs, evidenced by six case studies. That claim is load-bearing on the premise that the stateless LLM verifier is reliable enough for the fact graph to be the sole source of truth, so later workers may safely depend on earlier facts without re-checking them (§2.5, §4.3). The paper itself reports that the verifier can accept skipped steps and erroneous literature citations, that revocation was needed after a flawed reference in §3.5, and that the §3.6 manuscript still has an incomplete justification for Lemma 8.7 even after human review. In the largest run the theorem rests on 664 supporting facts in chains up to depth 54; any systematic false-positive rate, however small, compounds along those chains. The case studies therefore demonstrate impressive orchestration and human–AI collaboration, but they do not yet establish that the accumulated proofs are independently reliable at the scale claimed. The reader correctly flags this; the residual risk is not merely residual manuscript polish but the soundness of the shared memory that the whole architecture treats as truth.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper introduces Danus, an orchestration system for research-level mathematical reasoning built around a shared fact graph (a DAG of verifier-checked claims with proofs and dependency edges). A main agent plans and coordinates; multiple worker agents explore proof search in parallel; and a stateless LLM verifier is the sole gate for admitting facts. Global and local memory record plans, dead ends, and consultations. The system is evaluated through six research-level case studies in algebraic geometry, singularity theory, and combinatorics, with reported fact counts, dependency depths, human-input logs, and a limited comparison to Rethlas and GPT-5.5-pro. The authors argue that fact-graph memory enables long-horizon parallel proof construction while keeping intermediate state organized, and they release the system as open source.","tokens_in":19422,"tokens_out":1340,"duration_ms":29348,"significance":"If the systems claims hold, Danus is a concrete advance over single-line generate–verify–revise agents (including Rethlas) for long research proofs: it shows how to scale test-time compute in both width (parallel workers) and depth (trusted dependency chains) without collapsing shared state. Strengths that should be credited include: a clearly specified architecture with separation of planning, search, and verification; open-source release; unusually detailed case documentation (fact counts, depths up to 54, human-input inventories); and honest reporting of residual gaps and human interventions. The six case studies, several of which produced independent arXiv manuscripts, are strong existence evidence that such orchestration can contribute to research-level mathematics under human–AI collaboration.","major_comments":[{"comment":"§2.5 and §4.3 make the reliability of the stateless LLM verifier load-bearing: the fact graph is the sole source of truth, and later workers may depend on earlier facts without re-derivation. The paper reports that the verifier can accept skipped steps and erroneous literature citations, that revocation was needed after a flawed reference (§3.5), and that in the largest run the theorem rests on 664 supporting facts in chains up to depth 54 (§3.6, Fig. 2). “Essentially no false positives” is supported only by post-hoc expert review of final manuscripts, not by a quantified audit of intermediate facts or measured false-positive rates. Without such an audit (or a clearly weakened claim that the graph is a collaborative working memory rather than independently reliable truth), the central scaling argument remains under-supported at the depths claimed.","section":"§2.5, §4.3, §3.6"},{"comment":"§3.6 is presented as the strongest controlled comparison (Rethlas failed three times; Danus produced a verified solution) and the deepest fact graph. Yet after the full pipeline—including manuscript verification and human review—the authors still report that the justification of Lemma 8.7 is incomplete as written. This residual gap in the showcase case should be resolved or more carefully scoped when claiming that the system constructs long, correct proofs and that writing-stage verification catches seam errors. As written, it weakens the inference from “fact entered the graph” to “argument is sound end-to-end.”","section":"§3.6"},{"comment":"The evaluation is almost entirely qualitative case studies. Beyond the single Rethlas comparison in §3.6, there is no ablation that isolates the fact graph from other design choices (main-agent summarization, global memory, worker count/effort split, GPT-5.5-pro consultations). Free parameters (3–9 workers; high vs xhigh split; ≤1/hour expert consultation) are stated but not systematically varied. For a systems claim that fact-graph orchestration is the effective route, the manuscript needs either additional controlled comparisons or a clearer statement that the contribution is an existence demonstration of human–AI collaborative proof construction rather than a measured superiority of the memory mechanism.","section":"§3, §4.1, §4.4"}],"minor_comments":[{"comment":"Figure 2 is informative but hard to read in grayscale print; a short caption table of cluster meanings (conditional scaffolding / Chern re-derivation / integral lift) would help.","section":"Figure 2"},{"comment":"The term “verified” is used for LLM-checked informal proofs throughout; a brief terminology note distinguishing this from formal (Lean/Isabelle) verification would reduce ambiguity for mixed AI/math audiences.","section":"§2.2, §2.5"},{"comment":"§4.5 lists writing and citation-format issues as residual human cleanup; quantifying how often writing-stage verification rejected drafts (beyond §3.3 and §3.6) would strengthen the writing-loop claim in §2.7 and §4.2.","section":"§2.7, §4.2, §4.5"},{"comment":"Related-work coverage of other multi-agent math systems (Aletheia, QED, ProofCouncil, AI co-mathematician) is useful; a compact table comparing memory model, parallel proof search, and verification authority would make the positioning sharper.","section":"§1"},{"comment":"Several arXiv identifiers and dates in the reference list are very recent relative to the manuscript date; ensure all cited companion papers are stably available or mark them as concurrent work.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The contribution is real as a systems/engineering paper and is unusually transparent about human input. The main risk for the journal is over-reading informal LLM “verification” as establishing independent mathematical reliability at depth 50+. I would accept after the authors either (i) provide a sampled audit of intermediate facts / measured verifier error modes or (ii) reframe the claim around collaborative orchestration with human final authority rather than the fact graph as sole truth. Note also that several case-study math papers share authors with the systems paper; that is not disqualifying for a systems venue but should be kept in mind when assessing independence of the evaluation."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The punchline: this is a systems paper that actually runs a multi-agent harness on six research-level problems and shows, with concrete fact counts and a head-to-head against Rethlas, that shared fact-graph memory lets parallel workers build long proofs without stepping on each other. The distinctive piece is not another generate–verify loop; it is the DAG of verified claims plus a main agent that reassigns workers and summarizes state, on top of the authors’ prior Rethlas worker–verifier core.\n\nWhat is new and solid: clear separation of roles (main agent plans, workers prove, only the verifier admits facts), open source, and unusually transparent human-input logs. The matroid case is the strongest evidence—Rethlas failed three times on the same prompt; Danus produced a graph of 3,157 facts, depth 54, with 664 supporting the theorem—and several cases show unprompted decomposition, unexpected routes, and repair after a bad literature dependency via revocation. Writing is treated as a second verification problem, which is the right instinct. Self-citations to Rethlas/Matlas are engineering dependencies, not circular proof of the claim.\n\nSoft spots, in proportion: the architecture treats the fact graph as sole source of truth, so reliability rests on a stateless LLM verifier that the paper itself says can accept skipped steps and erroneous references. Revocation was needed once; the largest manuscript still has an incomplete justification for one lemma after human review. That does not erase the orchestration result, but it means the accumulated mathematics still requires expert checking, and the paper’s “effective route” claim is about search organization more than autonomous soundness. Evaluation is six detailed case studies, not a broad quantitative suite—fine for a systems paper if you do not overread it.\n\nWho it is for: people building AI-for-math agents and long-horizon multi-agent harnesses. Pure mathematicians will care about the outputs only after independent checking. I would send it to peer review; the design is specified carefully enough and the evidence is sharp enough to deserve referee time. Engage if you work on this stack; treat the math outputs as collaborative drafts, not machine-checked theorems.","headline":"Fact-graph orchestration is a real systems advance for parallel research-level math search; the load-bearing risk is informal LLM verification, which the paper mostly owns rather than hides.","tokens_in":20058,"tokens_out":548,"would_cite":true,"duration_ms":17763,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68T20","68T05","00A35"],"pacs":[],"model":"grok-4.5","headline":"A shared fact graph lets many AI workers build long research-level math proofs in parallel without losing track of what has been checked.","keywords":["mathematical reasoning agents","fact graph","multi-agent orchestration","proof verification","long-horizon reasoning","algebraic geometry","combinatorics","test-time scaling"],"falsifier":"Run the same research problems with workers and verifier held fixed but the fact graph replaced by a single shared blueprint or unstructured memory; if long verified proofs still appear at comparable depth and reliability, the fact-graph claim fails.","tokens_in":20015,"feed_emoji":"📐","tokens_out":566,"duration_ms":6424,"temperature":0.7,"pith_summary":"Scaling AI agents on hard mathematics is hard not mainly because models are weak, but because parallel search quickly muddles intermediate claims. Danus answers that problem with a shared fact graph: only statements that pass a separate verifier enter the graph, each stored with its proof and dependency edges, so the graph becomes the single source of truth. A main agent plans and reassigns workers; the workers propose local claims; the verifier alone decides correctness. Across six research-level problems in algebraic geometry, singularity theory, and combinatorics, the system assembled proofs spanning hundreds to thousands of verified facts, sometimes with little human guidance and sometimes after a short expert hint. The paper argues that this memory design is what makes long-horizon, multi-agent mathematical reasoning workable.","feed_headline":"Shared fact graph lets AI teams finish long math proofs","feed_subtitle":"Six research-level case studies show parallel workers can build arguments hundreds of facts deep","key_machinery":"The fact graph: a DAG of verified mathematical statements, each carrying a checked proof and dependency edges, serving as the system's only source of truth and the shared memory that supports both parallel search and deep chains of reasoning.","core_discovery":"Danus shows that orchestrating parallel LLM proof search around a shared directed acyclic fact graph—nodes are verifier-checked statements with proofs, edges are logical dependencies—lets many workers contribute to one long argument without context explosion or mutual interference, and that this design can produce research-level proofs that single-line or single-blueprint agents fail to complete.","pith_inferences":[],"forward_implications":[],"fun_headline_variants":["Shared fact graph orchestrates parallel AI provers for long math proofs","Verified fact DAG lets LLM workers build research-level arguments","Danus coordinates math agents via shared fact-graph memory","Fact-graph memory enables multi-agent construction of long proofs","Parallel workers + verified claims graph finish research math proofs"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"The separate, stateless verifier almost never accepts a wrong proof, so later workers can safely stand on earlier facts without re-checking them.","fun_headline_variants_meta":{"raw":{"variants":["Shared fact graph orchestrates parallel AI provers for long math proofs","Verified fact DAG lets LLM workers build research-level arguments","Danus coordinates math agents via shared fact-graph memory","Fact-graph memory enables multi-agent construction of long proofs","Parallel workers + verified claims graph finish research math proofs"]},"model":"grok-4.5","effort":"low","cost_usd":0.004018,"raw_usage":{"total_tokens":1261,"prompt_tokens":791,"num_sources_used":0,"completion_tokens":85,"cost_in_usd_ticks":40180000,"prompt_tokens_details":{"text_tokens":791,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":385,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":791,"tokens_out":85,"duration_ms":4780,"temperature":1.0,"reasoning_tokens":385,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-11T00:24:49.489339+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Run the same research problems with workers and verifier held fixed but the fact graph replaced by a single shared blueprint or unstructured memory; if long verified proofs still appear at comparable depth and reliability, the fact-graph claim fails.","supporting_citations":[],"review_version":2}