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

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 toward the main theorem. The system first generates a blueprint (optionally guided by a natural language proof), then a tool-equipped Lean prover component closes each open lemma node in parallel, with failed lemmas driving refinement of the global blueprint. This differs from mainstream recursive lemma decomposition approaches, which can inefficiently loop on dead-end strategies. Using the open-weight DeepSeek-V4-Flash (284B-A13B) model, Goedel-Architect achieves 99.2% pass@1 on MiniF2F-test and 75.6% pass@1 on PutnamBench. With optional natural language proof guidance, 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—reportedly the best open-source pipeline at a cost up to 500x lower than comparable open-source pipelines. The paper is available on arXiv (2606.06468).

Paper Overview

Research Area: 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

Introduction

We introduce Goedel-Architect, 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.

Method

1. Blueprint generation: Goedel-Architect generates a blueprint of formally stated definitions and lemmas, along with declared dependencies. This blueprint is optionally 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 in turn drive refinement of the global blueprint.

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

Results

Using the open-weight DeepSeek-V4-Flash (284B-A13B) as the backbone:

MiniF2F-test: 99.2% pass@1
PutnamBench: 75.6% pass@1
With optional natural language proof initialization of the blueprint for harder problems:
Solves the two remaining MiniF2F-test problems (100%)
PutnamBench improved to 88.8% (597/672)
IMO 2025: 4/6 problems solved
Putnam 2025: 11/12 problems solved
USAMO 2026: 3/6 problems solved

This represents state-of-the-art performance for an open-source pipeline at this price point—up to 500x cheaper than comparable open-source pipelines.

Paper Abstract

> We introduce Goedel-Architect, 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. First, Goedel-Architect generates a blueprint of formally stated definitions and lemmas, along with declared dependencies. This blueprint is optionally guided by a natural language proof. Then, a tool-equipped Lean prover component closes each open lemma node in parallel using relevant dependencies. Failed lemmas in turn drive refinement of the global blueprint. This strategy contrasts with other mainstream approaches which use recursive lemma decomposition, and can inefficiently loop on dead-end strategies. Using the open-weight DeepSeek-V4-Flash (284B-A13B) ...

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