Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement

This paper takes the standard "decompose a theorem into lemmas" recipe for LLM-based formal proving and replaces the recursion tree with a single global artifact: a blueprint — a compiling Lean file that encodes the whole proof strategy as a dependency graph of unproved lemmas — which gets proven in parallel and rewritten wholesale when pieces fail. On a 284B open-weight MoE backbone (DeepSeek-V4-Flash, 13B active), the pipeline hits 99.2% pass@1 on MiniF2F-test and 75.6% pass@1 on PutnamBench at about $0.44 per problem — roughly 500× cheaper than the next-best open pipeline — and, with natural-language proof seeding, closes all 244 MiniF2F problems, 88.8% of PutnamBench, 4/6 of IMO 2025, and 3/6 of a contamination-free USAMO 2026.

Why recursive decomposition is the wrong shape

The dominant open recipe for hard formal proving (e.g., Hilbert, on Gemini 2.5 Pro) works top-down: try to prove the goal; if that fails, split it into subgoals; recurse. This mirrors how a human might locally attack a proof, but it has a structural flaw the paper zeroes in on: all commitment flows downward. Once the root-level split is chosen, every unit of compute below it is bet on that split being right. If the top-level strategy is a dead end — a subtly false intermediate claim, a decomposition that doesn't match what Mathlib can actually discharge — the system grinds through enormous subtrees before anything can propagate back up. And when it does back off, it typically resamples the whole strategy from scratch, discarding every subgoal it already proved.

The other failure mode is informational: each branch of the recursion tree is proved in isolation, so a lemma at one leaf can't be handed to a sibling that needs it. Real proofs aren't trees; the same intermediate fact often supports several parts of the argument. Trees force you to either re-prove it or contort the decomposition.

The cost consequences are stark. Hilbert reaches 70.0% on PutnamBench, but at pass@1840 and ~163k for a run — about244 per problem. Agentic single-LLM provers on frontier backbones (AxProverBase on Claude Opus 4.5) get 54.7% pass@1 at ~$12.60 per problem. Fine-tuned open provers used in one shot sit in the single digits to low teens on Putnam-class problems.

The blueprint: a proof plan you can compile

The paper's central move is to make the plan itself a first-class, machine-checked object. A blueprint is one Lean 4 file where:

• every node is a formally stated definition or lemma, annotated @[blueprint];
• every lemma body is exactly := by sorry_using [parent1, parent2, ...] — a placeholder that declares its dependencies;
• the target theorem is the unique sink, with its original signature byte-for-byte;
• the file must actually compile, and the declared graph must be acyclic with every node reachable from the target (validated by a Lean package, LeanArchitect).

So before a single proof is attempted, you have a globally consistent, well-typed strategy: every intermediate claim is a real Lean proposition, every dependency is explicit, and the compiler has already vetoed nonsense. This is the "aha": the expensive thing in formal proving isn't tactics, it's strategy validation, and a compiling skeleton lets you validate strategy at a tiny fraction of the cost of executing it.

The mechanism, concretely

Stage 1 — Blueprint generation. Given the formal statement (and optionally an informal proof as a structural guide), the model emits the blueprint file and iterates against the compiler until it parses, every node type-checks, and the graph passes structural validation. The system prompt (Appendix C, worth reading — it's essentially the full spec) instructs that each lemma should be "nearly trivial" given its parents: 1–2 new logical ideas at most.

Stage 2 — Parallel proving. Each open lemma is dispatched to an independent tool-equipped prover agent that sees only its lemma and the signatures of its declared parents, presented as available facts. The prover has two tools — the Lean compiler and semantic Mathlib search — and a per-lemma budget (65k tokens, 4 retries). Crucially, it has three possible exits, not two:

1. Proved — a compiler-verified proof.
2. Formally negated — if the prover suspects the lemma is false, it can register a compiler-checked proof of the negation. A false intermediate claim doesn't just time out; it dies with a machine-verified death certificate.
3. Forfeit — out of budget, the prover must write a structured post-mortem: diagnosis (STATEMENT_WRONG or PROOF_TOO_HARD), a forensic account of what it tried, and a suggested fix — for PROOF_TOO_HARD, an explicit proposed decomposition into named helper lemmas.

Stage 3 — Refinement. A refinement model reads the annotated graph — proved nodes marked, failed nodes carrying diagnoses — and emits a revised blueprint: false statements repaired (add a hypothesis, fix a quantifier) or dropped and re-routed; hard lemmas split using the prover's own proposed decomposition; dependencies rewired. Proved nodes with unchanged signatures carry their proofs forward automatically. The loop runs up to 8 iterations (16 for PutnamBench).

The diagnostic channels are the underappreciated engineering here. Negations fire on 292 of 672 PutnamBench problems. The case studies (Appendix B) show why this matters: on Putnam 1971 A6, the blueprint proposed that every non-decreasing completely multiplicative integer-valued function is a power function; the prover disproved it with the constant-zero function and suggested adding f(1)=1, which the next revision did. On Putnam 1985 B1, a prover forfeited on a monolithic case-analysis lemma but wrote out the full case split in prose; the refinement turned it into five helper lemmas, all of which closed on the next pass. Failure is being converted into structured, localized edits — not into "resample and pray."

The evidence

The headline pass@1 numbers beat every system with a published sample budget: 75.6% vs Hilbert's 70.0% at pass@1840 and AxProverBase's 54.7% at pass@1. Only the fully closed Seed-Prover 1.5 (87.9%) exceeds it, and the NL-seeded pass@4 mode matches that (88.8%, 597/672). On fresh competitions: 4/6 on IMO 2025 (Seed-Prover 1.5's fifth solve is a geometry problem handled by a dedicated engine, not a general Lean prover), 11/12 on Putnam 2025, and 3/6 on USAMO 2026 — which postdates every model's training cutoff, making it the one genuinely contamination-proof result in the paper.

The cost gap is the most dramatic single number:

The whole 672-problem evaluation cost **294**. The NL-guided pass@4 push cost another986. This is the difference between formal proving as a frontier-lab flex and something an academic group runs overnight.

The ablation you should care about. Is this the 284B backbone or the blueprint? Section 4.1 answers it directly by running Hilbert's algorithm verbatim on the same backbone:

Recursive decomposition (Hilbert) on this backbone gets 83.6–84.4%; the blueprint pipeline gets 99.2% at pass@1. On the harder Putnam subset, a single tool-integrated agent tops out at 54.5% while burning up to 10^8 tokens per problem in its tail; the blueprint reaches 76% on the same subset with the full refinement sweep costing less than one hard agentic attempt. The backbone matters (67.6% → 97.1% from tool use alone on easy problems), but the pipeline is doing real, separable work — and the efficiency win is entirely the pipeline. Solve count also grows roughly log-linearly with refinement iterations (Figure 2: 200 problems solved by the initial blueprint alone, 508 by iteration 16), so refinement is a genuine test-time compute axis, not a one-shot trick.

What to be skeptical about

The hardest results lean on Gemini. Every olympiad solve beyond pass@1 — the last two MiniF2F problems, IMO 2025 P1/P3/P4, Putnam 2025 A3/B1/B4/B6, all three USAMO solves — was seeded with a natural-language proof from Gemini 3.1 Pro. The paper is honest about this (Section 4.2 shows 0 successes without NL across 4–12 pipeline runs per problem, vs 1–4 with it), and it's a legitimate finding: for problems with non-local structure, deriving the dependency graph from the formal statement is the bottleneck, and any strong informal reasoner can supply the scaffold. But it means the "open-source pipeline" solving USAMO problems has a proprietary frontier model in the loop for the strategy. (The PutnamBench 88.8% number uses DeepSeek-generated NL proofs, keeping that stack open.) It also inherits Draft-Sketch-Prove's known risk: the formalized blueprint may drift from the informal argument, though here the compiler and refinement loop police that.

Contamination. MiniF2F and PutnamBench problems (and their human solutions) are all over training corpora; DeepSeek-V4-Flash has surely seen them. This affects every system in Table 1 equally, so the comparison is fair, but absolute numbers on old benchmarks overstate generalization. The clean signal is USAMO 2026: 3/6 with NL seeding — good, not superhuman.

Pass@1 accounting. "Pass@1" means one blueprint with up to 16 refinement iterations, each involving many parallel prover calls with retries. It's a fair pipeline-level metric (and the cost numbers keep everyone honest), but don't mentally map it onto prover-level pass@1 from earlier papers.

Backbone availability. All conclusions rest on DeepSeek-V4-Flash being as strong per-dollar as reported; the "500×" figure also benefits from comparing against Hilbert's frontier-API pricing, and Hilbert's cost is acknowledged as an underestimate of their spend — but that cuts in this paper's favor.

Why it matters

If this holds up, the interesting export isn't the benchmark numbers — it's the pattern: make the plan a compilable, verifiable object; execute its pieces in parallel with limited context; require typed failure reports (including verified counterexamples); revise the plan globally. That's a general template for agentic systems in any domain with a checker, and Lean is simply the domain where every component of it can be machine-verified. The negation channel in particular — provers actively disproving the planner's false intermediate claims — is a clean answer to the compounding-error problem that plagues hierarchical LLM planning.

Practically, a $0.44-per-problem, fully open PutnamBench-class prover changes who can do formal-math research, and makes "formalize the AI's proof so a human doesn't have to check it" economically plausible at scale.

Where to spend your reading time: Section 4 (the backbone-controlled ablation and the NL-guidance study) is the scientific core; Appendix B's case studies are the best window into why the refinement loop works; and Appendix C's system prompts are effectively the full implementation spec — you could rebuild the pipeline from them.