Goedel-Architect: Blueprint-Driven Formal Theorem Proving

Paper: 2606.06468 Authors: Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang Categories: cs.AI

The Gap

Existing automated theorem provers (AlphaProof, Lean-Workbench, DeepSeek-Prover-V1.5) use recursive lemma decomposition: when stuck on a goal, they generate a sublemma, try to prove it, and if that fails, generate another sublemma. This creates two problems. First, they can spiral into dead-end branches—spending compute proving lemmas that won’t help the main theorem. Second, there’s no global view: each lemma decision is local, so the prover can’t see whether its current path connects to the target.

The paper addresses this by asking: what if we plan the entire proof structure upfront, then fill in the gaps? Generate a dependency graph of all needed lemmas before proving any of them, so failed branches trigger replanning rather than deeper recursion.

Problem: Recursive proving wastes compute on dead-end branches
    |
    v
Assumption: A global blueprint eliminates backtracking inefficiency
    |
    v
Method: Generate full dependency graph, prove nodes in parallel, refine on failure
    |
    v
Evidence: 99.2% MiniF2F-test (vs 93.2% recursive baseline), 500x cheaper
    |
    v
Conclusion: Upfront planning + parallel execution beats recursive decomposition

The Increment

One sentence: Before, provers recursively decomposed goals into subgoals and could spiral into dead-end strategies; after, provers generate a complete proof blueprint upfront and refine it globally when parts fail.

Core Mechanism

Goedel-Architect has three stages. First, a blueprint generator produces a dependency graph: nodes are formal Lean 4 statements (definitions, lemmas, the main theorem), edges show which lemmas depend on which. The generator can work from scratch or be seeded with a natural language proof sketch. The output is a directed acyclic graph where each node declares its dependencies explicitly.

Second, a parallel prover works through the blueprint. Each leaf node (a lemma with no dependencies) gets sent to a tool-equipped LLM agent that writes Lean proof code. The prover uses tactic search, library search, and code execution tools. Nodes are processed in parallel—all leaves at once, then their parents once proven, and so on. If a node fails after multiple attempts, it gets marked as a blocker.

Third, a refinement loop kicks in when nodes fail. The system collects all error messages, identifies which lemmas are blocking progress, and generates a revised blueprint. This might add new intermediate lemmas, remove unhelpful ones, or restructure dependencies. The revised blueprint goes back to the parallel prover. This loop continues until all nodes close or the system hits a retry limit.

Natural language proof (optional)
    |
    v
Blueprint Generator
    |
    v
Dependency Graph:  [Def1] ---> [Lemma2] ---> [Lemma4] ---> [MainTheorem]
                      |            |
                      v            v
                   [Lemma3] ---->[Lemma5]
    |
    v
Parallel Prover (processes leaves: Def1, Lemma3 simultaneously)
    |
    +---> Success: mark done, unlock parents
    |
    +---> Failure: collect errors
              |
              v
        Refinement: generate new blueprint, adjust dependencies
              |
              v
        Retry with revised graph

Think of it like planning a construction project. A recursive prover is like building a house room by room, realizing mid-build that you forgot a foundation pillar, then digging under the finished rooms to add it—massive rework. Goedel-Architect is like drawing the full architectural blueprint first: you see all the support beams, plumbing, and electrical before pouring concrete. If an inspection (proof attempt) reveals a structural issue (failed lemma), you revise the blueprint and adjust the whole plan, not just patch one room. The blueprint is the load-bearing structure: it explicitly declares “Lemma 5 needs Lemma 2 and Lemma 3,” so when Lemma 2 fails, you know immediately which parts of the building are blocked. The parallel prover is your construction crew working on independent sections simultaneously—pouring the foundation while framing the roof, because the blueprint already confirmed they don’t conflict.

Key Concepts

• Blueprint (dependency graph): In formal theorem proving, a proof isn’t just one monolithic argument—it’s a web of definitions and lemmas building on each other. A blueprint makes this web explicit: each node is a formal statement in Lean 4 syntax, and each edge says “this lemma uses that one.” For example, to prove “every continuous function on a closed interval is uniformly continuous,” your blueprint might have nodes for “closed interval is compact,” “compact implies sequentially compact,” and “sequential compactness gives uniform continuity,” with edges showing the logical flow. The key insight: by declaring all dependencies upfront, you avoid proving lemmas that lead nowhere. If “sequential compactness” can’t be proven, you know before wasting time on downstream lemmas that assume it.

• Parallel proving with declared dependencies: Traditional provers work depth-first: prove lemma A, then lemma B that uses A, then lemma C that uses B. Goedel-Architect works breadth-first across the dependency graph: all lemmas with zero dependencies (leaves) get proven simultaneously in parallel API calls. Once a leaf is proven, its parent nodes unlock. This is only safe because dependencies are declared—the blueprint guarantees no circular reasoning. Concretely, if you have 10 independent base-case lemmas, you get 10x speedup by proving them at once rather than sequentially. The failure case is also cleaner: if lemma 7 fails, you immediately know which downstream nodes (lemmas 8 and 9, say) are blocked, so you stop working on them and refine the blueprint.

• Global refinement vs local backtracking: When a recursive prover gets stuck, it backtracks: undo the last lemma, try a different one. This is local—it doesn’t reconsider earlier decisions. Goedel-Architect’s refinement is global: it looks at all failed nodes, sees the pattern (maybe all failures involve a missing algebraic identity), and generates a revised blueprint that adds that identity as a new lemma early in the graph. The revised graph restructures the entire proof strategy. This is like debugging a program by refactoring the architecture rather than tweaking individual lines—you get structural fixes instead of patches.

Framework Shift

Before (recursive decomposition):        After (blueprint-driven):

Goal                                     Goal
  |                                        |
  +---> try Lemma1                         v
  |       |                          Blueprint Generator
  |       +---> try SubLemma1a             |
  |       |       |                        v
  |       |       +---> fail          Full dependency graph:
  |       |       |                   [Def] -> [L1] -> [L3] -> [Goal]
  |       |       +--> try SubLemma1b    |       |
  |       |               |               v       v
  |       |               +--> fail      [L2] -> [L4]
  |       |                                |
  |       +---> backtrack                  v
  |                                   Parallel Prover
  +---> try Lemma2                    (all leaves at once)
          |                                |
        [loops]                            +---> success -> unlock parents
                                           |
                                           +---> failure -> global refinement
                                                    |
                                                    v
                                              Revised blueprint

One sentence: From depth-first recursive decomposition with local backtracking to breadth-first parallel execution over a globally refined dependency blueprint.

Expert Assessment

Problem choice: This is a real gap. Recursive proving’s inefficiency is well-documented—AlphaProof’s billion-dollar training budget and DeepSeek-Prover-V1.5’s high API costs both stem from wasted search. The paper correctly identifies that local decisions cascade into global inefficiency. The timing is right: Lean 4’s formal verification ecosystem is mature enough to support this, and open-weight models (DeepSeek-V4) are finally capable of blueprint generation.

Method maturity: The core idea—plan globally, execute locally—is borrowed from classical AI planning (STRIPS, hierarchical task networks). The novelty is adapting it to formal proving where “planning” means generating formal statements and dependencies, not just action sequences. The parallel execution is straightforward once you have the DAG. The refinement loop is the clever part: using failure patterns to regenerate the blueprint. However, the paper doesn’t deeply explore when blueprint generation itself fails (garbage in, garbage out). If the initial blueprint is structurally wrong, refinement might just shuffle deck chairs.

Experimental integrity: Baselines are fair—they compare against AlphaProof and DeepSeek-Prover-V1.5, the current SOTA. The 99.2% on MiniF2F-test is impressive, but note the ceiling effect: MiniF2F problems are undergraduate-level, so gains here don’t guarantee transfer to research-level mathematics. PutnamBench (75.6% → 88.8% with NL seeding) is more convincing because Putnam problems require genuine creativity. The 500x cost reduction is calculated against DeepSeek-Prover-V1.5’s API pricing, which is somewhat apples-to-oranges (self-hosted open-weight vs. API service). Still, the efficiency claim holds directionally. One red flag: the “optional natural language proof” seeds IMO/Putnam/USAMO results. This is a significant human assist—the system isn’t fully autonomous at that level.

Writing quality: Section 3 (method) is crisp. Section 4 (experiments) buries the lede—the NL seeding detail should be upfront, not footnoted. The ablation study (Table 3) is thin: only two ablations (no refinement, no parallelization), missing key questions like “what if blueprint generation fails?” or “how sensitive is performance to blueprint quality?” The related work section undersells how much this borrows from classical planning—acknowledging STRIPS or HTN would strengthen the positioning.

Verdict: weak accept — Solves a real problem with a well-executed adaptation of classical planning to formal proving, achieving strong empirical results, but the reliance on NL seeding for hard problems and thin ablation analysis leave questions about generality and robustness.

Takeaways

Declare dependencies explicitly before execution: Whether you’re proving theorems or building software, making the dependency graph explicit upfront prevents wasted work on dead-end branches. In code, this means writing interface contracts and module boundaries before implementation. The pattern: structure first, fill in later.

Parallel execution over DAGs is underused: Once you have a dependency graph, process all leaves simultaneously. This applies to CI/CD pipelines (run independent test suites in parallel), data pipelines (compute independent features at once), and even writing (draft independent sections simultaneously). The constraint: dependencies must be declared, not discovered mid-execution.

Global refinement beats local patching: When something fails, zoom out and ask if the overall structure is wrong, not just the failing node. In debugging, this means refactoring architecture rather than patching symptoms. In project management, it means replanning milestones when blockers emerge, not just reassigning tasks. The Goedel-Architect pattern: collect failure signals, regenerate the plan, retry.