Skip to content

Hilbert: Recursively Building Formal Proofs with Informal Reasoning

🕒 Published (v1): 2026-01-01 · Source: ICLR · Venue: ICLR 2026 · link

Why this paper was selected

Recursive informal-to-formal proof construction advances LLM theorem-proving agents

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

HILBERT is an agentic framework that closes the gap between informal LLM mathematical reasoning and formal theorem proving by orchestrating a general-purpose reasoner, a specialized prover LLM, a Lean 4 verifier, and a semantic theorem retriever through recursive subgoal decomposition. It achieves 99.2% on MiniF2F and solves 462/660 PutnamBench problems (70.0%), surpassing the proprietary SeedProver (50.4%) by ~20 percentage points.

Problem

Specialized prover LLMs achieve only ~13% on PutnamBench in formal Lean 4 proofs, while general-purpose reasoning LLMs informally solve ~83% of the same problems. Existing hybrid methods (DSP, LEGO-Prover, DSP+) use shallow single-layer decomposition and cannot recursively break down subgoals that remain too hard to prove directly; agentic alternatives (COPRA, ProofCompass) still lag far behind informal reasoning performance.

Method

HILBERT orchestrates four components — a reasoner (Gemini 2.5 Pro/Flash or gpt-oss-120b), a prover (DeepSeek-Prover-V2-7B or Goedel-Prover-V2-32B), a Lean 4 verifier (Kimina Lean Server), and a retriever (sentence-transformer + FAISS over Mathlib informal descriptions).

Given a theorem, the pipeline is: 1. Direct prover attempt: generate \(K_\text{initial}=4\) candidate proofs; return if any pass. 2. Subgoal decomposition (on failure): retrieve relevant Mathlib theorems via 5 semantic queries; prompt the reasoner for an informal proof and then a Lean 4 sketch with have statements using sorry placeholders (\(K_\text{sketch}=4\) attempts, verifier-corrected); extract subgoals as independent theorem statements; assemble the proof skeleton. 3. Subgoal verification per subgoal: (a) prover attempts (\(K_\text{formal}=4\)); (b) if failed, reasoner correctness check and error feedback; (c) "shallow solve" — retrieval-augmented reasoner writes short formal proofs with up to \(K_\text{proof correction}=6\) verifier-feedback refinement passes (\(K_\text{informal}=6\) total attempts, aborted if proof exceeds 30 lines); (d) if still failing, recursive decomposition of that subgoal, up to depth \(D=5\). 4. Final proof is assembled by concatenating subgoal proofs into the assembled sketch.

Key Contributions

  • Multi-turn agentic framework combining informal reasoning and Lean 4 formal verification through recursive subgoal decomposition
  • Semantic retrieval of Mathlib theorems at decomposition time, reducing reasoner token cost and improving pass rate
  • State-of-the-art results on both MiniF2F and PutnamBench from publicly available models
  • Ablation evidence that choice of informal reasoner (Gemini > gpt-oss-120b) matters more than prover model size

Results

  • MiniF2F-Test (244 problems): 99.2% (Gemini 2.5 Pro + Goedel-V2-32B); 98.4% (Gemini 2.5 Pro + DeepSeek-V2-7B); 96.7% (Gemini 2.5 Flash + DeepSeek-V2-7B); +16.2% to +37.1% improvement over each prover's pass@4 baseline
  • Best public prior method: BFS-Prover-V2-32B w/Planner at 95.1%; proprietary Delta Prover 95.9%, SeedProver 99.6%
  • PutnamBench (660 problems, September 2025 version): 462/660 (70.0%) with Gemini 2.5 Pro + Goedel-V2-32B
  • vs. SeedProver (proprietary): 331/657 (50.4%), a +~20 pp improvement
  • vs. best open-source baseline Goedel-Prover-V2-32B self-correction: 86/644 (13.4%), a 5.4× improvement
  • gpt-oss-120b variant: 88/660 (13.3%), comparable to that open baseline
  • Retrieval ablation (MiniF2F): retrieval improves pass rate 1.3–2.5 pp while reducing reasoner tokens by ~10–43% and prover calls by ~29–44%

Limitations

  • Computational cost is high: top configuration uses ~548 reasoner calls and 2.3M reasoner tokens per sample on MiniF2F; PutnamBench evaluation was run only for the single strongest config
  • Relies on proprietary reasoner (Gemini 2.5 Pro) for best results; open-source reasoner (gpt-oss-120b) cuts PutnamBench performance from 70.0% to 13.3%
  • Recursion depth \(D=5\) and multiple \(K\) hyperparameters require tuning; failure modes at depth limit are not recoverable within a single run
  • Two MiniF2F problems remain unsolved (AMC 12A 2020 P25 and IMO SL 2007 A6), suggesting hard limits on current decomposition strategy
  • Scaling behavior with inference-time compute is analyzed only on MiniF2F; PutnamBench scaling is not reported

Relevance to Agentic AI / LLM Agents

HILBERT is a strong existence proof that multi-agent orchestration — where a general reasoner, a specialized executor, a formal verifier, and a retriever each play distinct roles — dramatically outperforms any single model acting alone, closing a 70 pp gap on PutnamBench over the best standalone prover. The recursive decomposition loop with verifier-in-the-loop feedback is a concrete instantiation of the broader "tool-augmented, self-correcting agent" paradigm, and the finding that reasoner choice dominates prover choice is a practically important design signal. For researchers tracking agentic AI, HILBERT extends the "informal-to-formal" bridge into a fully recursive, multi-turn control flow that could generalize to other domains where a cheap fast specialist (prover) can handle easy subtasks and an expensive general reasoner handles decomposition and error correction.