Source-linked AI summary
Hilbert: Recursively Building Formal Proofs with Informal Reasoning
Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu, Ke Ye
TL;DR
Formal theorem proving offers reliable verification, but specialized prover LLMs solve fewer problems than general-purpose models reason through informally, while informal solutions can contain unchecked errors. HILBERT combines reasoning and proving agents with retrieval, verification, recursive decomposition, and feedback-driven refinement. It reaches state-of-the-art results on miniF2F and PutnamBench, including 99.2% and 70.0% pass rates.
Problem
Informal LLM solutions can contain serious errors, while formal prover LLMs lag general-purpose reasoning LLMs in problem-solving coverage.
Method
HILBERT orchestrates an informal reasoner, formal prover, verifier, and semantic retriever with recursive subgoal decomposition and verifier-guided correction.
Results
HILBERT achieves state-of-the-art performance across miniF2F and PutnamBench, reaching 99.2% and solving 462/660 PutnamBench problems (70.0%).
Takeaways & Limitations
HILBERT narrows the gap between informal mathematical reasoning and formally verified proof generation.
Takeaways & Limitations
LLM-based verifiers remain fallible because of hallucinations and silent failures.
Abstract
from arXiv · showhide
Large Language Models (LLMs) demonstrate impressive mathematical reasoning abilities, but their solutions frequently contain errors that cannot be automatically checked. Formal theorem proving systems such as Lean 4 offer automated verification with complete accuracy, motivating recent efforts to build specialized prover LLMs that generate verifiable proofs in formal languages. However, a significant gap remains: current prover LLMs solve substantially fewer problems than general-purpose LLMs operating in natural language. We introduce Hilbert, an agentic framework that bridges this gap by combining the complementary strengths of informal reasoning and formal verification. Our system orchestrates four components: an informal LLM that excels at mathematical reasoning, a specialized prover LLM optimized for Lean 4 tactics, a formal verifier, and a semantic theorem retriever. Given a problem that the prover is unable to solve, Hilbert employs recursive decomposition to split the problem into subgoals that it solves with the prover or reasoner LLM. It leverages verifier feedback to refine incorrect proofs as necessary. Experimental results demonstrate that Hilbert substantially outperforms existing approaches on key benchmarks, achieving 99.2\% on miniF2F, 6.6\% points above the best publicly available method. Hilbert achieves the \textbf{strongest known result} from a publicly available model on PutnamBench. It solves 462/660 problems (70.0\%), outperforming proprietary approaches like SeedProver (50.4\%) and achieving a 422\% improvement over the best publicly available baseline. Thus, Hilbert effectively narrows the gap between informal reasoning and formal proof generation. Code is available at https://github.com/Rose-STL-Lab/ml-hilbert.
1 INTRODUCTION
General-purpose LLMs reason well informally but produce unverifiable errors, while formal provers offer accuracy yet solve fewer problems. HILBERT combines reasoning, formal proving, verification, retrieval, recursive decomposition, and correction to improve benchmark performance.
- Motivation: Manual verification of informal LLM proofs is time-consuming, difficult, and error-prone.Generated solutions may contain hallucinations, logical fallacies, unjustified assumptions, or calculation errors.
- Motivation: Reasoning LLMs solve approximately 83% of PutnamBench problems informally, whereas public prover LLMs achieve only 13% with formal proofs.General-purpose models also achieve only a 49.1% miniF2F pass rate with 16,384 attempts when generating full formal programs.
- HILBERT: HILBERT orchestrates a reasoning LLM, prover LLM, formal verifier, and semantic theorem retriever to bridge informal reasoning and formal verification.The framework retrieves relevant theorems, generates informal and Lean proof sketches, and coordinates proof generation across components.
- HILBERT: HILBERT recursively decomposes failed proofs into subgoals, solves them with the prover or reasoner, and uses verifier feedback for refinement.Ablation studies validate recursive decomposition and retrieval-augmented generation as key technical contributions.
- Results: 99.2% miniF2F performance is 6.6 points above the best public method, while PutnamBench reaches 462/660 problems, or 70.0%.These experiments establish state-of-the-art performance on both benchmarks.
2 RELATED WORK
Prior work combines informal language-model reasoning with formal theorem proving through proof sketches, retrieval, tactic generation, and feedback. These approaches have progressively expanded automation but remain distinct from HILBERT’s framework.
- Automated Theorem Proving: Automated theorem provers traditionally rely on symbolic reasoning and integration tools connecting them with interactive proof assistants.Recent work has introduced LLMs as another tool for automated theorem proving.
- Prover LLMs: Specialized prover LLMs are trained on large corpora of formal proofs, especially for the Lean theorem prover.Examples include GPT-f, ReProver, DeepSeek Prover, Goedel Prover, BFS Prover, STP-Prover, and Kimina Prover.
- Informal LLMs: DSP and LEGO-Prover use general-purpose LLMs to propose proof sketches, with automated theorem provers filling formal components.LEGO-Prover additionally maintains a growing skill library of intermediate theorems for retrieval-augmented proving.
- Agentic Frameworks: Agentic systems such as COPRA, Prover-Agent, and ProofCompass use informal models, retrieved lemmas, formalization, and execution feedback to refine proofs.These systems represent increasingly interactive approaches to combining informal reasoning with formal proving.
3 HILBERT SYSTEM
HILBERT is a multi-agent Lean framework that combines informal reasoners, specialized provers, a verifier, and semantic retrieval. It decomposes theorem proofs into verified subgoals, retries them through staged solving, and recursively refines failures.
- Components: HILBERT orchestrates general-purpose reasoners with specialized formal provers to solve theorems that neither component handles alone.The system uses Gemini or gpt-oss-120b as reasoners and DeepSeek-Prover or Goedel-Prover as formal provers.
- Components: The verifier checks theorem statements and proofs in Lean 4, while the retriever uses semantic search over Mathlib theorems and tactics.Retrieval is built with sentence-transformer embeddings and FAISS indexing.
- Inference Flow: HILBERT first attempts direct proof generation with four prover candidates before invoking decomposition when those attempts fail.Valid candidates are accepted immediately through verifier checking.
- Subgoal Decomposition: Subgoal decomposition retrieves relevant theorems, creates a Lean proof sketch with have statements and sorry placeholders, extracts independent subgoals, and assembles the proof.Verifiers check the sketch, extracted statements, and assembled proof, with iterative error correction.
- Subgoal Verification: Each subgoal receives direct prover attempts, correctness verification, and a reasoner-based shallow solve before recursive decomposition.Shallow solving uses retrieved theorems and up to six correction passes, terminating incorrect proofs over 30 lines.
- Evaluation: The benchmark tables report HILBERT results on MiniF2F-Test and PutnamBench, with MiniF2F improvements measured against each prover family’s pass@4 baseline.The PutnamBench table uses the September 2025 version containing 660 problems.
4 EXPERIMENTAL RESULTS
HILBERT performs strongly on MiniF2F and PutnamBench across configurations, while recursive decomposition, retrieval, and additional inference-time computation improve formal proof success.
- Main benchmark results: 99.2% pass rate is achieved on MiniF2F by combining Gemini 2.5 Pro with Goedel-Prover-V2-32B.The system fails on only two problems in this configuration.
- Main benchmark results: 16.2% to 37.1% improvements over standalone base provers at pass@4 are obtained across HILBERT configurations.The strongest MiniF2F results use Gemini 2.5 Pro, while weaker provers still perform strongly.
- Main benchmark results: 70.0% pass rate is achieved on PutnamBench, solving 462 of 660 problems with Gemini 2.5 Pro and Goedel-Prover-V2-32B.This exceeds SeedProver’s 50.4% pass rate and the closest publicly available baseline by more than fivefold in solved problems.
- Scaling behavior with inference-time compute: Pass rate increases continuously with token usage, with the hardest problems requiring 22.8M or 27.0M tokens for the Gemini 2.5 Pro variants.These totals exceed most LLM context lengths, indicating computation is distributed across the agentic process.
- Ablation studies: Pass rate improves consistently over the D = 0 baseline of 75%, with full HILBERT reaching near-optimal performance at relatively shallow recursive depths.The depth analysis uses Gemini 2.5 Pro with Goedel-Prover-V2-32B on MiniF2F.
- Ablation studies: Retrieval raises MiniF2F pass rates from 97.1% to 98.4% with DeepSeek Prover and from 97.9% to 99.2% with Goedel Prover.The comparison evaluates HILBERT with and without the retrieval step.
5 CONCLUSION
HILBERT combines informal mathematical reasoning with formal Lean theorem proving through hierarchical decomposition. Its generated proofs and reasoning traces are intended to support future training of stronger prover and reasoner models.
- Conclusion: HILBERT bridges Lean formal theorem proving with informal reasoning by recursively decomposing complex problems into manageable subgoals.It orchestrates general-purpose reasoners with formal provers.
- Conclusion: HILBERT’s proofs and reasoning traces can be used to train improved Prover and Reasoner models.The authors describe this as a potential virtuous cycle for advancing mathematical reasoning capabilities.
A.1 ALGORITHM
The HILBERT algorithm first attempts direct formal proof generation, then recursively decomposes unresolved problems and iteratively validates, corrects, and assembles subproofs.
- Direct proof generation: HILBERT first makes multiple formal prover attempts and returns a proof immediately when verification succeeds.Algorithm 5 verifies each candidate proof before returning it.
- Subgoal decomposition: Failed direct attempts trigger recursive subgoal decomposition with a bounded depth parameter D.The resulting subgoals are solved and combined into a final proof.
- Sketch validation and refinement: Proof sketches are compiled, their subgoals extracted and validated, and errors are iteratively corrected before assembly.The correction process handles syntax, compilation, and invalid-subgoal feedback.
- Subgoal resolution: Each subgoal is addressed through formal prover generation, with informal reasoner assistance available for shallow solving.Relevant theorems are supplied to the reasoner during this fallback process.
- Retrieval: The retriever generates search queries, semantically searches Mathlib, and selects relevant theorems for the proof process.Retrieval can be disabled, in which case the relevant-theorem set is empty.
Search Query Generation (SEARCH_QUERY_PROMPT)
The search-query prompt instructs the reasoner to identify mathematical concepts and generate concise natural-language queries for relevant theorems, tactics, properties, and definitions.
- Search process: The prompt begins by breaking the problem into its mathematical concepts, operations, and structures.This decomposition guides subsequent theorem and tactic searches.
- Search process: Queries may describe relevant theorems, useful tactics, structural properties, or definitions needed for the proof.Examples include associativity, arithmetic simplification, group structures, and definitions of mathematical objects.
- Query format and guidelines: Each query must use <search> tags and the prompt limits the reasoner to a maximum of five concise queries.Queries may be based on theorem names or natural-language descriptions and should consider edge cases.
Theorem Selection (SEARCH_ANSWER_PROMPT)
The theorem-selection stage supplies the Lean problem and candidate Mathlib results, then instructs the model to choose useful theorems from that list.
- The prompt presents a Lean theorem-proving problem together with potentially relevant theorems and definitions.
- The model must select only useful theorems from the given list and exclude module names.
- Selected results are formatted individually with <theorem> tags and full theorem names.
Informal Proof Generation (INFORMAL_PROOF_PROMPT)
The informal-proof stage asks a mathematical expert to produce a rigorous, natural-language derivation from premises to conclusion.
- The reasoner is prompted to act as a mathematical expert solving problems with rigorous reasoning.
- The proof must proceed step by step from the given premises to the conclusion.
- Each step is numbered, precise, thorough, and explicit about calculations and theorem applications.
- The problem statement is supplied as the input to the informal proof.
Lean Sketch Creation (CREATE_LEAN_SKETCH_PROMPT)
The Lean-sketch stage translates an informal proof into structured Lean subgoals, emphasizing simplicity, explicit progression, syntax discipline, and verifier-friendly organization.
- The prompt combines the problem, selected theorems, and informal proof as inputs for Lean sketch generation.
- Complex reasoning is decomposed into named have-based subgoals that build toward the main theorem.
- Each subgoal should use one key theorem or a few tactics and remain simpler than the original problem.
- Subgoals are designed for atomic reasoning, clear premise-to-conclusion progression, and theorem-focused applications.
- Lean code must maintain consistent indentation, avoid nested or anonymous have statements, and use named subgoals.
Lean Sketch Creation (CREATE_LEAN_SKETCH_PROMPT) (continued)
The continued pipeline validates theorem statements, extracts missing subgoal theorems, completes and repairs Lean proofs, and evaluates performance and failure behavior across benchmarks.
- Lean Sketch Creation: The workflow prohibits undefined-type natural-number division or subtraction and requires explicit types for fractions.
- Lean Sketch Creation: Subgoal extraction turns each sorry in a proof sketch into an independent theorem with the relevant preceding context.
- Verification: A verifier checks mathematical correctness and provability, while the system reports YES or NO with a brief justification.
- Proof Completion: The prover completes supplied proof sketches using given theorems without modifying the sketch or using sorry.
- Proof Repair: Compilation-error repair targets the main theorem while preserving helper theorems and mathematical meaning.
- Results: Pass rates were 55.9% with Gemini 2.5 Pro and 13.3% with gpt-oss-120b in the reported inference-time comparison.