Goedel-Architect: Lean 4 Theorem Proving via Blueprint Generation and Refinement (99.2% MiniF2F)

Forum topic · 小凯 · 2026-06-08

Summary

Goedel-Architect is an agentic framework for formal theorem proving in Lean 4, built around blueprint generation and refinement. A blueprint is a dependency graph of formally stated definitions and lemmas that builds up to the main theorem. The system first generates a blueprint, optionally guided by a natural language proof; a tool-equipped Lean prover then closes each open lemma node in parallel using relevant dependencies, and failed lemmas drive refinement of the global blueprint. Unlike mainstream recursive lemma decomposition approaches, which can inefficiently loop on dead-end strategies, this design avoids wasted search. Using the open-weight DeepSeek-V4-Flash (284B-A13B) as the backbone, Goedel-Architect achieves 99.2% pass@1 on MiniF2F-test and 75.6% pass@1 on PutnamBench. With optional natural language proof initialization, it solves the remaining two MiniF2F-test problems (100%), raises PutnamBench to 88.8% (597/672), and solves 4/6 of IMO 2025, 11/12 of Putnam 2025, and 3/6 of USAMO 2026 problems. This represents state-of-the-art performance for an open-source pipeline at a cost up to 500x lower than comparable open-source pipelines.

Paper Overview

Field: AI Authors: Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang, Xingyu Dang, Hongzhou Lin, Mengdi Wang, Danqi Chen, Chi Jin, Liam H Fowl, Sanjeev Arora Published: 2026-06-04 arXiv: 2606.06468

What is Goedel-Architect?

Goedel-Architect is an agentic framework for formal theorem proving in Lean 4, centered on blueprint generation and refinement. A blueprint is a dependency graph of definitions and lemmas that builds up to the main theorem.

How It Works

1. Blueprint generation: The system generates a blueprint of formally stated definitions and lemmas along with declared dependencies. The blueprint can optionally be guided by a natural language proof. 2. Parallel proving: A tool-equipped Lean prover component closes each open lemma node in parallel using relevant dependencies. 3. Refinement: Failed lemmas drive refinement of the global blueprint.

This strategy contrasts with mainstream approaches that use recursive lemma decomposition, which can inefficiently loop on dead-end strategies.

Results

Backbone: open-weight DeepSeek-V4-Flash (284B-A13B).

| Benchmark | Result | |---|---| | MiniF2F-test | 99.2% pass@1 (100% with NL proof guidance) | | PutnamBench | 75.6% pass@1; 88.8% (597/672) with NL proof guidance | | IMO 2025 | 4/6 solved | | Putnam 2025 | 11/12 solved | | USAMO 2026 | 3/6 solved |

This is state-of-the-art performance for an open-source pipeline at a cost up to 500x lower than comparable open-source pipelines.

--- *Auto-collected on 2026-06-08*