Hilbert: Recursively Building Formal Proofs with Informal Reasoning
Authors: Sumanth Varambally
Thomas Voice
Yanchao Sun
Zhifeng Chen
Rose Yu
Ke Ye
Venue: ICLR 2026 Poster (2026)
Keywords: Formal Mathematics
Automated Theorem Proving
Mathematical Reasoning
Lean 4
LLMs for Math
Agents
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: We built an AI system that combines informal math reasoning with formal proof verification, achieving state-of-the-art results on formal math benchmarks.

Abstract: 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 ~\url{https://github.com/Rose-STL-Lab/ml-hilbert}.

Published as conference paper ICLR 2026
HILBERT: RECURSIVELY BUILDING FORMAL PROOFS WITH INFORMAL REASONING
Sumanth Varambally UC San Diego
Thomas Voice Apple
Yanchao Sun Apple
Zhifeng Chen Apple
Rose Yu' UC San Diego
Ke Ye Apple
ABSTRACT
Large Language Models (LLMs) demonstrate impressive mathematical reasoning abili- ties, but their solutions frequently contain errors that cannot be automatically checked. Formal theorem proving systems such Lean 4 offer automated verification with com- plete accuracy, motivating recent efforts to build specialized prover LLMs that generate verifiable proofs in formal languages. However, significant gap remains: current prover LLMs solve substantially fewer problems than general-purpose LLMs operating in nat- ural 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 mathemati- cal reasoning, a specialized prover LLM optimized for Lean 4 tactics, a formal verifier, and 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. leverages verifier feedback to refine incorrect proofs as necessary. Experimental results demonstrate that HILBERT substantially outper- forms existing approaches on key benchmarks, achieving 99.2% on miniF2F, 6.6% points above the best publicly available method. HILBERT achieves the strongest known result from a publicly available model on PutnamBench. solves 462/660 problems (70.0%), outperforming proprietary approaches like SeedProver (50.4%) and achieving 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: /ttp::/gitthbbb com/ Rose- STL Lab/m ml hilbert
INTRODUCTION
Large Language Models (LLMs) have achieved dramatic improvements in mathematical understanding. Reasoning LLMs like GPT-5 and Gemini 2.5 Pro attain near-perfect performance on high- school olympiad exams such as AIME and can solve a significant proportion of competitive undergraduate- level problems from the Putnam exam (Dekoninek et al. 2025). These systems also show promise on research-level benchmarks like FrontierMath (Glazer et al. 2024; OpenAl 2025).
However, several fundamental limitations severely constrain their practical utility. These systems frequently hallucinate, producing confident-sounding but ultimately incorrect solutions. solutions, Even when the final answers correct, the underlying reasoning often contains serious flaws: "proving" by example, logical fallacies, unjustified assumptions, and calculation errors (Petrov et al.) 2025 Guo et al.) [023] Mahdavi et al.) 2025 Balunović et al. 2025). Manual verification of generated proofs is time-consuming. difficult, and error-prone.
Work done during internship Apple. Correspondence: svarambal lyducyd. edu, rosey:@ucsd.edu Equal co-supervisors.

---

Published as a conference paper ICLR 2026
Stup
Subtpool
--icor 200
Decomposition
Irretional (Bea) agrt RO)
theores sgrt.ton.iraatinl
Prover
Subgoal Decompositinn
Target Theorem
More SCAAA
Prover
Shallow
Solve
Decompositoon
Subgooa
Stop
Subgoal Theorems
Stop
Stop
Figure The HILBERT algorithm. Given target theorem, HILBERT attempts formal proof generation with the prover. Upon failure, it decomposes the problem into subgoals and tries to solve them with the prover, followed by the reasoner (shallow solve). If both strategies fail, resorts to recursive decomposition until all subgoals are resolved.
Although recent advances show LLM-based verifiers can approach human-level performance (Guo et al. Dekoninck et al. 2025), they remain fallible due to hallucinations and silent failures (Mahdavi et al.
2025
2025
Petrov et al. (002)).
Formal theorem proving systems such as Lean 4 (Moura & Ullrich| 2021) offer promising solution, as they can automatically and unambiguously verify whether a proof is correct when expressed a formal language [Kontorovich] 2025). This capability has spurred the development of purpose-built prover LLMs (Polu & Sutskever 2020), with substantial research focused on developing specialized models for generating formal
2025 Wang et al., 2025). The best open prover models achieve over 90% pass rate on m (Zheng et al. 2021 and solve
Lean 4 proofs (Yang et al., 2023 Xin al. 2024a b) 2025a Ren al. 2025 Dong & Ma
86 of 657 problems on the challenging PutnamBench (Tsoukalas al. (202).. Proprietary systems such AlphaProof (AlphaProof & AlphaGeometry/ (2024) and SeedProver (Chen et al. 2025) demonstrate this paradigm's 's potential, achieving silver-medal performance on problems from the International Mathematical Olympiad (IMO).
Despite this progress, significant performance gap remains between specialized prover LLMs and general- purpose reasoning LLMs. For example, Dekoninck et al. (2025) found through human verification that reasoning LLMs can solve approximately 83% of PutnamBench problems informally, while the best publicly available prover LLMs achieve only 13% with formal proofs. General-purpose LLMs excel at informal mathematical reasoning and understand formal language syntax well enough to write effective proof sketches and short proofs (Ren et al. 2025 Liang et al., 2025). However, they struggle with full formal program synthesis, achieving only 49.1 pass rate (with 16384 attempts) on miniF2F (Zhou et al. 2025b). Conversely, specialized prover LLMs excel at producing syntactically correct formal proofs for standalone theorems, but are brittle at language-intensive tasks like leveraging existing theorems or error correction (Liang et al. 2025). ).
To address this gap, several works have explored incorporating informal reasoning from general- LLMs to augment formal theorem- pareving capabilities. Early approaches like DSP (Jiang et al. (022)) and LEGO-Prover (Wang et al., 2023) used
L.LMs propose proof sketches, with automated theorem provers (ATPs) filling formal components, but were limited by heuristics- based ATP capabilities. DSP+ (Cao et al.) 2025) extended this approach using modern prover LLMs for intermediate steps. However, these methods struggle with complex subgoals due to shallow, single-layer decomposition. They break down the original problem but cannot further decompose subgoals that remain too difficult to solve directly. Recent agentic frameworks including COPRA (Thakur et al. 20044,, Prover-Agent (Baba et al., (202)), and ProofCompass (Wischermann et al. (2225) iteratively construct proofs using informal reasoning with feedback from the formal verifier. Although these methods show promise, their performance still significantly lags behind general-purposs reasoning LLMs.
We introduce HILBERT, agentic framework that bridges informal reasoning with formal verification (Figure П}. It orchestrates four key components: seneral-purpos reasoning LLM, a prover LLM, a verifier, and a semantic theorem retriever. Given mathematical problem, HILBERT first retrieves relevant theorems
2

---

Published as a conference paper ICLR 2026
from Mathlib (mathlib Community 2020) and generates a detailed informal proof using the reasoner. then creates a Lean 4 proof sketch decomposing the problem into manageable subgoals. For each subgoal, HILBERT employs two-stage approach: attempting formal proof generation with the prover, then falling back to the reasoner augmented with retrieved theorems. When both stages fail, the system recursively decomposes problematic subgoals into smaller problems. Throughout the process, HILBERT leverages the reasoner to interpret compilation errors, suggest corrections, and guide proof refinement at inference-time. We summarize our main contributions below.
We design HILBERT, a multi-turn agentic framework that systematically combines informal mathematical reasoning with formal proof verification, closing the performance gap between these paradigms.
We conduct comprehensive experiments on MiniF2F and PutnamBench, achieving state-of- ofte--of-theart per- formance on both benchmarks. HILBERT reaches 99.2% pass rate on miniF2F (6.6 points above the best public method) and solves 462/660 PutnamBench problems (70.0%), outperforming proprietary systems like SeedProver (50.4%) and achieving over 4x improvement versus the best open- speen-oouree baseline.
Through extensive ablation studies, we validate the effectiveness of our key technical contributions: the recursive decomposition procedure for breaking down complex proof' and the retrieval-augmmened generation mechanism for enhanced reasoning capabilities.
2 RELATED WORK
Automated Theorem Provers (ATPs) are computational systems designed to automatically discover proofs of mathematical theorems. Traditional approaches have primarily relied symbolic reasoning methods [Robinson 1965 McCune 2003, Schulz 2002) and integration tools like Sledgehammer that connect ATPs
with interactive proof assistants (Blanchette al. 2013 Czajka & Kaliszyk 2018). Recently, LLMs have emerged as a promising new tool for automated theorem proving (Polu & Sutskever 2020 Yang et al.) 2024).
The general principle is to train specialized prover LLMs large datasets of formal proofs, most prominently for the Lean (Moura & Ullrich (022]) theorem prover. Some prominent models include GPT-f (Polu & Sutskever 2020), ReProver YYang al. (2023), DeepSeek Prover family of models (Xin et al.
Prover LLMs.
2024a bj
Ren et al., 2025). ABEL (Gloeckle et al. 2024), Goedel Prover V1 and V2 (Lin et al.) 2025a b).
BFS Prover VI and V2 (Xin et al. 2025a b). Prover (Dong & Ma 2025) and Kimina Prover (Wang 2025). These models are trained by curating a substantial corpus of formal proofs and performing some combination of supervised finetuning and reinforeement learning. Several approaches have enhanced these models by incorporating subgoal decomposition into the training process (Zhao et al.) 20233 2024
ct al.
Ren et al., 2025), while POETRY (Wang et al. 2024) and ProD-RL (Dong et al. 2024) employ recursive problem decomposition. Proprietary prover LLMs like AlphaProof (AlphaProof & AlphaGeometry 2024)
and SeedProver (Chen et al., 2025) have pushed the frontier further, achieving a silver-medal performance problems from the International Mathematies Olympiad (IMO). Still, significant performance gaps remain between specialized prover models and general-purpon LLMs in mathematical reasoning capabilities (Dekoninck et al. 2025).
Using Informal LLMs for Formal Theorem Proving, Several previous works have attempted to incorporate informal reasoning from general-purper LLMs improve formal reasoning abilities. DSP (Tiang et al. 2022) used the Codex LLM to propose proof sketches in Isabelle, with intermediate steps filled in by Sledgehammer.
LEGO-Prover (Wang al. 2023) extended this framework handle growing skill library of intermediate theorems for retrieval-augeee augmented proving. Liang et al.) al.) (2025) argue that general purpose reasoning LLMs are more effective decomposing problems into simpler subgoals compared to prover LLMs. Our work extends upon this observation by using informal reasoners to recursively build proof sketches to break the problem down into simpler sub-problems that can be handled by a prover or reasoning L.M.
3

---

Published as a conference paper ICLR 2026
Several works have also proposed using an informal LLM in an agentic framework for automated theorem proving. COPRA (Thakur et al.] 2024) queries an informal LLM to construct proofs tactic by tactic, incorporating execution feedback, search history, and retrieved lemmas into subsequent prompts. Prover- Agent (Baba et al., (025) uses small informal reasoning model to produce proof steps and lemmas, which are autoformalized and solved using prover LLM. Feedback from Lean is used to iteratively refine incorrect proofs. ProofCompass (Wischermann et al.) 2025) enhances prover LLMs by adding informal proof steps as comments in the input. When proof attempts fail, it analyzes these failures to extract intermediate lemmas that enable effective problem decomposition. DeltaProver (Zhou et al. 2025b) introduces custom Domain- Specific Language to perform subgoal decomposition, and iteratively repair the generated proof using verifier feedback. Notably, it only uses an informal LLM and does not rely prover LLMs. In contrast, our work demonstrates that prover LLMs become highly effective tools when orchestrated in an appropriately designed multi-agent framework.
3 HILBERT SYSTEM
In this section, we detail HILBERT, multi-agent system that bridges informal mathematical reasoning and formal verification by orchestrating general-purpose reasoning LLMs with specialized prover LLMs. Our approach uses recursive subgoal decomposition break complex theorems into simpler subgoals that can be proven and combined, achieving performance exceeding either approach in isolation.
3.1 COMPONENTS
Before we describe the inference algorithm, we first describe the components that HILBERT orchestrates.
Reasoner. A general-purpose reasoning LLM to write informal proofs, proof sketches in Lean, and in certain instances, a formal proof. In our work, we use Google Gemini 2.5 Flash and Pro (Comanici et al. 2025) due their superior mathematical reasoning capabilities (Zhou et al. 2025b Dekoninek et al.) 2025). We also experiment with the open-source gpt spt--os-tie 12 2 Ob model (Agarwal et al. 2025) to assess the generalizability of our approach beyond proprietary models.
Prover. A specialized prover LLM to write formal proofs given formal theorem statement. In our work, we DeepSeek-V22
(Ren al. 2025) and Goedel-Prover--V. 32B (Lin et al. 2025b).
Verifier. A formal language verifier to check the correctness of the theorem statements and proofs. We use the Kimina Lean Server (Santos al. 2025) with Lean v4.15.0 and Mathlib v5.1
Retriever. A semantic search engine to retrieve relevant theorems from Mathlib (mathlib Community 2020) built using sentence transformers (all 111--mmpttbbaae
(Song al. 2020 and FAISS (Douze et al. 2024) indexing. The system computes cosine similarity between query embeddings and pre-computed embeddings of informal theorem descriptions from the mathi ib informal (Gao al. 2024) dataset, providing a simple yet effective alternative to custom retrieval models (Gao et al. 2024 Lu ct al. 2025).
3.2 ALGORITHM
Given a formal statement in Lean 4, we first attempt direct proof using the Prover. It generates Kinitial proof = 4 candidate proofs, which we verify using the Verifier. If any proof is valid, we return it immediately. When direct proof attempts fail, we use the Reasoner to decompose the problem into simpler subproblems and assemble them into valid proof strategy. Figure 2 provides overview of this stage.
4

---

Published as conference paper ICLR 2026
x
Error Messages
Verified
Proof Sketch
Proof Sketch
Reasoner
(2)
Verifier
Reasoner
Target Theorem
Error Messages
(1) Retriever
Useful Theorems
(3)
Verified
Subgoals
Verifier
Assembled Proof
44)
Reasoner
Verifier
Extracted Subgoals
LEW
LMVN
506
doo
x Error Messages
Figure 2: Subgoal Decomposition: Given theorem statement, HILBERT: (1) retrieves relevant theorems from Mathlib using semantic search, (2) generates formal proof sketch with subgoals marked as have statements with sorry placeholders, (3) extracts these subgoals as independent theorem statements, and (4) assembles the proof by replacing sorry placeholders with calls to the subgoal theorems. Verifiers ensure correctness at each stage. The error correction loops are indicated by dotted lines.
3.2.1 SUBGOAL DECOMPOSITION
Step 1 (Theorem Retrieval). Given the formal statement, we prompt the Reasoner to produce search queries to look for theorems that might help simplify the proof strategy. For each search query, we use the Retriever to retrieve the top m most semantically similar theorems and tacties from Mathlib. We again query the Reasoner to select only the relevant theorems from the fetched search results.
Step 2 (Formal Proof Sketch Generation). We prompt the Reasoner to produce detailed informal proof using the retrieved theorems. With this proof supplied in-context, we ask the Reasoner to generate Lean 4 proof sketch that decomposes the problem into simpler subproblems represented as have statements. subgoals are initially filled with sorry, placeholder keyword that Lean can temporarily treat as proof of the subgoal. We verify that the proof sketch is valid using the Verifier and leverage its feedback to correct any errors. We generate a maximum of Kaketch attempts
4 sketch attempts for each input theorem.
Step 3 (Subgoal Extraction). The Reasoner extracts subgoals from the proof sketch, converting them into independent theorem statements with relevant context from the original problem and preceding subgoals. As before, we use s sorry for the proof. We verify completeness by counting have statements in the proof sketch and ensuring that all of them extracted. In case any of them missing, prompt the Reasoner extract the missing subgoals. Each extracted theorem undergoes syntax verification using the Verifier. When errors occur, we provide error messages in-context the Reasoner for correction. This approach proves more reliable than parsing source code directly or extracting subgoals from Lean 4's proof state data structure (InfoTree) (Liang al. 2025). also enables us prune irrelevant premises from the theorem statement of the subgoal.
Step 4 (Sketch Assembly from Subgoals). We provide the Reasoner with the extracted subgoal theorem statements (which contain sorry placeholders) and validated proof sketch. The Reasoner produces an assembled proof for the target theorem by replacing each sorry placeholder in the proof sketch with calls to the corresponding subgoal theorem. We then verify both the subgoal theorem statements and the assembled proof together using the Verifier to ensure the overall structure is sound. We check for errors using the Verifer
5

---

6 attempts until we obtain Published as a conference paper ICLR 2026
and correct them through iterative feedback with the Reasoner. This guarantees that after all subgoals are proven, we will have complete proof of the given theorem.
3.2.2 SUBGOAL VERIFICATION
At this stage, we have a valid theorem proof structure and a list of subgoals that, if proven, complete the original proof. However, the mathematical correctness and provability of these subgoals remain unverified. For each subgoal, we execute the following verification and proof process:
Step (Prover Attempts), We first attempt prove each subgoal directly using the Prover, generating formal proof = 4 candidate proofs and verifying them with the Verifier. If any generated proof is valid, we accept it and proceed the next subgoal.
Step 2 (Correctness Verification). For subgoals that cannot be directly proven, we prompt the Reasoner evaluate whether the subgoal mathematically correct and whether the formal statement is formulated correctly and is provable. If the Reasoner identifies the subgoal as mathematically incorrect, unprovable, or poorly formulated, we flag for correction and return to refine the original proof sketch, repeating all steps from Section 3.2.1 onwards with the identified issues incorporated as feedback. Apart from mathematical errors, some common failure modes detected by the Reasoner at this stage include missing hypotheses or conditions in the subgoal theorem statement, and atypical behavior due to the Lean type system, such as truncation of natural numbers
We prioritize direct Prover attempts over Reasoner verification because the Prover models computationally cheaper, and a valid proof automatically confirms mathematical correctness. Empirically, we observe that a significant proportion of generated subgoals can be successfully proven by the Prover. Step ensures that we save on the computational costs of the expensive Reasoner model for verification on the successful subgoals.
Step 3 (Shallow Solve). After Step fails and Step 2 confirms subgoal correctness, we employ a Reasoner model for a "shallow solve" approach that writes short proofs for subgoals the Prover could not directly solve. We retrieve relevant theorems from the Mathlib library and ask the Reasoner write formal proof for the subgoal. The Reasoner iteratively refines proof' based on Verifier feedback for up to K proo correction passes. When compilation errors indicate missing or incorrect theorem references, we retrieve additional relevant theorems. To preserve computational resources, we terminate this step if an incorrect proof exceeds the length threshold K Kmax shallow solve length 30 lines, as excessively long proofs indicate the need for further decomposition. This entire shallow solve process repeats for up to K informal passes a successful proof or exhaust all attempts.
prroccoreationn = 6
Step 4 (Recursive Decomposition and Proof Assembly). If subgoals remain unproven after Steps 1-3, we recursively apply the subgoal decomposition process (Section 3.2.1] to break them down further. Each subgoal is subdivided until it is either successfully proven we reach the maximum recursion depth D. Should all subgoals become proven, we proceed to create a complete proof for the given theorem by stitching together the proofs for all subgoals and the assembled proof outline from Step 4 of subgoal decomposition. This is done by concatenating the proofs of the subgoals with the assembled proof produced in Step 4 of subgoal decomposition (Section 3.2.1) Any remaining unsolved subgoals this point trigger failed proof attempt, prompting us to restart the subgoal decomposition process for the theorem.
The complete algorithm is presented in Algorithm |
For implementation details, particularly parallelization
strategies, refer to Section A.3
6

---

Published as conference paper ICLR 2026
Method
Pass Rate
STP (Dong & Ma 2025) (pass 3200)
65.0% + 0.5%
(pass @ 25600)
67.6%
Simina-Prover-Ba (Wang al. 2025)
(pass 32)
78.3%
Saenna-Prover-2220 (pass (p255@1024) I024)
87.7%
w/ TTRL
92.2%
Gemini 2.5 Pro (pass @ 16384)
49.1%
Delta Prover (Zhou et al. 2025b
(pass @ 16384)
95.9%
Seed Prover Chen al.
2025
99.6%
P-o-Prroo----33 w/Planner
Xin et al. 2025b
95.1% 1%
Goedel-Prover-SFT (Lin et al.
2025a) (pass @ 3200)
62.7%
Goedel-Prover-V22. V2-88B (Lin al.
2025b (pass @ @8192)
90.2%
w/ self-correction
(pass
(024)
89.3%
Socdell-Proer--22-.1
(pass
74.6% + 1.2%
(pass@ (1922)
92.2%
w/ self-correction
(pass@ 1024)
92.6%
HILBERT (gpt-on -0ss-120s)) + Goodel-Prover--22333 V2-32B
90.8%
[+16.2%]
HILBERT (Gemini 2.5 Flash) + Goedel-Prover--e V2-32B
94.7%
[+20. 1%]
HILBERT (Gemini 2.5 Pro) Goedell-rover- V2-32B
99.2%
[+24.6%]
DeepSeek- Proveer V2-7B (CoT) (Ren
2025) (pass@8192)
82.0%
DeepSeek-Prowe Prover- V2-7B (non CoT) (pass @4)
61.3% + 0.2%
(pass @812)
75.0%
DeepSeek-Proverr V2-671BB (pass @1922)
88.9%
HILBERT (Gemini 2.5 Flash) + DS Prover- V2-7B (non-CoT)
96.7%
[+35.4%%
HILBERT (Gemini 2.5 Pro) DS Prover-V2-7B (non-CoT)
98.4%
[+37.1%)
Table 1: Results the MiniF2F-Test dataset. Improvements shown brackets for HILBERT are calculated
relative to the pass @4 baseline for each prover family. Note: Delta Prover and Seed Prover are proprietary methods and not publicly available to use. Gemini 2.5 Pro result obtained from Zhou al. (2025b)
Model
Solved Problems
% Solved Problems
Goedel-Prover-Sii (Lin al, 2025a
(pass (512)
7/644
1.1%
ABEL GGloeckle al. 20224 pass 396)
7/644
1.1%
Self Self-play Theorem Prover [Dong Ma 2025
(pass @ 3200)
8/644
1.2%
Kimina-Prover-7BB. Distill
Wang al.
2025
passs 192)
10/657
1.5%
DSP4 (Cao et al. 2025
(pass (28)
23/644
3.6%
Bourbakı Zummer et al.
2025
(pass @ 512)
26/658
4.0%
DeepSeck-Provers V2 13 (Ren al.
2025
(pass @ 1024)
47/657
7.1%
SeedProver (Chen et al.
2025
331/657
50.4%
Goedel-Prover-V2-333 V2-32B (self-correction) Lin
2025b
(pass@ 184)
86/644
13.4%
HILBERT (gpt-ose o (spt-ooss-20b) + Gredel-Prroerr
V2-32B
88/660
13.3%
HILBERT (Gemini 2.5 Pro) + Goedel-Prover. V2-32B
462/660
70.0%
Table 2: Results on the PutnamBench dataset. We benchmark on the September 2025 version containing 660 problems.
7

---

Published as conference paper ICLR 2026
Method
Retrieval
Pass Rate
Reasoner Calls
# Prover Calls
# Reasoner Tokens
# Prover Tokens
DeepSeek- Prover-V2-77
V
HILDERT+ PropSeek-Prove--2..1
X
97.1%
426
290
2.
0,4M
HILBERT+ (oedel--rovvr-V22-
V 99.2 %
548
391
2.3M
1.3M
HILDERT+ Goodel-Prover- V2-32B
X 97.9%
862
4.0M
1.2M
Table 3: Ablation with/without retrieval. HILBERT with retrieval achieves a higher pass rate while using
less inference-time compute than without retrieval. Numbers show average calls and tokens per sample, computed over samples requiring subgoal decomposition.
4
EXPERIMENTAL RESULTS
4.1 MAIN RESULTS
MiniF2E. The M dataset (Zheng et al. 2021) is a 488 problem dataset comprising of high-school mathematics competition problems. Some problems are particularly challenging, sourced from the AMC, AIME and IMO competitions. We benchmark on the 244 problems from the test split of MiniF2F. We use recursion depth D for all our experiments. For the Prover, we instantiate HILBERT with two LLMMs: DeepSeek-Proved V2-7B (Ren et al. 2025), representing a relatively weaker model, and Goedel-Prover--? V2- 32B (Lin et al. 2025b), representing a stronger one. This pairing allows us to compare performance across different capability levels. For the Reasoner, we analogously employ Google's Gemini 2.5 Flash, Gemini 2.5 Pro (Comanici et al. 2025) and OpenAl's gpt-oss oss -as--osss---- 120b. The results are presented in Table
HILBERT demonstrates strong performance across all model configurations. Our top-performing setup combines Gemini 2.5 Pro with Grover--Prove--2- V2-32B, achieving a 99.2% pass rate and failing on only two problems (AMC 12A 2020 Problem 25 and IMO Shortlist 2007 Problem A6). Even with weaker formal provers, HILBERT maintains impressive results: pairing DeepSeek-Prover V2-7B with Gemini 2.5 Pro yields 98.4%, while using Gemini 2.5 Flash achieves 96.7%. HILBERT also generalizes open-source informal reasoners: using gpt opt-oss-
-ss 120b as the informal reasoner paired with Goedel-Prover- V2-32B achieves 90.8%, a 16.2% improvement over the pass @4 baseline. Notably, the choice of informal reasoner appears more critical than prover strength. Gemini 2.5 Pro consistently outperforms Flash variants by 3-4%, larger gap than observed between different prover models, and both substantially outperform the open-source gpt-oss-120 Ob variant. Compared to standalone base provers at pass pass@4, our approach delivers substantial improvements ranging from 16.2% 37.1%.
PutnamBench. PutnamBench is a challenging theorem-prone proving benchmark comprising 660 problems from the William Lowell Putnam Mathematical Competition from 1962 to 2024. contains undergraduate- problems across Algebra, Analysis, Number Theory. Geometry, Linear Algebra, Combinatorics, Abstract Algebra, Probability, and Set Theory. Given the high computational cost of evaluating on this dataset, we only experiment with the strongest configuration of HILBERT, (HILBERT with Gemini 2.5 Pro and Proverrr-r---223 As before, we set = Our results are presented in Table
HILBERT achieves state-of-the-art performance on PutnamBench, solving 462 out of 660 problems (70.0% pass rate) when paired with Gemini 2.5 Pro. This surpasses the previous best method, the proprietary SeedProver (50.4%). by nearly 20 percentage points. Using the open-source gpt-oss-120b as the informal reasoner yields 88/660 problems solved (13.3%), performing comparably to Goedel-Prover-V2-55 with self-correction (86/644, 13.4%). HILBERT, with Gemini 2.5 Pro solves over 5 times more problems than the closest publicly available baseline, Goedel-Prover-V22-- V2-32B. We attribute this success to HILBERT'S ability compose long proofs (see Figure without the long-context reasoning issues that plague traditional LLMs (Zhou et al. (025a). For more information about the failure modes of HILBERT on PutnamBench. refer to Appendix A.7
8

---

Published as a conference paper at ICLR 2026
MisiF'2 Ressener
MiniFIF:
100
100
95.15%
95
Cumutaiive Pass Rate (%9
90
Cumulatte Pass (5)
on 0.40
85
85
20
80
75
70
Red Faoii
Fack Goekk
Rid DeopSaek
65
Fad Despaal
65
Tre Gooki
Pra- Goold
Drs Deztlcc
Pro Decpfakk
16'
10
Rensoner Calls (log scale)
LLLM Calls (log scale)
Pass Rate (ri) Reasener Tokenn
MiniF2F: Pass Rate (va) If Total eReassnne Prower) Tokens
99.3%
100
25,55
96.7%
95
Cummlativee Rat (%6)
90
T4A. TM
60
80
Cummlative
75
40
70
Gaods
Goods
65
Deppooo
Gooki
10 10'
30'
10'
10
10
10 30' 10 10
10
10'
Reasoner Tokens (Bog scalc)
Total Tokens (log scalc)
Figure 3: Pass rate (vs) Inference-time Budget. We plot the pass-rate for HILBERT on M2ni as a function of (top left) the number of Reasoner calls (top right) the total number of LLM (Reasoner + Prover) calls (bottom left) the number of tokens used by the Reasoner (bottom right) the total number of tokens used (Reasoner + Prover) per sample.
4.2 SCALING BEHAVIOR WITH INFERENCE- TIME COMPUTE
Unlike traditional prover LLMs that distribute compute across many independent proof attempts from scratch, HILBERT allocates inference-time compute across multiple interconnected stages, from subgoal decomposition to subgoal proof generation. Since this compute allocation is adaptive, cannot be captured by a simple count of independent attempts. To illustrate the compute- cempute-performance tradeoff, we plot HILBERT pass rate against the per-sample number of calls to (1) the Reasoner and (2) the Reasoner + Prover combined (Figure 3) The results reveal clear scaling relationship where pass rates increase with the number of calls per sample. Our pert-perforning configuration (Gemini 2.5 Pro with Goedel Prover) requires at most 4.5K reasoner calls and 11.3K total calls, significantly fewer than DeltaProver's 16,384 calls with Gemini 2.5 Pro. Interestingly, the weaker reasoner (Gemini 2.5 Flash) demands a substantially higher inference budget to achieve comparable performance with both prover variants. While HILBERT+ DeepSeek Prover starts with lower pass rates, it demonstrates faster improvement rates, particularly in low-budget settings, eventually performance.
matching HILBERT++Goede-
We also plot the rass-rate with token usage and observe a continuous increase in pass rate as token usage increases. Notably, the most challenging problems required 22.8M and 27.0M tokens for the Gemini 2.5 Pro variants with Goedel- Proeee-rrve---- V2 and PerSSee--Pover---e context length of most LLMs. demonstrating that our agentic framework enables models go beyond their inherent context limitations when solving complex mathematical problems, at the cost of increased inference-
respectively. These token counts far exceed the
9

---

Published as a conference paper ICLR 2026
time computation. For additional analyses of pass rates versus prover/verifier calls and inference-time compute behavior on PutnamBench, refer to Appendix A.6
4.3
ABLATION STUDIES
Performance (vs) depth. To evaluate the effectiveness of subgoal decomposition, we analyze the pass rate of HILBERT using Gemini 2.5 Pro + Goedel-Prover-- V2-32B the MiniF2F dataset across different recursive depths D. The baseline (D = 0) corresponds to no decompo- sition, where we report the standalone Prover (pass@) @4) performance. We compare two configurations: the full HILBERT system, and variant with shallow solving dis- abled iKinformal passes 0). This variant relies solely on us- ing the Prover for resolving subgoals. Figure # formance across different values of D, and demonstrates substantial gains from subgoal decomposition. Both con- figurations show monotonically increasing performance with depth, but exhibit different convergence patterns. The full HILBERT system achieves rapid performance gains, reaching 98.36% at = 2 and 98.7% by D = 3. In contrast, the no-shallow-sole variant requires greater depth achieve comparable performance. The consistent improvement over the = 0 baseline (75% pass rate) validates the efficacy of hierarchical subgoal decomposition, with the full system achieving near-optimal performance relatively shallow depths.
Pass Rate vs Depth Comparison
100
Rate (%))
90
- Hilber
Shallow Solve)
Depth
Figure 4: Pass rate (vs) recursive depth D on MiniF2F for HILBERT (Gemini 2.5 Pro) + Goedel-Prover- V2-322B
shows per-
Retrieval Ablation. To assess the impact of the Retriever on both performance and computational efficiency, we compare HILBERT a variant that omits the retrieval step. We experiment on MiniF2F across two Prover configurations:
and GoodellProvve-V2-3221 Table 3 presents the results. With retrieval enabled, HILBERT achieves higher pass rates across both configurations: 98.4% vs 97.1% for DeepSeek Prover and 99.2% vs 97.9% for Goedel Prover. More importantly, retrieval significantly reduces inference-time compute utilitzation. For the DeepSeek model, retrieval decreases reasoner calls from 426 420, average prover calls from 290 to 205, and average reasoner tokens from 2.1M to 1.9M. The efficiency gains are even more pronounced for HILBERT with Goedel Prover V2, where retrieval reduces average reasoner calls from 862 to 548 and average reasoner tokens from 4.0M to 2.3M. These results show that retrieval improves both performance and efficiency by surfacing useful theorems that simplify proofs and prevent failures from incorrect theorem names.
5 CONCLUSION
We present HILBERT, hierarchical agentic framework that bridges formal theorem proving in Lean with the informal mathematical reasoning capabilities of general-purper purpose LLMs. Our approach recursively decomposes complex problems into manageable subgoals and orchestrates informal reasoners (Gemini 2.5 Pro/Flashhgptt-oss conttttssss0000000 120b) with formal provers (DeepSeek-PPrverr V2-7B and Groedel-Prover-V22 V2-32BB) to solve theorems that neither component can handle alone. HILBERT achieves state-of-the-an performance on miniF2F with pass rates of 90.8% to 99.2%. On the challenging PutnamBench dataset, HILBERT with Gemini 2.5 Pro achieves 70.0% pass rate, nearly 20 percentage points above previous methods and approaching the 82% informal proof rate reported in Dekoninck et al. (2025).
the future, we plan to leverage this framework to train increasingly capable models. Proofs and reasoning traces generated by HILBERT can be used to train better Prover and Reasoner models. These improved models should be able to solve more complex problems than before, resulting in virtuous cycle that has the potential to continually advance mathematical reasoning capabilities.
10

---

Published as a conference paper ICLR 2026
ACKNOWLEDGMENTS
SV would like to thank Bohan Lyu and Sharut Gupta for several useful discussions about this work. RY was supported in part by the U.S. Army Research Office under Army-ECASE award W91 the U.S. Department Of Energy, Office of Science, IARPA HAYSTAC Program, NSF Grants #2205093, #2146343, and #2134274, CDC-REA-FT-2330006, as well as DARPA AIE FoundSci and DARPA YFA.
REFERENCES
Sandhini Agarwal, Lama Ahmad, Jason Ai, Sam Altman, Andy Applehaum, Edwin Arbus, Rahul K Arora, Yu Bai, Bowen Baker, Haiming Bao, al. gpt-oss- 120b & gpt-oss-20b model card. arXiv preprint arXiv:2508. 10925, 2025.
Team AlphaProof and Team AlphaGeometry. Ai achieves milver-medal standard solving international 178 mathematical olympiad problems. DeepMind blog, 179:45, 2024.
Kaito Baba, Chaoran Liu, Shuhei Kurita, and Akiyoshi Sannai. Prover agent: An agent-based framework for formal mathematical proofs. arXiv preprint arXiv:2506.19223, 2025.
Mislav Balunović, Jasper Dekoninck, Ivo Petrov, Nikola Jovanović, and Martin Vechev. Matharena: Evaluat-
ing Ilms on uncontaminated math competitions. arXiv preprini WMMiv:2505.2288. 2025.
Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C Paulson. Extending sledgehammer with smt solvers. Journal of automated reasoning, 51(1):109 128, 2013.
Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, and Fan Yang. Reviving dsp for advanced theorem proving in the era of reasoning models. arXiv preprint 1xXiv:2506611487 2025.
Luoxin Chen, Jinming Gu. Liankai Huang, Wenhao Huang. Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-prover: Deep and broad reasoning for automated theorem proving. arXiv preprint arXiv:2507.23720 223726.72776..... 2025.
Gheorghe Comanici, Eric Bieber, Mike Schaekermann, Ice Pasupat, Noveen Sachdeva, Inderjit Dhillon, Marcel Blistein, Ori Ram, Dan Zhang, Evan Rosen, et al. Gemini 2.5: Pushing the frontier with ad- vanced reasoning, multimodality, long context, and next generation agentic capabilities. arXiv preprint arXiv:2507.0626/ 2025.
Lukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. Journal of automated reasoning, 61(1):423-44 453, 2018.
Jasper Dekoninck, Ivo Petrov, Kristian Minchev, Mislav Balunovic, Martin Vechev, Miroslav Marinov, Maria Drencheva, Lyuba Konova, Milen Shumanov, Kaloyan Tsvetkov, al. The open proof corpus: large-scale study of llm-generated mathematical proofs. arXiv preprini arXiv:2506.2162), 2025.
Kefan Dong and Tengyu Ma. Stp: Self play Ilm theorem provers with iterative conjecturing and proving. arXiv preprint 202.0222002.0222., 2025.
Kefan Dong, Arvind Mahankali, and Tengyu Ma. Formal theorem proving by rewarding 1lms to decompose proof's hierarchically, arXiv preprint 2xXi:2441.00182) 2024.
Matthijs Douze, Alexandr Guzhva, Chengqi Deng, Jeff Johnson, Gergely Szilvasy, Maria Lomeli, Lucas Hosseini, and Hervé Jégou. The faiss library. 2024.
Mazaré,
11

---

Published as a conference paper ICLR 2026
Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. A semantic search engine for mathlib4. arXiv preprint arXiv:2403. 13310, 2024.
Elliot Glazer, Ege Erdil, Tamay Besiroglu, Diego Chicharro, Evan Chen, Alex Gunning, Caroline Falkman Olsson, Jean-Stanislas Denain, Anson Ho, Emily de Oliveira Santos, al. Frontiermath: A benchmark for evaluating advanced mathematical reasoning in ai. arXiv preprint arXiv:2411.04872, 2024.
Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. Abel: Sample efficient online reinforcement learning for neural theorem proving. In The 4th Workshop on Mathematical Reasoning and Al at NeurlPS 24, 2024.
Jiaxing Guo, Wenjie Yang, Shengzhong Zhang, Tongshan Xu, Lun Du, Da Zheng, and Zengfeng Huang. Right is not enough: The pitfalls of outcome supervision in training Ilms for math reasoning. arXiv preprint Sttt::25000068777 2025.
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210. 10.2220..222. /2283, 2022.
Alex Kontorovich. The shape of math to come. arXiv preprint arXiv:2510.15924 2025.
Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng. Cody Hao Yu, Joseph Gonzalez, Hao Zhang, and Ion Stoica. Efficient memory management for large language model serving with pagedattention. In Proceedings of the 29th symposium on operating systems principles, pp. 611-626, 2023.
Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang. Feng Zhang, Haitao Mi, and Dong Yu. Towards solving more challenging imo problems via decoupled reasoning and proving. arXiv preprint 27X1x22507.06804,
2025.
Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover frontier model for open-source source automated theorem proving. arXiv preprint arXiv:2502.07664. 2025a.
Yong Lin, Shange Tang, Bohan Lyu. Ziran Yang. Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508 2500::::300003111,, 2025b.
Jialin Lu, Kye Emond, Weiran Sun, and Wuyang Chen. Lean finder: Semantic search for mathlib that understands user intents. In 2nd Al for Math Workshop @ ICML 2025, 2025. URL https
/ /oopnrevieww.coo net. forum? i dd5.SFFF4FFFFFF
Hamed Mahdavi, Alireza Hashemi, Majid Daliri, Pegah Mohammadipour, Alireza Farhadi, Samira Malek, Yekta Yazdanifard, Amir Khasahmadi, and Vasant Honavar. Brains vs. bytes: Evaluating Ilm proficiency in olympiad mathematics. arXiv preprint arXiv:2504. 00094..09,,..11 2025.
The mathlib Community. The lean mathematical library. Proceedings of the 9th ACM SIGPLAN Interna- tional Conference on Certified Programs and Proofs, POPL '20, pp. 367-381. ACM, January 2020. doi: 04.14453377885.3373555 /ttppppp//aaa......oo/.1.1111111
William McCune. Otter 3.3 reference manual. arXiv preprint cs/0310056, 2003.
Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pp. 625 635. Springer, 2021. 2021.
OpenAL. Introducing gpt-5. 2025. htt.://ttte///oooo...o////////ra
12

---

Published as a conference paper ICLR 2026
Ivo Petrov, Jasper Dekoninck, Lyuben Baltadzhiev, Maria Drencheva, Kristian Minchev, Mislav Balunović, Nikola Jovanović, and Martin Vechev. Proof or bluff? evaluating Ilms on 2025 usa math olympiad. arXiv preprint arXiv:2503.21934, 2025.
Stanislas Polu and Nya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03399, 2020.
ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang. Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, al. Keepseek-prover-ee Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprini arXiv:2504.21801, 2025.
J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1))223431111 January 1965. ISSN 0004-5411. doi: 10. 00.1445321250.321255 URL.ttps://ooi.oo///00..11 321253
Marco Dos Santos, Haiming Wang, Hugues de Saxcé, Ran Wang, Mantas Baksys, Mert Unsal, Junqi Liu, Zhengying Liu, and Jia Li. Kimina lean server: Technical report. arXiv preprint prepiitt arXivv2504.2/2330, 2025.
Stephan Schulz. E-a brainiac theorem prover. Ai Communications, 15(2-3)1111-266 2002.
Kaitao Song, Xu Tan, Tao Qin, Jianfeng Lu, and Tie- Yan Liu. Mpnet: Masked and permuted pre-training for language understanding. Advances neural information processing systems, 33: 1687--1666,, 2020.
Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An in-context learning agent for formal theorem-proving. First Conference on Language Modeling, 2024.
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provee on the putnam mathe- matical competition. Advances Neural Information Processing Systems, 37:11545 37:11555-11569 2024.
Haiming Wang. Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong. Han Shi, Enze Xie, et al. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310. 00656, 2023.
Haiming Wang. Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang. Jing Tang, Jian Yin, Zhenguo Li, et al. Proving theorems recursively. Advances in Neural Information Processing Systems, 37:86720-86747 2024.
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina Kimina-prover prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11335 2025.
Nicolas Wischermann, Claudio Mayrink Verdun, Gabriel Poesia, and Francesco Noseda. Proofcompass: Enhancing specialized provers with Ilm guidance. In 2nd Al for Math Workshop@ ICML 2025, 2025.
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prowe prover: Advancing theorem proving in 1lms through large-scale synthetic data. arXiv preprint arXiv:2405. /4333, 2024a.
Huajian Xin, ZZ Ren, Junxiao Song. Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, 5: Harnessing proof assistant feedback for reinforcement
Xuan Lu, Qiushi Du, et al. learning and monte-carlo tree search. arXiv preprint arXiv:2408.08/ 08/522 2024b.
Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Sealable best-first tree search for blsed automatic theorem proving. arXiv preprint arXiv:2502.088. 03438, 2025a.
13

---

Published as conference paper ICLR 2026
Ran Xin, Zeyu Zheng, Yanchen Nie, Kun Yuan, and Xia Xiao. Scaling up multi-turn off-policy rl and multi-agent tree search for Ilm step-provers arXiv preprint arXiv:2509.06499; 2025b.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval- auggeeteed language models. In Neural Information Processing Systems (NeurIPS), 2023.
Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song.
Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412. 16075, 2024.
Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-base based demonstration learning for formal theorem proving. arXiv preprint arXiv:2305.16366, 2023.
Xueliang Zhao, Lin Zheng, Haige Bo, Changran Hu, Urmish Thakker, and Lingpeng Kong. Subgoalxl: Subgoal-based expert learning for theorem proving, arXiv preprint arXiv:2408. 11172, 2024.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: cross-system benchmark for formal
olympiad-level mathematics. arXiv preprint 1rXiv:2109.001 10, 2021.
Yang Zhou, Hongyi Liu, Zhuoming Chen, Yuandong Tian, and Beidi Chen. Gsm-infinite: How do your Ilms behave over infinitely increasing context length and reasoning complexity?, 2025a. URL https
//arxiv. owg. abs / 2502. 05252
Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang, Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jic, Xinbo Zhang, et al. Solving formal math problems by decomposition and iterative reflection. arXiv preprint arXiv:2507.15225, 2025b.
Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, Anthony Bordg, Jun Wang, and Haitham Bou Ammar. Bour- baki: Self-generated and goal-conditioned mdps for theorem proving. arXiv preprint arXiv:250..02726. 2025.
A APPENDIX
A.I ALGORITHM
The complete algorithm presented across multiple blocks for clarity and modularity. Algorithm [ provides the main entry point and high-level control flow, while Algorithm [ details the subgoal resolution strategies. Algorithms 3 and 4 focus on sketch generation, validation, and assembly processes. Algorithm [ contains the core proof generation functions that interface with different LLM components, while Algorithm 6 specifies the prompt-based functions for various reasoning tasks. Algorithm Thandles error correction and refinement procedures, and Algorithm provides supporting functions for theorem retrieval and verification.
14

---

Published as conference paper ICLR 2026
Algorithm 1 HILBERT: Hierarchical Proof Generation System
1: function GEN em, header)
2:
Input: problem (formal statement), header (context)
3:
4: Phase 1: Direct Proof Attempt
5:
proof <- ATTEMFPPROVVLLLLPPOOOOOOOCC
header)
6: proof o 1. then
return proof
8:
end
9:
10:
Phase 2: Subgoal Decomposition
11: proof <- SUBROALDDECOMPOSTTOOxoro.....e header, depth-1)
12: return proof
13:
end function
14:
15:
function DIBEGOLLDDCOMMPOSTTONNELLLLL
header, depth)
16: Decompose problem subgoals and solve recursively
17:
if depth > then
18: return L b Maximum recursion depth reached
19:
end if
20:
21:
for attempt <- Katetch ittecppes
22:
celevant_theoreeee + RETRIEVETHHOREEMS(Prbbl.cc sketch + GGNBEATTPRROOSSXEYCKOoo....c
23:
relovant_tthorrmm)
24:
sketch_ asdemblee subgoals, proved_subgcals: BERNEEAWWVALIDAATSSEECCCroOoo sketch, header, relevant__therrms)
25:
26:
then if sksetch_assembl +
27:
final_proet
SoLVAALLSUrGooAs((aubyea..,
proved_subgoals,
sketch sketch_asseeeeeeeeeeeeeeeeeessse assembled, header, depth)
ffinal_prook & then return Einol_proof end if 31: end if
28:
29:
30:
32:
end for
33: return
34:
end function
15

---

Published as conference paper ICLR 2026
Algorithm 2 HIIBBRT: Subgoal Resolution
1: function Su..VAAt..SIRGOonssssbagaaaa proved_subgoa
sketcchassembl led, header,
depth)
Solve all remaining subgoals assemble final proof
3: subgoal__pree <-
4:
5:
for all subgoal subgoals
subgeolsssssllssssss do
proof SonvEStBGOAL(aubgoa. header, depth)
7: if proof then
8:
return 1 & Failed to prove required subgoal end if
9:
10:
subgoal proofs[subgoall] &- proof
end for
12:
13: -inal_ proof +- CoNCATEMATE(header,, subgoal_prroke proofs, sketch_assembledd
14:
return final final_proci proci
15:
end function
16:
17:
function SoLVEESURGAA((uuggoal header, depth)
18:
Solve individual subgoal with multiple strategies
19:
20:
Strategy Direct Prover Attempt
21: proof + ANTEMFPRRVVRLLLLPPORRrrbyga hoader)
22:
proof # 1. then
23:
return proof end if
24:
25:
26:
Strategy 2: Shallow Solve with Reasoner
27:
relevant tteorremteeeeeeeetee < RETRIVEETHERREMSSebbbaa
28:
proof +- SHALLOWSOLWE(eubgoaL, header, [terrnntthhermmm]
29:
proof * then
30:
return proof end if
31:
32:
33:
Strategy 3: Recursive Decomposition
34:
if depth < then
35:
proof <- SSIEOALDDECOTOOSSTOOVEEEEogg,,, header, depth + 1)
36:
if proof * I then
37:
return proof
38:
end
39: end
40:
return
41:
end function
16

---

Published as conference paper ICLR 2026
Algorithm 3 HILBERT: Sketch Validation and Refinement
1: function AEFINEAANDVADAATSSKEET rooo 1 em, sketch, header, rellevant_theorem: Iteratively refine sketch until all subgouls valid
2:
3:
for correction t- o
overections
4:
cretcchssyttcctii <- COMPLANNCCMMCCSSSIAEEEXXSSO... sketch, header,
relevant Sevvant_thhorem_e
if w == 1 then return 1, 0, 7: end
5:
8:
subgoals +- BRR.RCCSSunoooAAAcctcccssstttttt header) if subgoals == 1 then
9:
10:
return 1,0,0
end
12:
sketch_assembless + AASHLLPPPPFFFooTSTooooooCCCACACS subgoals, header)
13:
if sketch_assemblee == then return 1,00
14:
15:
end
16:
valid, verified verified_subboals; groved_subgoall atror_justification < VALDDTEESUBGOALSSSubbbea header)
17:
if I'valid id then
18:
sketch verified proved_subgoals
19:
else
20:
skotch error_jusee prror_justiFication
21:
end
22: end for
23: return 1. 0.
24: end function
25:
26:
function VALIDATESTRROAA.SSeubgaaa header)
27:
Validate subgoals through formal proving and correctness checking 28: verified_subee
+- ()
29:
proved_subgoas
30:
31:
for all subgoal E subgoals do
32:
proof + XTTAAFRROOELLLLMROOGGIIIgLL header)
33:
if prooff I then
34:
verified_subgoale groved_subboollssuubggee < proof
stl.fiiiidssugllleeeeeeaa U (subgoal}
35:
36:
else
37:
mathematicalll
justification
CHECGMMATHHMAATTCACCCORRTTTT
NESS(subgoal)
38:
if mattheaticallyy correct then
39:
verified veri@iee_suupoalls subgoals <- verified subgooaaddd (Ssogoaassuuuuoaa) (subgoal) else return false, 0, 0, justification end end if
40:
41:
42:
43:
44:
end for
45:
return true,
proved_subgoals, 1
46:
end function
17

---

Published as conference paper ICLR 2026
Algorithm 4 HILBERT: Proof Sketch Refinement and Assembly
1: function AAREEEAACCOORRRTTYTTTEARRRR
em, sketch, header, rellevat__hhoremm)
2: Compile sketch with sorry and cornect errors
3: verified, error_messan +- VERIIYYROOFFhhaaee: + sketch)
4: verified then
5: return sketch
6: end if
8: Error correction loop for sketch
9:
for correction + to K hheurm do
10:
sermmented_thoremeee selat_t__hheoesss
AUCMEAYTHIOOERSSSTTTTSSSSSSS
problem,
sketch +- CoURECTSAETCHIRRRoOsseee.dd error prro__mesaage augmented__heoremm)
12: verified, error_ seror_message + VERIFYRoOOF(hadder sketch)
13: verified then
return sketch 15: end
14:
16: end for
17: return 1.
18: end function
19:
20:
function AASSAMBLLPPOOFFooSSBBOLLLLLLLCCE
subgcals, header)
21:
b Assemble complete proof outline with verification
22:
all_theorems + REAAONEELLLMMSSLLLCCCLLLLLLLLLLD
23:
sxetcch_sseeblles +
sketch,
[_theormm))
24:
corrected_promm
Varnkhhtcckrekoooowrhhnnnnseseee return correctea_proos
al1 a11_theorems, header)
25:
26: end function
27:
28: function Ver.WATOOKEFFPOTTTTooneeccee...
theorems, header)
29: b Verify assembled sketch and correct ermors
30: Full_proof header + thecrems + sketch_assemblle
31: verified,
VEaIrYPRooF(uul_prroo
32: if verified then
33:
return www.shhassseealleee
34: end if
35:
36:
for correction + Ksterre corrections do
37:
sketcchassembl f- REASONVRRLL.(A.SSSRRII CORRRCTTON_PROOEE error)
full_proo= + header + theorems + sketchhasseeeeeee ed fied, error +- VERIFYPROOF(Fu11 (fporfo 40: if verifiee then
38:
39:
41:
return sketch assembled
42:
end
43:
end for
44: return 1
45: end function
18

---

Published as conference paper ICLR 2026
Algorithm 5 HILBERT: Proof Generation
1: function ATTEMPTPROVERL.N I o em, header)
2: Multiple allempts with formal prover LLM
3: for attempt <- formal stterpps
4: procf <- PRovEeLLM(probleem
5: verified, error +- VeauYPRoorraedder prooff
6: if verified then return proof 8: end
9: end for
10: return 1.
11: end function
12:
13:
function GENERKTPPROFSSEECCCHrroo... gelevaat_theoreen
14:
Generate informal proof sketch using prompts informal_pree
15:
REASONERLLMM BOWIHLLAOOONOAAAALPOPOOOOOOOOO
problem,
relevant_theorens)
16:
sketch +
problem, relevant_theorems,
informal .
17:
return sketch
18:
end function
19:
20:
function SHALLOWSOLVV(suubaall, header, rolovant_thcoroms]
21:
Shallow solve with error correction loop
22: proof 4- ATTEMETRREASOOEEPRROOSSSSSSSE
televant_theoreng
23: verified, error_nessage VERimYPRoOF(haader prooff)
24: if ieverified then
25: return proof
26: end if
27:
28:
Error correction loop
29:
for correction + to K subgoal corrections do
30:
augmented_theoorems re relevant_ arrrant_therrems_
ANCKENYTHOORMSSKTOOOJJaaga
subgoal,
31:
proof CORRCCROOFEEROOICO... error_message sugmented_theorem.. verified, error peror_messageece +- ViaUFYRooFrheader prooff) verified then
32:
33:
34:
return proof
35:
else
36:
Check proof length cutoff when verification fails |proof] K mas shallon soive lengh then return b Proof too long and still incorrect, abandon
37:
38:
39:
end if end
40:
41:
end for
42:
return 1.
43:
end function
19

---

Published as conference paper ICLR 2026
Algorithm 6 HILBERT: LLM Prompt Functions
1: function PRO
rellevan__cheormms)
2: Shallow solve using informal reasoning
3: proof +
subgoal, relevant_theorems)
4: return proof
5: end function
6:
7: function SECCEMAVVEEAAATC..CCCEEEEEEEEEE
8:
> Verify mathematical correctess of subgoal
9: correct, justification + REASSNERLLOETERMIN IF SULG__LL_OOAAOOPOO
subgoal)
10:
return correct, justification
end function
12:
13:
function EXTRACTISUBGOALS(Kktttt.. headez)
14:
Extract have statements independent subgoals
15:
subgoals
sketch)
16:
17:
b Syntax check and correction for each subgoal
18:
corrected suteeessssslllsss__s <- ()
19:
for all subgoal subgoals do
20:
verified, error +- VERIEYRooOr(zeader subgoal)
21:
verified then
22:
correctcc__ubboaals + corccccdduuupal U (subgooa1)
23:
else
24:
Error correction loop
25:
corrected <- false se
26:
for attempt + to Kauggni conections do
27:
subgoal COORECTTEORRMMEROMGCGCCCCOOO verified, if veerifie +- VERUrYPRooFfbesder subgoal)
error)
28:
29:
30:
corrected_subgaate + corrected_subgoalls U {subgoal)
31:
-orrected+ttri +
32:
break P Successfully corrected
33:
end if end for if -corrected then
34:
35:
36:
return 1 Failed to correct subgoal, return failure
37:
end if end
38:
39:
end for
40:
41:
return correcteed_subgaal
42:
end function
20

---

Published as conference paper ICLR 2026
Algorithm 7 HILBERT: Error Correction
1: function SETTINSSKKECBBSEEENERRRROOO
error_justi fi fication
2: Refine proof sketch based subgoal validation
3: refined < REASONELUL(COORRET SKETCH BASED ON INCORRECT SUBGOAL PROMPT,
sketch, error_ irror_juutiffiationn
4: return refined
5: end function
6:
7: function COREECTXEECCEERO((Xcc.... error_message, relevant_theoroms)
8: b Correct syntax and compilation emors
9: corrected < MAAXOVELLMPPROFFBEEEECLLLCCCLOOE
error_message,
sketch, relevant_theorems)
10: return correctec
11: end function
12:
13: function CoRRECTRROFERROR(pPro
arror_message, sugmentted_theoremm)) Correct proof ernors using enror feedback corrected +
14:
15:
error_nessage, proof,
augmented augmenteed_theorems)
16:
return corrected
17:
end function
18:
19:
function CORKECTTHOOEEEEEROOCCCCLLL. crror_mossage)
20:
Correct syntax errors in extracied subgoals corrected <-
21:
error_message,
subgoal)
22:
return corrected
23:
end function
21

---

Published as conference paper ICLR 2026
Algorithm 8 HILBERT: Retrieval and Helper Functions
1: function RETRRIEVETHROORRMSprro Theorem retrieval from Mathlib
2:
3:
retrieval_een ed then
4:
search, queries <- GEYBRATTSSANNCHHQUUULLSSppoo.eeE
5:
candidate eew.rdtttttheesmeeeeeeeee <- SSNANTTCEE.RCCtEENonnneeaaaa..c quepreeeeeeeecrcccuuerrrresee
6:
selevant__heereee SLLCCAALEETANTTHRRERMCCnnaaaae
htwpriidddttttteeeteteeee theorems, problem)
return relevvaa___hheereemm
8: else
9: return
10: end if
11: end function
12:
13: function CAANAATESSACGIIUUESSSSOOOO...
14:
Generate search queries for theorem retrieval
15: queries REASONERLLM(GEARGR QUERY PROMPI, problem)
16: return queries
17: end function
18:
19: function SELETTRILLWAATTHHOOMCCCCCaaCaai theorems,eeee problem)
20:
Select most relevant theorems from candidates
21: selected <- REAOOEELL((SSAICCAANNOO
problem, candidate (
22: return selested
23: end function
24:
25: function VERUFY prooff)
26:
Verify proof using Lean verifier
27: result, error_message +- La
28: return resuit, sxror_messee
29: end function
30:
31: function or
exheren
32:
b Add theorems for missing identifiers
33:
missing_ids EXTAACCMSSSNNOONTTRRRRCCOLLLLLs
34:
if missinng_ds then
35:
additional_theoreme < RerRewveTHtoteee(ppoclleen
missing_ids)
36:
return suuuneiiiiiinghhhreeeeee + additional Saaditiioal__heoreems
37: end if
38:
return existing_thheoemms
39:
end function
22

---

Published as conference paper ICLR 2026
A.2 PROMPTS
Search Query Generation (SEARCH QUERY PROMPT)
You are helping solve Lean theorem. proving problem using the mathlib library.
Refora attempting write the proof,
first search for relevant theorems and tactics.
Search Process:
1. Icentify key concepta: Break down the problem Into mathematical concepts, operations, and structures lavelved.
2. Genezate search queries: For each concept, create informal search strings that describe: Relevent theorems or reselts (0.g., "asseciativity of addition", "existence of inverse elements*)
Useful Lactics le.g., "simplify arithmetic expressions", *split conjunctiona")
Properties (e-g., "group struuture integera", "metric apace propert Relevant definitions uselul for the proof or used theozem (e.g, "definition of group", "definition of metric space")
search Query Format:
pags your informal description, Limit yourself maximum of 5 search queries. Make the search queries simple, concise, and cleas.
query
Suidelines:
You can either search by theorem name or nstural language description parts of the proof Consider edge cases and spectal conditions mentfored in the problem
Search for theorems that might
Problem to Solve:
(problem:
Theorem Selection (SEARCH
You helping to solve Sean theorem proving problem using the mathlib Library, The problem is: (pzoblem;
Here are some potential fal ly ralevant thaorems and definitions: [Sheorema]
rnstrioioon::
1. Select important theorems and definitions necessary solve the problem.
2. IMPORIANT: ONLY SELECT theorems from the GIVEN list.
3. Enclose of them in separate <theoram> tags.
4. Only atate the full names of the theorema, Do NOT include the module name. Select
useful in intermediate sleps of the proof.
23

---

Published as conference paper ICLR 2026
Informal Proof Generation (INFORMAL PROOF PROMPT)
You are nathematical expert whose goal is Le solve problens with zigorous nathematical reasoning.
[useful_theoremm____ _tthhooeemssecttonn
instructions:
Provide natural language, step-by-step proof the gi ven prob] aa.
2. Start from the given premises and reason step-by-step to reach the conclusion.
3. Number each step of the proof as 1, 2, and 20 on.
4. pedantic
thoreugh passible.
5. Keep each atep precise, increase the number of steps if needed. N07 gloas
any step, 7. Show the explicit sellollatoons/cmmmlliiiaaaa.ss ayalysts.
thorough posaible. theorem applications and case
8, Enclose the informal preof in cinformal Lags.
Problam Statement: [problem]
24

---

Published as conference paper ICLR 2026
Lean Sketch Creation (CREATE LEAN SKETCH PROMPT)
You are Lean 4 expezt who is Lrying co help write a proof Lean 4.
Problam Stotement: [problem]
Informal Froof: (informal_proef)
instructions:
informal
proof
the problem
following
these guidelines:
Breax сomplex reasoning into logical sub-goals vaing "have" statements.
The aubguals should build up to the main theorem.
Make sure to include all the steps and calculatiens from the given proof in the proof sketch.
Rach subgos should ideally require applying just one key theorem or lemma, or a Lactle applications.
Rase subgoal around:
Useful theorema mentioned in the problem context
Standard library theorems llkke arithmetic properties, operations, etc.l
The supplied premises the theorem statement
of the Do NOT create subçoala that are more complex than the original problema, The given probles.
NOT create subgoala idantical
hypotheses
subgosis should SIME
Do NOT skip over ateps. no NOT make any machematical leaps.
Subgesl Structure Requirements:
siiimpiiity:=:: Each sthgoal proof should be achievable with 1-3 basic tactics
*vAtom reasoningee: Avold combining multiple logies steps
aubgoal
++Clear progression<4: Show logical flows "premises + Intermedlate steps + final result" possible
Theoren focused.:: Design
subgoal directly apply specific
NOTE: Only add sub goalsgall that simplify the preof the main goal.
when writing Leen proofa, mointain consistant indentation lavels.
Rules:
proof
indentation: tactics
loçical must
use idencical indentation
2. Consistent characters: Use either tabs 98 spaces consistently (den's mix)
3. Proper nesting: Indent sub-proofa
lavel deeper than their perent
4. no NOT nest "have" statementa in each other. Usse inst sub-goals as much as posaible.
5. Do 80T include all goals
anonymous imports or open statements in your code.
One 'have" subgeal. Bo NUT split subgeals 7. Use proper Lean syntax and corvensions. Ensure the proaf aketch is enclosed in triple backticks ">lea"'>
Uhe
different
8. Usa 'sorry' for subgoal proofs forus
irplementation 9. +DDo NOT use "aorry" for the main goal proote - use your subgoala to prove it "sorzy"
NEVER
statement iteelf
11. insure subgoals collectively provide evezything needed for the main proof Make logical dependancies ialid and provable in Tean 4.
subgoals explicit. Ensure subgoals
13. Bo NET change anything in the original theorem statement.
tean Hints: (leen_hints)
25

---

Published as conference paper ICLR 2026
Lean Sketch Creation (CREATE LEAN SKETCH PROMPT) (continued)
IMPCRTANT INSTRUCTION; Do NOI, under ARY circumstances, allow division and subtraction operations
number literals with UNDEFINED types, uniess REQUIRED by the theorem statement. For example, do NOT allow literals like "1 5" "1
ANYNHERR
of the subgeals. ATMAYS specity the typea.
AVOID natural zumber arithmetic UNLESS NEEDED by the theoren statement.
ATMAYS specity types whar describing fractiona. For example, [12 R)
or
((2 Q) 3) Lnstead (2 3), Do this evezywhere EXCEFT the given theorem statement. INPORTANT INSIRUCIION: Do NOI, under ARY circumsiances, sllow division and subtraction operations variables of type natursl numbers (Nat N), unless REQUIRED by the theorem statement. For example, do NOT allow expressians like (a-h) type
suitable type (2, Q or Ri whan performing arithmetic operations. AVOID netural number arithmetic UNLESS by the theorem statement.
Subgoal Extraction EEXTRATT_SUBGOLLS SUBGOALS FROM SKETCH SKETCH_PROMPT)
From this procf sketcá, extract any missing proofs (specified with "sorry") as independent subgos (theorems), Instructiona:
Usa same name as
atenaments the theorems.
2, Each subgoal should have the relevant context from the previous aubgoals needed simplify the proof as much as possible.
3. there should be many extracsed theorems 'sorzy's the given theorem.
4. no NOT include any importa or open stataments. to NOT add any definitions. ONLY inolude the thecrem
5. Use separate Lesn 4 "'lean" block for each subgual. scrry
proof. NOT prove any theorem.
7. Do NOT change the conclusion of the theorems frem the extracted aubgoals, Keep them As IT IS.
8. N0t
the conclusions of the preceding theorems when presenting them hypotheses for the next aubgoals. Keep then As TT IS.
different theorems, 10. Make zure the names and types of the premises/arguments in the extrected theorems subgoals
N07
distinet
names
they extracted.
IMPORTAN: INS:RUCT_ON: Do NOI, under ANY circumstances, allow division and sustraction operations natural zumber liserals with UNDEFINED types, unless ReoUTRED by the theorem statement. For example, do NOT al literals is like '1 3 "1
theorem statement. AVOID astural zumber arithmetic UNLESS NEEDED by the theoren statement. ALMAYS specify types wher. daseribing fractions. For example, [12 R) ((2 Q) instead (2 /
specify
types.
or
IMPORTAN: INS:RUCT_ON: to NOI, under ANY circumstances, allow division and subtraction operations
variables of typa natural numbers (Mat N), unless REQUTRED by the theorem statement, For example, do NOT allow expresatons like (a-b) are type
cast (2, 0 or XI when performing arithmetic operations. AVOID natural number arithmetic UNLESS by the theoren statement.
type
Lean Kints: [lean_hints]
s>leand (proof_sketch)
26

---

Published as conference paper ICLR 2026
Subgoal Solving (SOLVE_SUBGON) PROMPT)
Think stap-by-step to complate the following Leon procf.
(problem)
Lean Hints: (leen_hints)
Tactic sints: (sactic_hints)
Rules:
1. Same proof level = same indentation; All tactics the same logical level must use identical indentation
2. Consiatent characters:
either tabs 38 apaces consistantly (don't mix) 3. Proper nesting: Indant sub-prao*a one lavel deeper than their parent N0r inclide any imports open
5. Use proper Lean syntex and conventions. Ensure the prosf sketch is enclosed in ">lean"""
triple
6. only include aingle Tean 4 code block, corresponding to the proof slong with the theoren statement.
7. Whan dealing with
numeriesl quanticies, avoid explicit computation much as possible. Use tactics like rw to perforn aymbolic manipulation rather than nunezical computation.
8. Do 801 use sorry.
change anything
original statement.
guseful_chhorremsssee ion]
Mathematical Correctness Check (DETERMINE IF CORRECT SUBGOAL PROMPT)
You expert in mathematics.
evaluate
given mathematical. theorem
aathenatically correct. You do NOT have to previde preof for the theorem in Lean.
Eva Evaluation criteria:
1, Mathematioal vaLidity: Check for logical errors, Lacorrect assumptiona, or calculation mistakes.
2, no N0T flag general results or helper Temmas that are true independent of the given premises. flag inaccuracies mistakes.
5. Provability: Determine if the statement can be proven giver the provided premises, otherwise.
AasumpLiont
1. The given premises mathemscically correct. Do NOT caeck this.
2. The syntax is quaranteed to be correct (do not assesa syntax)
theorem Starement:
(problem)
Report your answer as either:
YBS if the statement is nathematically correct
NC if the statement has mathematical errors that preveat proof
Also provide brief justification for your decisien in cjuntiiaatiooss/uuttttiet tags, adding detaf's about why the stacerent is correct or incorrect.
If it incorrect, also provide description of how the error be corrected, there are missing azguments, make sure to add the zelevant missing preof steps.
27

---

Published as conference paper ICLR 2026
Sketch Assembly (USE SKETCH AND
LED THEOREMS THEOREMM_PROMPPT
You are Lean 4 expert. Your goal is to write a proof in Lear 4, according to the given sketch, usiing the supplied theorens.
[psoof_sketch]
ubeorems:
(cheoroma_atxtin)
Instructions:
You
correct
directly your proof.
2. Do NOT modify the given theorams.
3. Do N01 prove the given theorems.
N0T modify the given
sketch stops. Simply apply the given theorems
complete the mlasing "sorry" steps.
"sorcy" 5. Do 801 include any imports or definitions er open statements.
N07
your proof.
Not re-define
given
your response.
8. no NOT write proof for any subgeal from acratch. ATMAYS use the aupplied theorems.
under cirummstances, allow division and sust operations or natural number literala with UNDEFINED types, unlesa by
IMPCRTANT INSTRUCTION:
literals '2 5" or '1 3". ALMAYS specify the types. AVOID natural number arithmetic by the theoren statement.
statement.
example,
UNLeSS
ATMAYS specify types wher deacribirg fractiona. For example, [(2 R) / 3) or (12 : Q) 31 instead (2 3), Do this evezywheze EXCEFT the given theorem statement. under MYY roumstances, allow division and subtraction operations on variebles of Lype natural numbers (Mat or Ni, unless example, la/b) where b are of type N. ALMAYS cast the variables to suitable type (2, or Ri performing arithmetic operations. UNLESS NEEDED by the theoren statement.
IMPORTANT TNS"RUCT"OM:
REQUIRED
statement.
expressions
(a-b)
number arithmetic
be single block containing completed given theorem.
Assembly Correction (ASSEMBLY CORRECTION PROMPT)
The follexing Tean code has compl lat ervors. Please fix the errors wht le maintaining the mathematical meaning.
[e:ror_meesage)
Lean Hints: (leon_hinta)
Instructions:
1. Anslyze what the thecrem is trying prove. Then, analyze why the error is happening, step-by-step, Add a brinf explenation.
Thea, provide spacific errors.
You change of the helper theorems.
correct
that appears the and.
3. 8OT inciude any other Leen code blocks except for the proof. Do Nor include any imports open statements.
4. no NOT use "sorry" in any part of the proof.
change anything
originsl
statement.
6. Do NoT incltde the helper thearen. definirions in your responsa. NOT write proof for any subgoal from scratch. ATMAYS use the supplied theozems.
28

---

Published as conference paper ICLR 2026
Sketch Refinement Based on Incorrect Subgoal (CORRECT SKETCH BASED ON INCORRECT SUBGOAL PROMPT)
You expert writing where one of the subgos la hea some 1sauea, to the
proofs.
Lean proof sketch
proof sketca.
(proof_sketch)
Issues:
[isauea]
Lean Hints: (leon_hinta)
Rules:
1. Same proof leve:
indentation: All tactics the logical level must use identical indeatation
spaces consistently (don's mix) 3. Proper nesting: indent sub-praefs one lavel deeper than their perent NOT nest "have" statementa each other. Krita different hove statements for different sub goals.
Consisteat characters:
5. Ensuze all sub goels are named. NOT create anonymeus have statements. open statements.
6. Not include
7. Cne 1ine - One "have" subgoal. Do NOT apiit subgoals across different lines. proper
syntax and convenzions. in triple backticks "lean""
proof
Usa "sorry" for subgoal proofa foaus structure, not impetatttoioon "sorzy" for the sain goal prooI.a
10. *DDo NOT
subgoals to prove it
11. NEVER use "sorry" IN the theorem statement itself
subgoals collectively provide everything needed for the main proof 13. Make the logical dependencies between subgoals explicit. Ensure that the subgoals
12.
valid 14. Madify only the incorrest subgoal and averything that fallows it in the proof sketch. Leave all preceding portions unchanged.
provable
15. Either modify the groblematic subgoels fix the ercors, add additional subgcals to fill in the missing machemacical arguments.
29

---

named. NOT create anonymous have Published as conference paper ICLR 2026
Proof Sketch Correction (PROOF SKETCH SRROOF_SKEECHLLLCCC CORRECTION PROMPT)
The follewing Lean code has compilation eccors, Please fix the ezrore while maintaining the mathematical meaning.
Original statements innforml__tttermee
[e"ror_message]
Leen Hints: (lean_hints]
Instructiona:
1. Analyze what the theorem is trying prove. Ther, analyze why the error is happening, step-by-step. Add a brief explanation.
2. Thea, provide corrected version of the Lean 4 code that addresses these specific errors.
3. NOT inslude any other
code blacks except for the proof. Do include any importa or oper statements, serry
the
"have"
5. Rnsure there are no use of "serry" statements outside of "have" statemertss.
Do 807 use "sorry" while proving the main theorem.
N0T change enything the eriginel thecrem statement.
7. Do Not nest "have' statements in each other. Use distinct sub-goals as much poasible.
all
statements.
seneful_thhorems_coe sect ion]
Proof Correction (PROOF CORRECTION PROMPT)
The following Lean code has compilation errers. Please [ix the errora while maintaining the mathematicel meaning.
[e"ror_message)
Instructions:
theorem trying prove. Then, analyze why ezror happening, by step, Add brief explenation.
Analyze
2. then, provide a corrected version the Lean 4 code that addresses these specific
3. no N07 inolude any other Tean code blocks except for the proof.
801 eorzy.
5. Do 801 inciude any imports or open statements.
Not change anything original
statement.
suseful_theormmmssetiio
Subgoal Syntax Correction (SUBGOAL_ SYNTAX CONFRCTION (RORMCTTIONNPRMMTT)
The follewing Lean theoren has compiletion ecrors. Please fix the errors while maintaining mathematical meaning.
Instructiona:
1. Analyze why the error is heppening, step-by-step. Add a brief explanation. addresses
Thea, provide corrected version the specific errors.
blocks except 4. Usa sorry for the proof.
Not inciude any other
5. NOT inolude any importa or open atatements.
jpotnnially.eefu_leeeeeee
30

---

Published as conference paper ICLR 2026
A.3 IMPLEMENTATION DETAILS
We improve HILBERT efficiency through several runtime optimizations focused on parallelization. The Prover LLM is served using vLLM (Kwon et al., 2023) and the Lean Verifier using Kimina Lean Server (Santos et al. 2025) to handle multiple requests in parallel.
We implement AsyncJobPool, a mechanism built around Python's asyncio o library, to orchestrate parallel requests across framework's 's multiple steps. Submitted jobs run concurrentyy until specific completion criteria are met based on the algorithm step. Concurrency controlled using Semaphores. We implement three completion criteria:
Wait for All. The execution terminates when all jobs in the pool have finished execution. This criterion is used to parallelize across examples, and across subgoals (Section 3.2.2).
First-Success Termination. Execution terminates as soon one successful job is found, and pending jobs are terminated. This criterion is used to parallelize across proof attempts (the initial Prover attempts, and Steps and in Section 3.2.2).
First Failure. Execution halts upon the first job failure, immediately canceling remaining jobs. This criterion is applied during subgoal correctness verification (Step 2 Section [.2.2p. Since verification failures often indicate fundamental issues with the proof sketch that affect multiple subgoals, early termination prevents wasted computation on dependent subgoals, which may change after correcting the problematic subgoal.
31

---

by Published as conference paper ICLR 2026
A.4
SUBGOAL DECOMPOSITION EXAMPLE
theorem sqrt_ten_ sgrt_ten_irrational : Irrational (Real.sqp) sqrt (10 a))
Reasoner
sert. Lon.trrationa:: Irrational (Roal.sqrt
Verifier
C18 RD) i-
NEN
(Real. (18 RQ)
(1R: NO sorry
sorry have 63 Inrationsl (Real serr (1 (0) :o serry
-Ilssqurre
Retriever
(1)
Proof Sketch
Useful Theorems
Reasoner
iheonnn ki..srt_.ten inrational:
Imoetiona:
(3)
Verifier
irrational: Irratioral
(Rool.sort by sonry
-IoSquore
NPN
[38 R0) :- by
Inrational Steat..ortt
-IsSquore
[38: 1) -- -1.sgrt.tee ponrt.ten.trrttion
-Isiquare
h2
(B NO by serry
have Irrational (Real. sert R))
pe_.ert_teniirratien
h1_ssrt_.ten_tee inn.
(Real CaBl R33 -IaSquore (10 N)3
Assembled Proof
Irrational (Ros)..srr (10 (Q) to by sorry
Extracted Subgoals
Figure 5: Subgoal Decomposition Example. We illustrate the subgoal decomposition process using the input theorem
seen_irrationn The process consists four main steps: (1) We retrieve relevant theorems from Mathlib to inform the proof strategy. (2) The Reasoner generates a proof sketch, which verified by the Lean Verifier for validity. If verification fails, етгоr messages guide the Reasoner to make corrections. (3) The Reasoner extracts subgoals from the validated sketch and verifies their correctness, refining them as needed. (4) The Reasoner assembles a complete proof by incorporating the extracted subgoals into the original sketch. Since the subgoals lack proofs this stage, they are denoted by sorry. This assembled proof undergoes final verification. The process outputs both the complete assembled proof and the verified subgoals (without their proofs). Note that while Steps (3) and (4) are shown together this figure for simplicity, they represent distinct operations detailed in Figure
A.5 MINIF2F PROOF EXAMPLE
We include an example to demonstrate how our hierarchical algorithm can help discover proofs that are too complex for either the Prover or informal Reasoner alone. We present the proof for Problem 4 from AMC 12B 2002, problem which was unsolved even by DeepSeek Prover V2-67 IB after 8196 passes. find that HILBERT is able to solve the problem with one layer of decomposition using Goedel Prover V2-32B model as the Prover.
import Math" ib import Aеsop
option naxHeartbeats
open siguperators Real Nat Topology Rat
theorem _oooo__mmelb______ mmmi2b__c02_pp _p (n 8) m)
(8k
142
+ (h_k k_i___n V (k. N), 41 42 (42
m1
hamain
by
have hi : k 1 im isnooe & hk exact h1
32

---

Published as conference paper ICLR 2026
h_main
s_sum_i frac aasa__amcilb_2000 2002____0_____ Ni 100k) (1
to Q
(1 141 n 42)1 / 142
m) i= by
have 2
h1
/ tn (4 4211 (44 =- by
Q1 #
cast
linerith
Use faald_afmp co find common benominator and step! ffy the expresatin
field_simp [ha]
-- Normaliza the expresaton by expanding and aimpilfying it
5,2 ring_nf
</> fieid_simp [ha]
<12 ring_nf
4/> norn_oast
<)> simp [mui_assoc]
</> norm_num
4/2 linarith
apply h1
theorem h ____is_one_amcc2__22000
(n N) the 0 1k No, 41 42 142 n)
by
intro nkk
have h1 : # 0 by
by_contra
Ansume k and derive a cont ction, simpa usinng
zw [by] at lkk
by
by
ring_nf at n:k H
<;> alinerith
have 41
by
nlinarith linarith
h2 1m by by_contra
Assume k 2 2 and derive contradiction.
have
by
omega
:- by
have he : k (12
nl 2 2 (42 m) by
hg
hg
have hr (42 N)
by positivity
mlinarith
have hs : 2 (42 n) 84 =- by
ring
have le : k (42 n) 2 64 by
Linarith
have
< 84
have ha : n 2 := by linarith
have
43 by
mlinarith
have hro :
have h11 43
43 =m by mlinarich
omega
have hi1 64
by
cases n with
contradiction
suce =>
simp [Nat.mul_add, aad add
<j> ring_nf at hg <3> (try omegal <;>
rlinarith!
omega
33

---

Published as conference paper ICLR 2026
have has : 41 Linarith
(12 A) : by
linarith
have hg k
by
h4 : S by
have ls : 2 :- by
by_contra h6
TF K 1a not 2 ! then 0, which cad hy
hy
by
omega
contraciction
omega
theoron d_diviide__mmm2h___ 20022_22000_p____
(ho
(1
/ tn Qdeden
1) (h_aum_ s_trac (1 7.2 3 7
1 tn ( (1" + 4213 / 1442 nl) 42.
a I A 42 :- by
have ha ((1
42)
Q) 1(42 m)) .den
by
have h21 (41
42) : Q 142 m)) (1 1 /
1n Q : by
[h_aum_ [s_frae]
<p> field_simp <2> ring_nf <2> norm_cast
<p> field_aimp <i> ring_nf <3> norm_cast
rw [ha1]
exact h1
have ha 142 n n. 2) (41 n
42
2) 10 by
have ha1 1(141
Z))_cen
norm_cast at b2
<;> simpa "div_eg__e mul
using h2
have has 3 (K Σ), (141
42
21
1 / (42 2)
18 Q by
have has : [[[1] n 42 2) Q)
/ 142
_))_den :- h31
have h24 3
2), (141
2) Q1
(42
21
18
Q)
by
dee the fact that the nator 15 1 to find an inceger
has
Z),
n
Z)
Q)
Use the property of rational numbers with denominates
han (1(41
: 2)
h31
have ha7 3 (k 2), 1441
42 2) Q1 (42
2) (k () by
use the fact that the denominator is to find an integer
rafine' (1(141
-242 2) / (42
21) .um,,
have has : [(141
( (42 n 2)) 611141
42 21 () 142
by
have hss [1141 a 42
(12 . (d)_dea c has
have h40 : [(14]
0
(42
21) (11(4)
2) 0 / (42
2) nnm Q:
rw [t- Ram.num mtt_.mm__vvvdd (1141
* 42
2)
Q) / (42 21)1
<p> field_aimp [ha9]
<;> norm_cast
<;> simp_all [Rat_den_nz]
exact hao
exact has
exact hs7
exact has
h34
ostain (k, has) :- ha2
hes
2:
n
by
have has : [44 n 42 2) Q)
/
(42
2) (k Q :=
has
have has : 142
*
by
have
Ni
have has : (42 n 2)
> 0 sm by
norm_cast
<5> alinarith
linarith
have h37 : (41 n 42
(42
2) by
rie e_anpp [hae] at hgs
<7> ring_nf has norm_cast has
(try norm_num at has F) <5>
34

---

Published as conference paper ICLR 2026
(try linerith) <;>
(try simp_all [mul_comm]
(try ring_nf at has <7> norm_cost at hag </> 1inarith) <p>
(try
alinarich
1)
(try
fiald_simp has F </>
ring_nf at has <,>
norm_cast has Linarith
have has : (41 n 42 2) nost_ et ha7
(42
Zl = by
<t>
(try sing_nf at lisr H] 9p>
(try
at H) <p>
(try limerith)
(try
cield_simp ha7 H 83>
ring_nf at har H 62> Linarith
haz
have hag : (42 122-0:2 2) (41
42
Z) :- by
linerith
hga
exact hg4
have h4 42 41
42 by
h41
21
42 hg
have h42 142
No
11
42 N) by
Convert the divisibility from integers to natural numbers
<p>
[Lzy omegal
Itzy
Use the fect that the integers positive to convert naturel numbers cases' h41 with k hk
<1>
(tzy sing_nf
(try norm_cast at hk F) <2>
(try omega)
H)
<;> itry
Sandle any zemaining cases simplifications simp_ [mul_comm]
<1>
sing_nf
<1>
norm_oast
65>
onega
Use the natural number divisibiilty to conclude the proof simpa [mul_comm) using
35

---

Published as conference paper ICLR 2026
MiniF2F: Puss Rate (v5) Prover Cails
MiniFZF: Pass Rate (v5) Verifler Calls
2%%
99.2 2%%
95.1 7/"
Cumulative Pass Rate (N)
Cumulative Paos Rate (%)
80
24.7%
80
75
75
70
70
Goodcl
65
Flail - DeepSeek
65
Fladi Doypock
Ps Goodl
Pro Goodd
60
DeesSeck
60
DespBeck
10
10
10'
10'
Prover Calls (log scale)
Verifler Calls (log scale)
Figure 6: Pass rate (vs) Prover and Verifier Calls. We plot the pass-rate for HILBERT on MiniF2F as a function of (left) the number of calls to the Prover (right) the number of calls to the Verifier, per sample.
exact h4
theorem amcl2b_2002_pp la N) (ha : 0 m) (h1 (1
1a :0::: .d.den 1) a
42 1= by
Step 1: Combine the rationa! numbers into aingie fractioon.
have __aun_ia_rres
11
1/ 7 1 to Q) (f a 42)) / 142 nt :- by ho
exact 2ia__==s__sa__eee2___222222.
step 2: Use the denominator condition (hi) to establish a divisibility relation. for d N' with 'd 0",
According to 'Rat.dan www.dii__aaata_ee_eeoooo
'((m Q) / d).den = 1' iff 'd m'm.
h_divides :
41
:= by
exact
h_aun Lasuunna__rraaa frac
Step 3: By the definition of divisibilily, diiiivies"" implies theze exists a netural numbez "k" such that '41
42
142 n] This step proves that 'k' must be 1.
have h_k_ia_one__ : V.k N, 41 nnn 42 x (42 ni + k := by
exact p_k_is_one__mme aem__ammm2__.mmm 2002_p4 ho
From aidivides, we obtain the existence of such 'K" and its corresponding equation. reases h_dividas with (k, hie)
Re use commutativity of muitiplication to match the form expected by the heiper theprem. [mul_comm (42 n)] hk
proof from n_K_ia_one have kone k :- by
that this specific 'K" must exact "_one_amei" attpaammmc2_2______ p4 n ho hk h_k_1a_one Substituting à back into the equation. IM [k_one, one_mal] at hk
The equatias 18 now '41 n 42 42 + n", Ne solve for 'e". n".
can zewrite
[show 42 41 + a by zing] az hk
cancelling ing 142 a" Zrom both sides, get '62 27.
exact eddlt.edddefft_eeeee left_cencel hk). .ayam
A.6 INFERENCE TIME COMPUTE
PutnamBench. Our main paper results for HILBERT with Gemini 2.5 Pro were obtained using exhaustive compute with multiple retries per problem, without tracking inference-time compute. To better understand the inference-time compute scaling behavior, we rerun PutnamBench with strictly one attempt per problem
36

---

Published as conference paper ICLR 2026
Bench: Pass Rute vs Reasemer Calls
Bench: Pass Rate vs Total L.M Calls
Cumulative Pass Rate (%)
Cumulative
11-
sum
14158-1200 200
WV
(log scale)
Calls (log scalle
PuttammBench: Pass Rate Vertfler Calls
PainammBnnhh: Pass Rate Total Tokens
464
Cumelative Pass Rate (%)
Cumulative
Him
pum
GPE-065-1225
G2T--SS-
Verifier (log
Total Tokens (log scale)
Figure Pass rate (vs) Inference-time Budget. We plot the pass-rate for HILBERT on Putnam as a function of (top-left) the number of Reasoner calls (top-right) the total number of LLM (Reasoner Prover) calls per sample (bottom-left) number of verifier calls (bottom-right) total number of tokens.
for both HILBERT with Gemini 2.5 Pro and opt-oss-120b obtaining pass rate of 55.9% and 13.3% respectively. The results are reported in Figure
As observed on MiniF2F, performance improves continuously with additional inference-time compute for both model configurations. However, the more capable Gemini 2.5 Pro is substantially more compute-efficient than -ps- 120b, achieving higher performance equivalent compute budgets while also being capable sustaining more reasoning turns to tackle harder problems. Compared to MiniF2F, the most challenging PutnamBench problems require several orders of magnitude more tokens, reflecting the greater difficulty of the benchmark. Finally, the compute distribution exhibits pronounced long-tail, with the median number of LLM calls required being far lower than the mean (Table 5), indicating that while most problems resolved efficiently, a small number of hard problems consume disproportionately large amounts of compute.
A.7 FAILURE MODES ON PUTNAMBENCH
better understand the failure modes of HILBERT on PutnamBench, we log every LLM call and verifier call during inference to determine the bottleneck to model performance. We then analyze the last step of HILBER before failure and classify them as either sketch generation, sketch assembly or shallow solve. While sketch
37

---

Published as a conference paper ICLR 2026
Run
Avg #tokens/prohlem
Avg #verifier calls
Avg #reasoner calls
Avg. A.I.M...M calls
Gemini-2.5 2.5-ini Probll--rover
3.3M
427.5
403.9
635.0
Gemini-2.5 2.5mni-2.5-Flahh
2.7M
475.3
360.3
646.4
Gemini-2.. 2.5-Pru Goouee-Prooer--V V2-32B
0.9M
146.3
133.7
230.8
Gemini-2.5 2.5-Pro DeepSeck-Prover-V22.
137.0
159.5
235.5
GPT-OSS- 208 Prover---rover-Ve
0.1M
15.9
7.6
22.0
Table 4: HILBERT inference-tine compute summary statistics on the MiniF2F dataset, computed over
successful proofs.
Rus
Avg mokknn/prbblem
Avg Averiteer culls
Arg trassneer calls
Aug #LLM calls
Median ALLM calls
Mecian frcusonnr calls
Geaiini-2 5-Pro Goedel-Phover----11
24.4M
3019.4
4083.5
$352.
817.0
540.0
GPT-08S-1 120 + Cherkt--Pooor-22-000
20M
166.
129.2
235.
160.5
67.5
Table 5: HILBERT inference-tinee compute summary statistics on PutnamBench, computed over successful proofs.
generation/asssembyy failures indicate the model's inability construct usable sketch and decomposition strategy, shallow solve errors indicate failure to discharge Table indicates the percentage of number and percentage of problems failed at each stage.
subgoals into valid Lean proofs.
We observe that the failure profile is qualitatively different across models. PTT-OSS-120FF failures are overwhelmingly concentrated sketch generation (497/571, 87.04%) and assembly (68/660, 11.91%), with almost none reaching shallow solve (6/571, 1.05)). suggesting the model rarely produces usable proof structure in the first place. Gemini, by contrast, fails much later in the pipeline. Most failures occur at shallow solve (130/290, 44.83%). followed by sketch assembly (81/290, 27.93%) and sketch generation (79/290, 27. 27.24%). This pattern indicates that Gemini more reliably constructs a decomposition strategy but frequently struggles to close the final verification loop. These failure modes suggest that allocating more attempts per problem could help mitigate a meaningful fraction of these failures.
A.8 PROOF LENGTHS
Figures 8 and show the distribution of proof lengths generated by HILBERT on the MiniF2F and Putnam- Bench datasets, respectively. For comparison, Figure also includes proof lengths from DeepSeek-Prove V2-671B MiniF2F problems.
On MiniF2F, HILBERT generates substantially longer proofs than DeepSeek-Pron Prover- V2-67 IB, with an average length of 247 lines compared 86.7 lines. Notably, HILBERT produces one proof spanning 8.313 lines, demonstrating its capacity for tackling hard problems.
This trend toward longer proofs is even more pronounced PutnamBenchh where HILBERT achieves an average proof length of 1,454 lines. The longest proof on this dataset exceeds 15,000 lines of code. The ability consistently generate such extensive proofs likely contributes HILBERT's superior performance on PutnamBench compared to baseline methods, as longer proofs may reflect more thorough exploration of intermediate steps necessary for a complete Lean proof.
Failure Stage
OpenAl gpt-gsstt oss-1203
Gemini 2.5 Pro
Sketch generation
497 (87.0) (7.04%)
79 (27.24%)
Sketch assembly
68 (11.91%)
81 (27.93%)
Shallow solve
6 (1.05%)
130 (44.83%)
Table 6: Failure mode breakdown on PutnamBench.
38

---

Published as conference paper ICLR 2026
MiniF2F (Hilbert) proof))
Lengths (DeepSel--Prvee-- prouf)
Mos, proffinghh 131 Nees
Mix pronflenghh 1963 liwe.
Nuobet Pres
Number
Progf (Lines Cfde 1V
1
Leoght (Libes Cfde
Figure 8: Lengths of proof' generated by (left) HILBERT (Gemini 2.5 Pro + Goedel-Prover-V2) (right)
DeepSeek-Pront Prover-Vo V2 671B for problems from MiniF2R.
PutnamBench Proof Lengths
(462 proofs)
Avg. proof length 1454.5 lines proof length 15306 lines
25
Number of Proofs
20
15
10
10'
10
Proof (Lines of Code)
Figure Lengths of proofs generated by HILBERT (Gemini 2.5 Pro + Goeeell-Poverr-Ve V2) for problems from PutnamBench.
39


Reviews:
[{"review_id": "9QvVovfIFb", "reviewer": "Reviewer_xeDx", "summary": "This paper introduced Hilbert methodology to decompose  the mathematical problems into subgoals and try proving such subgoals in both formal theorem proving (Lean 4) system and informal approach (LLM-based reasoning). Their system consists of four components: a reasoner of general-purpose LLM to write informal theorem proof, a prover that writes formal proof given informal one, a Lean-based verifier that checks the correctness of the formal statement, and a retriever that retrieves relevant theorems from Mathlib. In addition to utilizing both formal and informal reasoning by the reasoner and Lean-based verifier, they use retrieved theorems to enrich the reasoner.\n\nIn the experiments, they introduced models with Gemini 2.5 Pro/Flash for the reasoner and\nGoedel-Prover-V2 for the prover. Gemini 2.5 Pro with Goedel-Prover-V2-32B, achieving a 99.2% pass rate. Needless to say, this is far better than those achieved by the Gemini 2.5 Pro model alone. They also achieved 70.0% in the PatNum bench.\n\nIt is difficult to fairly position this paper because the idea of decomposing the theorem and using both formal and informal reasoning is already examined in some of the previous studies [Baba 2025, Zhou 2025b] as the authors discussed in the related work section. Although, Hilbert system achieved remarkable scores, it can be also regarded as a combination of existing ideas and best performing models.", "questions": "- I'd like to know how the retrieval is effective within the PatnumBench. Can you present the ablation study to turn on/off the retrieval module in PatnumBench?", "limitations": "", "rating": 4, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- S.1: Achieving very close to the previous best model result (99.6% by SeedProver) of 99.6% in MiniF2F and better than the SeedProver in PutnamBench.\n- S.2: The effectiveness of the theorem retrieval is examined in the ablation.", "weaknesses": "- W.1: It seems that most of the core idea (dual use of formal and informal reasoning) comes from several existing studies [Baba 2025, Zhou 2025b] as the authors discussed in the related work section.\n- W.2: Similarly, authors didn’t compare their model with the similar formal and informal reasoning models [Baba 2025, Zhou 2025b].\n- W.3: Authors tried their system with the best performing external models that often prevent fair cost/performance comparison with the previous systems.\n- W.4: Compared to [Baba 2025, Zhou 2025b], the retrieval module can be new. However, the authors do not present the effectiveness of this module in the PatnumBench.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "kxUnU9xOvi", "reviewer": "Reviewer_N4a2", "summary": "This paper proposes a new agentic framework named HILBERT. It aims to bridge the gap between the informal mathematical reasoning capabilities of Large Language Models (LLMs) and the rigorous verification capabilities of formal proof systems like Lean 4. HILBERT orchestrates four components: a 'Reasoner' for informal reasoning (e.g., Gemini 2.5 Pro), a 'Prover' to generate formal proofs (e.g., Goedel-Prover-V2), a Verifier, and a theorem Retriever.\n\nWhen the Prover fails to find a proof alone, HILBERT recursively decomposes the problem into subgoals, attempting to construct and refine the proof using feedback from the Verifier and Retrieval-Augmented Generation (RAG) via the Retriever. Experimental results show that HILBERT achieves a 70.0% pass rate on the particularly challenging PutnamBench, significantly outperforming existing proprietary methods (SeedProver, 50.4%) and public baselines (13.4%), thereby reporting state-of-the-art (SOTA) performance.", "questions": "**Regarding novelty**: Concerning the novelty of the method, the combination of subgoal decomposition, RAG, and Verifier feedback has already been explored in prior research. What, specifically, do you consider to be the core \"Technical Novelty\" of the HILBERT framework that is not present in this existing work?\n\n**Regarding the theoretical background**: The effectiveness of subgoal decomposition is demonstrated empirically. However, are there any theoretical or empirical insights into what types of problems (or logical structures) this recursive decomposition is particularly effective (or ineffective) for? Furthermore, how were the failure modes of decomposition (e.g., decomposition into incorrect subgoals, getting stuck in an unsolvable state) addressed?", "limitations": "", "rating": 6, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "**Exceptional Experimental Performance (SOTA Achievement):** The primary strength of this research lies in its achievement of a remarkable 70.0% pass rate on the highly challenging PutnamBench, surpassing the existing SOTA by approximately 20 percentage points. This is an extremely strong engineering achievement in the field of formal theorem proving and represents a valuable result for the community.\n\n**Effective Framework Orchestration:** The proposed method effectively combines the strengths of multiple components with different capabilities (Reasoner, Prover, Verifier, Retriever). In particular, the agent design—which coordinates \"recursive subgoal decomposition\" triggered by Prover failure, a \"refinement loop\" using Verifier feedback, and \"contextualization\" via RAG—is sophisticated. It demonstrates a realistic and effective strategy for solving complex problems that a single model cannot solve alone.", "weaknesses": "**Lack of Theoretical Justification:** Although HILBERT is proposed as a controllable framework, it lacks theoretical analysis or guarantees as to \"why this approach works.\" In particular, the paper does not provide a theoretical background for why the core \"recursive subgoal decomposition\" is effective, what problem structures it is suited for, or where its limitations might lie. This absence gives the impression that the work lacks academic depth relative to its engineering success.\n\n**Limited Novelty:** The proposed framework appears to be primarily a sophisticated \"combination\" of ideas seen individually in existing research (e.g., DSP, POETRY, which are cited in the paper), such as subgoal decomposition, Verifier feedback, and RAG. There is no significant novelty in the individual technical elements, making it somewhat unclear what HILBERT's unique core \"Technical Advance\" is when compared to prior work.\n\n**Dependency on Closed Models:** The experiments achieving SOTA rely on a proprietary, closed model (Gemini 2.5 Pro) as the Reasoner. This not only severely undermines the reproducibility of the research, but it also risks effectively closing off the promising future research avenue suggested in the paper's conclusion—\"using the generated proofs to further train the agent (e.g., via reinforcement learning)\"—to the open-source community. This is a significant drawback.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "AMczN2JXq1", "reviewer": "Reviewer_D58n", "summary": "This paper introduces HILBERT, a framework designed to bridge the performance gap between the strong informal reasoning of general-purpose LLMs and specialized prover LLMs. The system includes a general-purpose \"Reasoner\" LLM and a specialized \"Prover\" LLM. When a direct proof attempt by the Prover fails, HILBERT leverages the Reasoner to generate a formal proof sketch, which is then broken down into simpler subgoals. These subgoals are addressed recursively through a hierarchy of strategies: a direct attempt by the Prover, a \"shallow solve\" by the Reasoner, or further decomposition. This method achieves SOTA performance on both MiniF2F and PutnamBench.", "questions": "1. What is the primary conceptual difference between HILBERT's recursive decomposition and the strategies used in POETRY and ProD-RL?\n2. Could the authors provide a failure analysis for the problems HILBERT failed to solve? What were the primary bottlenecks or failure modes?\n3. What is the computational cost (total Reasoner/Prover calls and tokens, similar to Figure 3) for the 70.0% result on PutnamBench?\n4. Why use a pass@184 baseline for Goedel-Prover-V2 on PutnamBench? Is it possible to Evaluate pass@8192 of Goedel-Prover-V2 on PutnamBench?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. HILBERT achieves SOTA performance on MiniF2F (99.2%) and PutnamBench (70.0%), significantly outperforming the existing method.\n2. The framework's design is intuitive and demonstrably effective. Using a powerful informal reasoner to guide a formal prover via recursive subgoal decomposition is a well-motivated approach to tackling complex proofs.\n3. The authors provide a comprehensive evaluation, testing on two standard benchmarks with different combinations of Reasoner and Prover models. The ablation studies validate the contributions of the retriever component and the recursive decomposition strategy. The inference budget analysis provides a better understanding of the performance and cost.", "weaknesses": "1. The core ideas of using informal reasoning to guide formal proof (e.g., DSP [1], LEGO-Prover [2]) and recursive decomposition (e.g., POETRY [3], ProD-RL [4]) are not new. The paper fails to clearly articulate the conceptual difference between HILBERT's decomposition strategy and these existing recursive methods. The contribution appears to be more a highly effective integration and scaling of these ideas with SOTA models rather than a fundamentally new algorithm.\n2. The paper lacks a failure analysis. Does the Reasoner generate flawed informal proofs? Does the sketch-to-subgoal extraction fail? Or does the Prover fail to solve a seemingly simple, decomposed subgoal? Analyzing these failure modes is crucial for understanding the framework's limitations and guiding future work.\n3. The reported SOTA performance is achieved at a significant computational cost. As shown in Figure 3, the best configuration requires up to 4.5K calls to Gemini 2.5 Pro and 11.3K total LLM calls on MiniF2F. The framework's performance is also highly sensitive to the Reasoner's capability, with the weaker Gemini 2.5 Flash showing a substantial performance drop and requiring even more LLM calls (>40K).\n4. The analysis comparing HILBERT to baselines feels incomplete and potentially misleading. Table 2 reports the Goedel-Prover-V2-32B baseline at 13.4% pass@184 on PutnamBench, while Table 1 uses pass@8192 for the same model on MiniF2F. Given that HILBERT's performance relies on an enormous number of calls, this comparison seems unfair.\n5. All computational cost analyses are only for MiniF2F. The paper should include the computational cost required to achieve the 70.0% on PutnamBench.\n\n[1] Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. “Draft, sketch, and prove: Guiding formal theorem provers with informal proofs.” ICLR 2023\n\n[2] Wang, Haiming, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong et al. \"LEGO-Prover: Neural Theorem Proving with Growing Libraries.” ICLR 2024\n\n[3] Lin, Haohan, Zhiqing Sun, Sean Welleck, and Yiming Yang. “Lean-star: Learning to interleave thinking and proving.” ICLR 2025\n\n[4] Dong, Kefan, Arvind Mahankali, and Tengyu Ma. \"Formal theorem proving by rewarding llms to decompose proofs hierarchically.” arxiv", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "WcdvJAvGlt", "reviewer": "Reviewer_eHJ5", "summary": "This paper proposes a framework for ATP which utilizes a LLM for informal reasoning and another LLM for writing the proofs in formal language. The output of the reasoning model is the base for writing the formal proof. Through extensive experiments on miniF2F and PutnamBench, the paper demonstrates that its proposed framework can improve the accuracy of base theorem provers by a significant margin. SoTA LLMs such as Goedel Prover V2 is utilized for theorem proving.", "questions": "Please see weaknesses.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "Results are impressive on Putnam Bench and miniF2F.\n\nAuthors \"plan to release the source code and other artifacts upon publication.\n\nI believe the method will be a useful contribution for the community. This paper seems to me as a good implementation for combining informal and formal reasoning.\n\nPaper is well written.", "weaknesses": "As far as I see in the paper, token budgets are only reported in Table 3 for the ablation of the retrieval module. This is good to understand the effect of retrieval module, however, token budgets are not reported for the main results. This lack of reporting makes the comparisons unclear to me and perhaps unfair.\n\nThe paper's method utilizes a reasoning model to reason about the proof in conjunction with another LLM. Hence, comparing its eventual accuracy directly with the accuracy of a theorem prover that does not benefit from informal reasoning with a large reasoning model seems to me as an incomplete comparison. I would like to see the token budgets reported across the board for all experiments.\n\nOne important question, in my view, is the effect of reasoning model in small number of sampling budgets. For example, consider the accuracy of Goedel Prover V2 8B pass 32 as the base. We have the option to use Hilbert pass 32 to improve the base accuracy. We can also increase the sampling budget of the base model to 64 or 128 without using the Hilbert. What would be the resulting accuracies and the total token budgets in each scenario? It might be the case that Hilbert leads to better accuracy and lower token budget. From the reported results, I could not infer whether Hilbert has such an advantage or not.\n\nI suggest authors perform an ablation study on different modules of their framework not just about the retrieval. \n\nI suggest token budgets be reported separately for each component in the framework, e.g., reasoning model, theorem prover, etc.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)