{"id":"6c39ebbe-dee1-4c7c-a5de-dc5b96ffb43f","arxiv_id":"2606.06468","paper_version":1,"verdict":"CONDITIONAL","confidence":"LOW","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Goedel-Architect introduces blueprint generation and iterative refinement for Lean 4 theorem proving, reaching 99.2% on MiniF2F-test and 75.6% on PutnamBench with DeepSeek-V4-Flash.","lead":"Goedel-Architect generates a dependency-graph blueprint of lemmas and definitions for a target theorem in Lean 4, then proves the lemmas in parallel with a tool-equipped prover and refines the blueprint on failures. This yields 99.2% pass@1 on MiniF2F-test and 75.6% on PutnamBench using an open 284B model, with further gains when seeded by natural-language proofs.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.3","headline":"Blueprint generation may output lemmas that fail to type-check or form a connected acyclic graph, so parallel closure success does not demonstrate the claimed architecture.","rationale":"The reader’s weakest_assumption isolates exactly the unverified precondition (formal correctness and connectivity of the generated dependency graph). The abstract supplies no counter-evidence or verification step, so the concern stands and the CONDITIONAL verdict is appropriate pending artifact inspection.","tokens_in":1880,"tokens_out":353,"duration_ms":15324,"concrete_test":"Sample the first 30 MiniF2F-test problems solved without NL seeding; for each, extract every lemma node from the reported blueprint, paste the Lean declarations into a fresh Lean 4 file with only the declared imports, and run `lean --check`. Record the fraction of nodes that fail to type-check or produce dependency errors. If this fraction exceeds 10 %, the blueprint-correctness assumption is falsified.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim requires that the initial blueprint step emits a set of formally stated Lean lemmas whose declared dependencies are both syntactically valid and sufficient to reach the target without exhaustive search. The abstract describes generation of “formally stated definitions and lemmas, along with declared dependencies,” followed by parallel closure and failure-driven refinement. No section or result in the provided material shows that the generated statements were independently type-checked in Lean 4 or that the resulting graphs were verified to be acyclic and connected. If a non-negligible fraction of nodes contain ill-formed or disconnected lemmas, the reported 99.2 % / 75.6 % pass@1 figures could be artifacts of the refinement loop rather than evidence that the blueprint strategy itself succeeds.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.3","summary":"The paper introduces Goedel-Architect, an agentic framework for Lean 4 theorem proving centered on generating a blueprint (a dependency graph of formally stated definitions and lemmas, optionally seeded by a natural-language proof), followed by parallel closure of lemma nodes via a tool-equipped prover and failure-driven global refinement. Using DeepSeek-V4-Flash, it reports 99.2% pass@1 on MiniF2F-test (100% with NL seeding), 75.6% on PutnamBench (88.8% with seeding), plus solutions on IMO 2025, Putnam 2025, and USAMO 2026, claiming SOTA for open-source pipelines at substantially lower cost than alternatives.","tokens_in":2020,"tokens_out":491,"duration_ms":19611,"significance":"If the blueprint generation step reliably emits type-checkable, connected Lean statements whose declared dependencies suffice for parallel closure, the framework could meaningfully reduce dead-end search compared with recursive decomposition methods while delivering high pass rates on established and contest benchmarks. The use of an open-weight model and explicit cost comparison are positive factors for reproducibility and accessibility.","major_comments":[{"comment":"The central performance claims (Abstract) rest on the assumption that the initial blueprint step produces formally correct, acyclic, and sufficiently connected dependency graphs of Lean statements. No results, tables, or sections demonstrate that generated lemmas were independently type-checked in Lean 4 or that the emitted graphs were verified for acyclicity and connectivity; without this, the 99.2%/75.6% figures could be driven primarily by the refinement loop rather than the blueprint architecture itself.","section":"Abstract / Blueprint Generation description"},{"comment":"Evaluation (implied in Abstract and results paragraphs) reports raw pass@1 numbers without error bars, ablation isolating the contribution of blueprint generation versus refinement, or details on failure selection criteria for refinement. These omissions make it impossible to determine whether the reported gains are robust or sensitive to post-hoc choices.","section":"Evaluation / Results"}],"minor_comments":[{"comment":"Notation for the backbone model (DeepSeek-V4-Flash, 284B-A13B) should be clarified with an explicit citation or model card reference.","section":"Abstract"}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":{"model":"grok-4.3","summary":"We thank the referee for the constructive feedback. We address each major comment below and indicate planned revisions to strengthen the manuscript.","responses":[{"response":"We agree that explicit verification of blueprint properties is needed to isolate their contribution. The generation process aims to output formally stated Lean statements, but the manuscript does not report independent type-checking success rates, acyclicity checks (e.g., via topological sort), or connectivity metrics. In the revised version, we will add a dedicated subsection reporting these statistics on generated blueprints across benchmarks, clarifying the role of the initial blueprint versus refinement.","revision_made":"yes","referee_comment":"[Abstract / Blueprint Generation description] The central performance claims (Abstract) rest on the assumption that the initial blueprint step produces formally correct, acyclic, and sufficiently connected dependency graphs of Lean statements. No results, tables, or sections demonstrate that generated lemmas were independently type-checked in Lean 4 or that the emitted graphs were verified for acyclicity and connectivity; without this, the 99.2%/75.6% figures could be driven primarily by the refinement loop rather than the blueprint architecture itself."},{"response":"We acknowledge these evaluation gaps. The current results lack error bars, ablations, and explicit failure criteria details. The revised manuscript will add error bars from repeated runs, an ablation comparing full pipeline versus blueprint-only or refinement-only variants, and a precise description of failure selection (e.g., criteria based on error types and dependency impact). This will better demonstrate robustness.","revision_made":"yes","referee_comment":"[Evaluation / Results] Evaluation (implied in Abstract and results paragraphs) reports raw pass@1 numbers without error bars, ablation isolating the contribution of blueprint generation versus refinement, or details on failure selection criteria for refinement. These omissions make it impossible to determine whether the reported gains are robust or sensitive to post-hoc choices."}],"tokens_in":1494,"tokens_out":413,"duration_ms":8891,"standing_objections":[]},"desk_editor":{"model":"grok-4.3","letter":"The main takeaway is that this work reaches 99.2% on MiniF2F-test and 75.6% on PutnamBench with an open-weight model by generating a dependency graph of lemmas up front, closing them in parallel, and refining on failures. That setup is presented as an alternative to recursive decomposition that avoids dead-end loops.\n\nThe blueprint generation step, optionally seeded by a natural language proof, is the clearest point of difference from prior agentic provers. The reported lift to 100% on MiniF2F, 88.8% on PutnamBench, and several IMO/Putnam/USAMO problems with the seeding option shows the pipeline can handle harder cases at low cost compared with other open-source systems.\n\nThe results are the strongest part of what is here. They are state-of-the-art for the open-source category and come from a fixed external model rather than heavy fine-tuning.\n\nThe soft spot is the missing check on whether the initial blueprints actually produce type-correct, connected Lean statements. The abstract describes formally stated lemmas with declared dependencies, but there is no indication that those outputs were run through Lean 4 to confirm they parse or that the graphs are acyclic and sufficient. If a non-trivial share of nodes are ill-formed or disconnected, the refinement loop could be doing most of the work, which would weaken the claim that the blueprint strategy itself is the advance. No ablations on the refinement component or variance numbers appear in the available material either.\n\nThis is for researchers working on LLM agents for formal mathematics and Lean verification. Readers who follow benchmark progress in this area will want the full methods and any released artifacts.\n\nIt deserves a serious referee. The performance numbers are high enough that the details matter, even if the current write-up leaves the central mechanism under-specified.","headline":"Goedel-Architect posts high benchmark numbers on theorem proving with a blueprint-plus-refinement loop, but the paper still needs to show that the generated lemmas are valid and connected.","tokens_in":2562,"tokens_out":449,"would_cite":false,"duration_ms":21383,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.3","headline":"Goedel-Architect generates a dependency graph of lemmas called a blueprint to structure and close formal proofs in Lean 4.","keywords":["formal theorem proving","Lean 4","blueprint generation","dependency graph","agentic framework","MiniF2F","PutnamBench","theorem proving"],"falsifier":"A concrete run on MiniF2F-test or PutnamBench where the generated blueprints repeatedly produce lemmas that remain unclosed after multiple refinement rounds, with no path to the target theorem, would falsify the central claim.","tokens_in":2776,"feed_emoji":"","tokens_out":707,"duration_ms":26418,"temperature":0.7,"pith_summary":"The paper introduces an agentic framework that first produces a blueprint, defined as a dependency graph of formally stated definitions and lemmas with declared connections, optionally seeded by a natural language proof. Each lemma node is then proved in parallel by a tool-equipped Lean prover. Failures in this closure step trigger refinement of the overall blueprint. This method reaches 99.2 percent pass@1 on MiniF2F-test and 75.6 percent on PutnamBench with an open-weight model, improving to 100 percent and 88.8 percent respectively when natural language guidance is added, plus solutions on several recent competition problems.","feed_headline":"Blueprint graph reaches 99.2% pass rate on MiniF2F-test","feed_subtitle":"Generating a lemma dependency graph and refining from failures lets an open model prove nearly all problems on standard formal math benchmar","key_machinery":"The blueprint, a dependency graph of definitions and lemmas that builds up to the main theorem.","core_discovery":"Goedel-Architect generates a blueprint as a dependency graph of formally stated definitions and lemmas with declared dependencies, optionally guided by a natural language proof. A tool-equipped Lean prover closes each open lemma node in parallel using relevant dependencies, and failed lemmas drive refinement of the global blueprint, yielding 99.2 percent pass@1 on MiniF2F-test, 75.6 percent on PutnamBench, and further gains to full coverage on MiniF2F-test plus 88.8 percent on PutnamBench with natural language seeding.","pith_inferences":["The same blueprint structure could be tested on theorem proving tasks in formal systems other than Lean 4 to check transfer.","If blueprint quality scales with model size, the method might further reduce the need for broad search on harder problems.","The parallel closure plus refinement loop might be combined with existing search-based provers to handle cases where initial blueprints contain gaps."],"forward_implications":["Parallel closure of individual lemma nodes succeeds when the blueprint supplies relevant dependencies.","Failure signals from closed lemmas can be used to refine the global graph without restarting from scratch.","The approach attains 99.2 percent pass@1 on MiniF2F-test and 75.6 percent pass@1 on PutnamBench.","Natural language proof seeding lifts performance to 100 percent on MiniF2F-test and 88.8 percent on PutnamBench while solving multiple recent competition problems."],"fun_headline_variants":["Blueprint graph reaches 99.2% MiniF2F pass@1","Refined blueprint reaches 75.6% PutnamBench pass@1","Blueprint reaches 88.8% PutnamBench with natural language","Dependency graph solves remaining MiniF2F problems","Open blueprint approach attains 99.2% on MiniF2F-test"],"cache_read_input_tokens":2112,"weakest_assumption_plain":"The initial blueprint generation produces a dependency graph whose lemmas are both formally correct and sufficiently connected that parallel closure plus failure-driven refinement can reach the target theorem without exhaustive search or dead-end loops.","fun_headline_variants_meta":{"raw":{"variants":["Blueprint graph reaches 99.2% MiniF2F pass@1","Refined blueprint reaches 75.6% PutnamBench pass@1","Blueprint reaches 88.8% PutnamBench with natural language","Dependency graph solves remaining MiniF2F problems","Open blueprint approach attains 99.2% on MiniF2F-test"]},"model":"grok-4.3","cost_usd":0.009301,"raw_usage":{"total_tokens":4206,"prompt_tokens":756,"num_sources_used":0,"completion_tokens":89,"cost_in_usd_ticks":93012000,"prompt_tokens_details":{"text_tokens":756,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":3361,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":756,"tokens_out":89,"duration_ms":32072,"temperature":1.0,"reasoning_tokens":3361,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-06-28T00:57:35.950047+00:00","model_set":{"reader":"grok-4.3"},"falsifier":"A concrete run on MiniF2F-test or PutnamBench where the generated blueprints repeatedly produce lemmas that remain unclosed after multiple refinement rounds, with no path to the target theorem, would falsify the central claim.","supporting_citations":[],"review_version":1}