Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
Authors: Yong Lin
Shange Tang
Bohan Lyu
Ziran Yang
Jui-Hui Chung
Haoyu Zhao
Lai Jiang
Yihan Geng
Jiawei Ge
Jingruo Sun
Jiayun Wu
Jiri Gesi
Ximing Lu
David Acuna
Kaiyu Yang
Hongzhou Lin
Yejin Choi
Danqi Chen
Sanjeev Arora
Chi Jin
Venue: ICLR 2026 Poster (2026)
Keywords: Theorem Proving
Reasoning
Primary area: foundation or frontier models, including LLMs

Abstract: Automated theorem proving (ATP) --- the task of generating a proof that passes automated proof verification given a math question in formal language --- is a critical challenge at the intersection of mathematics and Artificial Intelligence (AI). We introduce Goedel-Prover-V2, a family of two language models that establish a new state-of-the-art (SOTA) in open-source ATP, using the Lean proof assistant. In addition to standard expert iteration and reinforcement learning, our approach incorporates three key innovations: (1) During training when improvement plateaus on human questions, the prover does scaffolded data synthesis to generate synthetic questions of increasing difficulty for its own training; (2) The prover is trained to self-correct  using  Lean compiler feedback; (3) Improved test-time exploration through checkpoint averaging to balance accuracy and diversity. 

Our small model, Goedel-Prover-V2-8B, reaches 84.6\% pass@32 on MiniF2F and outperforms DeepSeek-Prover-V2-671B despite being $80\times$ smaller. Our flagship model, Goedel-Prover-V2-32B, achieves 88.1\% on MiniF2F at pass@32 in standard mode and 90.4\% in self-correction mode, outperforming prior SOTA by a large margin. Additionally, our flagship model solves 86 problems on PutnamBench at pass@184, securing first place among open-source models and surpassing DeepSeek-Prover-V2-671B's record of 47 problems by pass@1024 with about $20\times$ smaller model size and significantly lower compute budget. Our models, code, and data are released at \url{https://github.com/Goedel-LM/Goedel-Prover-V2}.

Published as a conference paper at ICLR 2026
GOEDEL-PROVER- V2: SCALING FORMAL THEOREM PROVING WITH SCAFFOLDED DATA SYNTHESIS AND SELF-CORRECTION
Yong Lin': Shange Tang 2+ Bohan Lyu" Ziran " Jui-Hui Chung
Haoyu Zhao ", Lai Jiang" ", Yihan Geng Jiawei Ge Jingruo Sun',
Jiayun Wu Jiri Gesi i, Ximing Lu", David Acuna,, Kaiyu Yang² 1
Hongzhou Lin + Yejin Choi Danqi Chen', Sanjeev Arora', Chi Jin
Prinnetoo Language and Intelligence, Princeton University 2NVIDIA
TTinggua University *Stanford University Meta FAIR Amazon
7 "Shanghai Jiao Tong University *Peking University
ABSTRACT
Automated theorem proving (ATP) the task of generating a proof that passes automated proof verification given a math question in formal language - is a critical challenge the intersection of mathematics and Artificial Intelligence (AI). We introduce Goodel-Provers
a family of two language models that establish a new sfateoof-the-ar (SOTA) in open-source ATP, using the Lean proof assistant. In addition to standard expert iteration and reinforcement learning, our approach incorporates three key innovations: (I) During training when improvement plateaus human questions, the prover does scaffolded data synthesis to generate syn- thetic questions increasing difficulty for its own training; (2) The prover is trained to self-correct using Lean compiler feedback; (3) Improved test-time explo- ration through checkpoint averaging to balance accuracy and diversity. Our small model, Goedel- V2-8B, reaches 84.6% pass @ 32 MiniF2F and outper- forms DeepSeek- Propseeek-PPove--22--26 BB despite being 80x smaller. Our flagship model, Coedel-Prrver--2-3323 achieves 88.1% on MiniF2F at pass @ 32 in standard mode and 90.4% in self-correction mode, outperforming prior SOTA by a large margin. Additionally, our flagship model solves 86 problems on PutnamBench pass @ 184, securing first place among open-source models and surpassing DeepSeek PeepSeek-Prover- Prover- V2-67 IB's Bss record of 47 problems by pass @ 1024 with about 20x smaller model size and significantly lower compute budget. Our models, code, and data are released https: / //gttttuu com fomm/Goeeeelee Goedel Prover-V2.
INTRODUCTION
Automated theorem proving (ATP) is grand challenge for AI, requiring the construction of step-by- step. machine-veriffee proofs in formal languages like Lean (De Moura et al., 2015; Moura & Ullrich, 2021). The field has advanced rapidly in recent years; for example, AlphaProof (Google DeepMind, 2024), Proverr (Chen et al., 2025) and AlphaGiometty (Trinh al., 2024; Chervonyi et al., 2025) demonstrated that AI systems level performance. While these closed-source frontier models have achieved major leaps in formal theorem proving, they demand extreme-scale compute and remain opaque in their training details. Open-source efforts such as DeepSeek-Prowe Prooceek---rr---Vee V2 (Ren et al., 2025) and Kimina-Prover (Wang al., 2025) have achieved impressive results on benchmarks like MiniF2F (Zheng et al., 2021) and PutnamBent (Tsoukalas et al., 2024), demonstrating the effectiveness of leveraging the reasoning ability of LLMS through chain-of-thoughts Yet, there remains substantial room to further improve both the accuracy and efficiency of open models.
capable of achieving IMO (International Math Olympiad) medal-
* Core Contributor.
This work is independent of and outside of the work at Amazon.
1 All experiments and data processing were conducted outside Meta.

---

Published as a conference paper at ICLR 2026
Serpieal-Provee-22777
Kimins-rrver-88
Boadel-Provar-2--8
Goedie- -V2-228
(Self-Cormecion Modie)
Deepseek-Provee--Vee Prover-V2-67-1
Kimina-rrvve-728
Prdell-Poove-V2-325
MiniF2F
PutnamBench
MathOlympiadBenhh
92.5
60
57
73
90.0
Performance (# solved problems)
Performance (# solved problems)
70
88.1%
50
87.5
44
Perforence (%)
60
85.0
84.0%
84.6%
40
80
82.4%
82.5
30
50
50
80.0
78.3%
20
77.5
75.8%
40
75.0
10
72.5
30
Figure 1: Performance of different models multiple benchmarks under pass @ 32.
We aim to push the boundaries of open-source ATP by building stronger and more efficient models. In this work, we introduce Goedel-Prover-Ve a new series open-source models for automated theorem proving in Lean that establish new state-of-the-e art in both performance and computational efficiency. Given math questions natural language the verifiers generate whole proofs while leveraging verifier feedback for iterative self-correction. Our flagship 32B model achieves 88. 38.1% % pass@32 on the MiniF2F benchmark, improving to 90.4% with self-correction. This performance surpasses both the concurrent 72B Kimina-Prover and the previous SOTA 671B DeepSeek-Provee Prover- V2, while using significantly fewer parameters (Figure 1). On the more challenging PutnamBench, our model solves 44 problems (57 with self-correction), more than doubling the number solved by DeepSeek- DeepSeek-Prover-VV Prover-V2 under the same metric. The efficiency of our approach is further underscored by our 8B model, which alone outperforms the 671B DeepSeek-Proved Prokke-Prve--22 on MiniF2F despite being nearly 80 times smaller. At the time of this submission, Goedel-Prover- V2 achieves the strongest overall performance among all open-source models.
The key to these gains lies in novel design across the framework, data, and training pipelines. We highlight the main components below:
Verifier-guided self-correction: Even humans need multiple attempts to translate their intuitive proof into Lean. Our incorporate feedback from the Lean compiler (verifier) into the model input to enable the error-correction ability of our theorem prover (verifier-guided self-correction). While correcting errors based on verifier feedback has been studied in theorem proving (First et al., 2023) and coding (Olausson et al., 2024; Chen et al., 2024; Bouzenia et al., 2024), we further incorporate this into models that generate long chain-of- thought (CoT) reasoning, which is effective for complex reasoning tasks such as ATP (Jaech et al., 2024; Guo al., 2025; Wang et al., 2025; Ren et al., 2025).
Scaffolded data synthesis: Successfully combining long CoT with verifier- error correction requires special efforts on curating data. In addition to formalizing existing math problems and curating data for error correction, we augment our training statement through scaffolded data synthesis. This technique creates math problems at an appropriate difficulty level to provide the model with better learning signals.
Model averaging: Our training recipe extends beyond standard expert iteration and rein- forcement learning. We also apply model averaging (Wortsman et al., 2022b) to mitigate the decrease in model output diversity that occur in the later stages of training.
Our results demonstrate that the frontier of formal theorem proving attainable within computa- tionally efficient and accessible open-source models. We hope that our open-source theorem prover series, Goedel-Prover- V2, will enable the community to build upon them and accelerate progress toward robust automated solvers that reliably generate formal proof details, thereby allowing human mathematicians to focus on high-level reasoning while offloading the rigorous verification burden AI (Kontorovich, 2025).
2

---

Published as a conference paper at ICLR 2026
2 METHOD
In this section, present our method in detail. We start with the key framework innovation compared to the previous vanilla whole-proof generation methods by utilizing the feedback from the Lean compiler guide the proof-corection procedure (Section 2.1). Then, Section 2.2, demonstrate how to curate the training data (statements). with an emphasis on augmenting the data through scaffolded data synthesis. Based on the curated data, we present the details of training our theorem prover in Section 2.3, which includes supervised fine-tuning (SFT), reinforcement learning (RI.), and model averaging. Section 2.4 provides summary of the overall framework.
2.1 CHAIN-OF-THOUGE AND SELF- COLF-CORRECTION
Prevailing paradigms for whole-pon proof generation in ATP have largely been "end-to-end;" where model simply generates a complete formal proof from theorem statement (Xin et al., 2024b; Lin al., 2025; Dong Ma, 2025). Recent work has significantly advanced this approach by leveraging the long-chain-of-thouge reasoning capabilities of large models (Wang et al., 2025; Ren et al., 2025).
key distinction between informal and formal proof generation lies in the availability and utilization of the feedback from formal compilers. Humans naturally leverage such feedback to iteratively revise their proofs. Recent works have shown that integrating the compiler's verification outcomes into proof generation significantly improves synthesis accuracy (First et al., 2023).
Our framework formalizes this intuition by explicitly incorporating verifier feedback within the whole- proof generation loop. We structure the pipeline so that, after an initial proof attempt, verification failures are parsed and communicated back into the model as corrective guidance. The model then generates proof repairs, leading to iterative self-coorection process.
2.2 CURATING FORMAL STATEMENTS
In this part, we detail our methods for curating a large, high-quality dataset of Lean 4 statements, which essential for expert iteration and RL. We start with the formalizer training, which the core of translating existing math problems written in natural language into Lean statements. We then present our scaffolded data synthesis pipeline that creates math problems at an appropriate difficulty level, which includes lightweight rule-based method that utilizes the Lean system, and an LLM-based system for large-scale data augmentation.
2.2.1 FORMALIZING STATEMENTS WITH REASONING FORMALIZER
Existing Lean datasets like Goedel-Pset-vi (Lin et al., 2025) contain many low-quality problems. Human evaluation on a sampled subset of it shows that over 80% of unsolved problems are incorrectly formalized. This highlights the need for stronger formalizers. We train our formalizer using the standard expert iteration pipeline, which combines Lean syntax checks and semantic evaluation via LLMSs assess translation quality. Only statements that pass both checks are included in the next iteration of SFT.
Table I: Comparison of different formalizers on 300 Omni-mate problems.
Name
Pass
Failed
Kimina- rimiin--atofoormlizzrr
161
139
Goedel--orrmaliee--e
228
72
To initialize expert iteration, we prompt Claude-4-Sonnet to formalize 70K statements with corre- sponding reasoning traces. Incorporating reasoning capability enables our formalizer to outperform previous models such as Soaeddll-Frmaaizee.... V1 and Limina-Autoformalizee, which lack this feature.
The total API cost is approximately $1350.
We evaluate our model, Formel-Formalizer V2 and Kimina- Autoforaiitt on 300 statements from Omni-MATH (Gao al., 2024a). Results shown in Table 1. To validate the reliability of the LLM judge, we performed a human evaluation on 30 problems, which showed 92% agreement between the LLM and human expert. The training and evaluation details are provided in Appendix D.
We use Foreddll-Fraaizze---r V2 to formalize 300K informal statements from the OpenMath ing (OMR) dataset (Moshkov al., 2025) and scaffolded informal statements (see Section 2.2.2).
3

---

Published as a conference paper at ICLR 2026
Chedren sun odd nurss In
Informal Statements Generation
Formalization and Qualitty Checking
Negation and Difficulty Filterng
No 1 E range
induction with zerc -5x -extract_goel
Informal/Formal statements
Formallzer
correctness and simplicity
LLM: Judge
succ extract goal saxry
Solved In Lean?
Whong problem?
Correct syntox?
Negation
theoren initial :
gange 9, (2 , +
12 sozry
simpler problems
harder variants
yes
theoren inductive step
LLM: Check formalization quality
simple?
(k Ni 1th E 3.1
sange
21
g d range ( 11, 0
Generated
Generated formal statements
+)
informal statements
sorry
Figure 2: (Left) Scaffolding from formal proofs with setrrattggoal. (Right) Scaffolding from informal problems, which leverages LLMs to generate informal problems, formalize them, and filter them for difficulty and correctness.
2.2.2 SCAFFOLDED DATA SYNTHESIS
As shown in Figure 2, our scaffolded data synthesis pipeline includes scaffolding from both formal proofs and informal problems.
Rule-based scaffolding. When the prover fails to prove a theorem, we can still leverage the incomplete proof attempt to generate simpler. related problems. The intuition that even an incorrect proof may contain valid subgoals that represent casier lemmas. We use a powerful tactic in Lean, extract -oaal, 1, to capture these unsolved states from proof attempt. These extracted goals, which are well-formed mathematical statements, are then used to augment our training data. Since an extracted statement not guaranteed to provable, we also include its negation, thereby training the model to recognize both true and false propositions.
M.M--baeed scaffolding. Another data synthesis approach to leverage an LLM'' strong natural language reasoning ability to create new problems. For given theorem, we prompt an LLM (Qwen3- 32B) to generate simpler sub- bab-problems if the theorem is unsolved, or harder variants it is already solved. The generated informal statements Bocdel-Formalizer--e V2. To avoid the high inference cost of verifying incorrect or trivial statements, LLM- based filter assess each statement for correctness and difficulty. Trivial statements are discarded, while the negations of incorrect statements are added to the dataset. This filtering process significantly accelerates data synthesis with only minor trade-off in potentially discarding some valid problems due to LLM judgment errors. Further details are in Appendix E.
then formalized using our formalization pipeline with
2.3 TRAINING ALGORITHMS
Supervised fine-tuning and expert iteration. We follow the standard pipeline of Expert Iteration by iterating between using the model conduct large-scale inference on the statement sets, collecting correct proofs with reasoning traces, and fine-tuning the model further on the collected samples. We utilize the open-source framework Llama- Factory (Zheng al., 2024) for model training.
Reinforcement learning. We aim to train a model that can both generate complete proofs and correct its own errors using grifier--uided feedhack. To achieve this efficiently, our RI. implementation adopts a multi-task setup: 50% of the inputs for whole proof generation, and the other 50% for self-correction. We train for a single epoch, using 46K and 67K unique inputs for the 8B and 32B models, respectively. On the algorithmic side, we use hybrid GRPO-based approach (Shao et al., 2024): we remove group normalization as suggested by Gr.RRPO (Liu et al., 2025) to avoid inherent bias on length, incorporate clip-higher, overlong penalties, and dynamic sampling from DAPO (Yu et al., 2025), and exclude the KL regularization term from the objective to encourage exploration. key observation is that question difficulty significantly impacts RL training. To address this,
4

---

Published as a conference paper at ICLR 2026
Inference
SFT
Data
Model
Gioedel-Pser
STP
Desplekk
Distil
Sy-Corect
Qwen
Sy-Comec
Sq
SPT
SFT-S;
Avg.
SET S:
Sy WWoong
Disrill
Correct
(2)
Qwen
Sy Sy-Coreett
SPT-S,
(5)
SP
Sq
S1
SPT
Goedel Pset
Winngg
SFTSS,
SFT-S,-Ag
Avg.
Gioedel chower
V2
SFT-S,-AVe -AVE
SFT-3
OMR
Figure 3: The overall pipeline of model training.
modify the dynamic sampling strategy to only include problems with pass rates in the range (0, 0.75] during optimization. For further implementation details, see Appendix F.1.
Model averaging for enhanced diversity. We observed that in the later stages of SFT and RL, the model's diversity decreases. This is reflected by an increase in pass @ but a decline in pass @N for larger values of N like 32. We adopt model averaging alleviate this issue and enhance model diversity (Wortsman et al., 2022b;a; Lin et al., 2023a;b; Dang et al., 2025). Specifically, let the parameters of the base model be denoted as 0g. and those of the fine-tuned model 0. We the combined model parameters defined as (1 a + a8, where a (0. Existing literature has demonstrated that this simple approach can significantly improve the feature diversity of the final model. Our observations also confirm that this method effectively enhances pass @ N. We perform model averaging each stage of the process. Specifically, we apply model averaging after each iteration of SFT and after RL. We use 0.8 in main experiments.
2.4 WHOLE PIPELINE: PUTTING EVERYTHING TOGETHER
We observe that while DeepSeek-Prowee Prover-Ve V2 models are already heavily trained and have lost self- correction capabilities, other models like Qwen3 lack the ability generate formal proofs. To address this trade-off, we use data distilled from DeepSeek-Prowe Prover- V2 to cold-start Qwen3, followed by large-scale generation of revision and direct proof data with the resulting model. We then train own model and iteratively refine it, incorporating scaffolded data. During training, we observe a reduction in output diversity (a form of overfitting) after each stage and apply model averaging to mitigate this. The whole training pipeline consists of the following steps, as illustrated in Figure 3:
We distill CeepSeck-Prover V2 models on Goedel-Psed and STP (Dong & Ma, 2025), creating the cold-start dataset S1, which includes correct proofs (S1 (S--Coreett) and incorrect ones -Sl-False).
(2) We fine-tune Qwen3 with S -orrret obtain the model SFT-S1-
(3) Using SFT-S1, we perform proof revision on Si-False and shole-proot generation on both Goedel-Pset and OMR. We collect the correct proofs to form dataset S2.
(4) We fine-tune Qwen3 with 930k entries from Si-Correct and S2 to create SFT-S2, Subsequently, perform model averaging between SFT-S, and Qwen3 obtain SFT-S--Avg.
(5) We use SFT-S2-Avg to generate proofs on our synthesized scaffolded statements and OMR. The correct proofs collected to form dataset S3.
(6) We fine-tune SFT-S2-Avg 860k entries from S -orrrre S2, and S₃ yield SFT-S3. We then perform model averaging between SFT-S; and Qwen3 to produce SFT-S3-Avg.
Finally, train SFT-Sy-Avg with RL, apply model average, and obtain the final models.
Compute. We conduct SFT and RL training of the 32B model on 64 GPUs, and the 8B model on 32 GPUs. The total GPU hours for dataset generation is approximately 12k H100 GPU hours. For the 8B model. SFT and RL used 2.3k and 1.3k GPU hours, respectively; the 32B model required 9.2k GPU hours for SFT and 3.9k GPU hours for RI.
5

---

Published as a conference paper at ICLR 2026
Combmatorica: 45
Problem Index
Number theery:
Algebru: 190
1959 1964 1969 1974
1979 1964
1989
1994 1999
2004
2009 2014 2019 2024
Year
Figure 4: Distribution of prob- lems in MathOlympiadBench by category.
Figure 5: Community's 's achievement on IMO problems by year and problem index. Each cell represents a problem: statement not formalized, not solved, and solved.
Decontamination. Comprehensive measures ensure separation between our training data and evaluation benchmarks. First, the source of informal statements, like OMR, has already undergone rigorous decontamination against common mathematical benchmarks. Since formal benchmarks like miniF2F are largely derived from these same informal benchmarks, e.g., MATH, the decontamination of the source informal data provides strong initial safeguard. Second, following standard practices in recent literature (Dong & Ma, 2025), compare the formal statements in the training set and the test set to ensure there's 's no training sample that has an exact string match with the test instances.
EXPERIMENTS
This section presents our experiment results on Goedel-Prover- V2. We first discuss our evaluation benchmarks (Section 3.1). Then, we discuss our main evaluation results on the selected benchmarks (Section 3.3), and correspondingly the scaling behavior (Section 3.5). Finally, we investigate the performance of reinforcement learning and model averaging (Section 3.6).
3.1 BENCHMARKS
MiniF2F. MiniF2F (Zheng et al., 2021) consists of 488 problem statements (244 validation and 244 test problems) in Lean. The problems are drawn from high-school level competitions including the AMC, AIME, and the International Mathematical Olympiad (IMO). We use the version of MiniF2F provided by Kimina (Wang al., 2025)', which has some incorrect statements fixed.
SntmamBench. PutnamBench (Tsoukalas et al., 2024) focuses on college-level mathematics com- petition problems that are sourced from the William Lowell Putnam Mathematical Competition years 1962 2023. PutnamBench comprises 644 problems, covering algebra, analysis, number theory, geometry, combinatorics, probability, and set theory.
To facilitate open evaluation on the most challenging math competition problems, we constructed MathOlympiaddBnnch comprises 360 formalized IMO and IMO short lists problems, sourced from Compfiles and IMOSLLean4 repository 3, It contains 158 IMO problems from 1959 to 2024, 131 IMO shortlist problems covering 2006 to 2023, 68 national mathematical Olympiad problems, and additional mathematical puzzles. The statistic of problem categories in MathOlympiadBBenhh is presented in Figure 4, and Figure visualizes humans' formalizing and solving status of IMO problems in MathhlympiadBench. Appendix A provides more details of MathOlympiadBench and its comparison with MiniF2F.
MathhlyypiadBench.
We also evaluate models FIMO (Liu al., 2023), which comprises problems from IMO Shortlisted problems from 2006 to 2021, and high-school competition problems and undergraduate-level problems.
(Ren et al., 2025) which includes both

---

Published as a conference paper at ICLR 2026
3.2 EVALUATED METHODS
Lean version. The evaluations are done under Lean 4.9.0-rl for fair comparison with previous works (Xin et al., 2024b; Lin et al., 2025; Dong Ma, 2025; Ren et al., 2025).
Table 2: Performance different whole proof gen- eration methods on MiniF2F test split. denotes concurrent work
Method
Budget
Performance
Token budgets. For the first round of whole- proof generation, the max token length of the model is set to be 30,000. For the verifier-guided error-correction, we sequentially conduct 2 ad- ditional rounds of self-correction, given the ver- ifier's feedback on the previous attempt, where the total number of tokens is set to be 40,000. We report the pass@N @N metric.
Seddel-Prover-SFTT
32
57.6% 0.7%
(Lin et al., 2025)
3200
62.7%
STP (Dong & Ma, 2025)
128
61.2% +: 0.6%
3200
65.0% +: 0.5%
25600
67.6%
Simina-Prover-722 (Wang al., 2025)
68.85%
8192
80.74%
SrepScek-Prover-V2
32
75.6% +: 0.5%
(Ren et al., 2025)
8192
82.0%
DeepSeek- Pwrverr-V-667777
32
82.4% + 0.6%
3.3 MAIN RESULTS
8192
88.9%
Kimina -rovnn-P
78.3%
The evaluation results MiniF2F and Putnam- Bench are shown Table and Table 3 re- spectively, the results FIMO and DeepSeek- ProverBench are shown in Table 4. The results for MathOlympiadBench are presented in the rightmost figure of Figure 1, Below, we summa- rize and discuss the results.
Kimina-Proveds Prover--0O''
32
84.0%
(Wang et al., 2025) w/ w/TTRL
1024
87.7%
unknown
92.29%
Goedel- Provee--r V2-8B
32
84.6% =: 0.6%
1024
87.9%
8192
90.2%
seself-correetion
32
86.1% E 0.2%%
1024
89.3%
Goedel-Prover V2-32B
0.8%
High performance at modest scale. Our 32B model achieves pass 32 accuracy of 88. 88.1%
1024
91.8%
8192
92.2%
MiniF2F, with 90.4% after rounds of erro- correction, exceeding the previous state-of-the- art DeepSeek- Bareseck-Proeer--. Trover-V2-67111
selfcoorection
32
90.4% = 0.6%
1024
92.6%
82.4% while
using far fewer parameters. Even the 8B variant
achieves 84.6%, nearly matching or outperforming Kimina-Prrver-70B's results under the same inference budget, and outperforming the previous SOTA DeepSeek- Prover- V2-671B on MiniF2F. with a significantly smaller model size. On PutnamBench, our 32B model solves 43 problems under pass @ 32, nearly doubling the PeepSeeet-Provvr--226777 same budget. With error-correction, Goodeel-Prove--77 outperforming DeepSeck Goedel-Prover-Ve 22B32B solves 86 on PutnamBench, securing the best open-source theorem prover the leaderboard.
model's performance under the solves 57 problems under pass@32. PrepSeck-Prover- Prover- Prover-V2-671BB under pass @ 1024. Under pass 184 and error correction,
Table 3: Comparison of different models on PutnamBench. Our Goedel-Prover-Ve V2 with compiler- guided self-correction solves 86 problems, improving the previous SOTA (DeepSeek-Pront V2) by 39 more problems, and securing the best open open-source model on the leaderboard.
Model
num-solved
open-source
compute
Goedel-Prover V2 (self-correction mode)
86
@ass 184
Goedel-Prover-V2 (self-correction mode)
pass@ 32
Goedel-Prover-VV
43
V
pass @ 32
DeepSeek-Prover V2
47
V
pass 1024
DeepSeck-Prover-V2 DSP+
22
V
pass @ 32
23
pass 128
Kimina-Proven Prover-7B. BB-Distill
pass 192
Self-play Thcorem Prover Goedel-Prood SFF
pass @ 3200
7
@ 512
SeedProver
331
X
unknown
ABEL
7
X
@

---

Published as a conference paper at ICLR 2026
Table 4: Experimental Results FIMO and DeepSeck-ProverBennt Model names abbreviated, where DS is for DeepSeek, Goedel is for Goedel-Prover V2, and rev. is for w/ revision, etc.
Dutaset
DS-V2-7B
Kimina-8B
Kimina-72B
Goedel-8B
Goedel-8B
Goedel-32B
Goedel-32B
FIMO
5.70
3.35
5.70
7.05
7.05
7.05
9.06
ProverBench
0.31
1.38
1.53
1.53
1,53
1.85
2.46
Efficacy of verifier-guided self-correction. Adding self-correction provides consistent gain of approximately 2 percentage points in pass @ 32 for our models on MiniF2F. On PutnamBench, error correction leads to 14 more solves under pass pass@33 32. 32. Moreover, was not explicitly trained with revision, shows negligible improvement (from 75.8% to 76.2%) on MiniF2F with under the self-correction mode. This shows that the self-correction method is primarily effective when the LLM trained to interpret and utilize Lean compiler feedback.
ParSeeek-Proeer:: V2-7B, which
Sample-efficient inference. Unlike prior models such as Kimina-Prover and DeepSeek-Provee V2. which rely heavily on large sampling budgets test-time reinforcement learning reach peak accuracy, Goedel-Prover-V2 attains very high pass@1 with minimal inference overhead (N=32 or 64), indicating that the model internalizes powerful reasoning strategies during training. The sample efficiency, together with the relatively small size, makes Goodel-Provene V2 series a very good candidate for the community develop new algorithms and test different benchmarks.
3.4 ANALYSIS OF SELF-CORRECTION
In our main experiments, self-correction was conducted for maximum of 2 rounds with 40k token context length. To further explore its capabilities, 2024) to extend the context length to 128k to- kens and allowed up 5 revision iterations. We conducted a series of experiments on the MiniF2F benchmark at pass @ 32, the results of which are presented in Figure 6. Alongside our standard prompting setup (Self Correction), we performed two ablation studies: (1) removing the specific compiler етrоr messages (w/o Er- Messages), and (2) removing the chain-of- thought from previous attempts, retaining only the formal proof (w/o Previous CoTs).
95-
used YaRN (Peng et al.,
pass@8192
Accuracy
91
90-
Corrcciinn
80-
wlo Previsus Cals
Enor Messages
2
Revision Iteration
Figure 6: Ablation study on self-correction with extended context length and revision iterations on the MiniF2F test split at pass @2..
The results show that removing compiler feed- back significantly lowers performance, confirming that specific error messages crucial for effective revision. contrast, removing the reasoning from previous attempts yields very minimal performance difference, which suggests that including prior CoT does not substantially improve performance. Since including CoT incurs additional compute cost per task, it may be preferable to omit this infor- mation for greater efficiency. Furthermore, with extended context and more revision iterations, the full self-correction model's pass @22 accuracy on MiniF2F reaches an average of 92.7%, which surpasses the 92.2% performance of the model without self-correction at pass@ a1ss highlighting the efficiency of our iterative revision process.
3.5 SCALING ANALYSIS
Figure 7(a) illustrates the scaling behavior of Goedel-Prover- V2 (8B and 32B variants) across
different inference budgets compared against baselines. At the lower sampling regime (pass @ 32), Goedel-Prover--22-33 already achieves 88.1%, notably surpassing DeepSeek-Prover--22 Proeee---oove--226611 V2-671BB (82.4%) and Kimina-Prover--2 (84.0%). This advantage persists across inference budgets, with our self-correction mode providing approximately 2-point performance improvement under pass @ass@? 32 and pass @64, peaking at 92.6% at pass@8199 masss81122 199. The smaller 8B model also demonstrates strong scalability, surpassing the 671B DeepSeek model at all budgets.
8

---

Published as a conference paper at ICLR 2026
Performance on mini 2F (Pass@K 9%)
91
Performnno on miniFF (80
66
86
83
DeopStek Prover-124TT
Drupoest Phane---n---
Docpöeek Prover V2-78
Despasne
Guode- 825
Goste-Rrovee-e Rex
Goede-Provee 12-00
Gaods-
Gness Grest-Prmee 12-86 Rey
Goste-Provee 92-222
75
Guote-Prvee
Gaode-Phowe-
Gosti-Prove 92-22-22----2 Nav
70
512 Pass (log scale)
512K Output Tokens (log scale)
(a) Performance vs Pass
(b) Performance vs Output Tokens
Figure 7: Scaling behavior MiniF2F test. 'Rev.' denotes 2 rounds of self-correction within 40k context length, 'Ext.' extending the context length to 128k but allowing only the first round generation, and 'Ext. Rev.' demotes 5 rounds of self-correction within 128k context length.
To further analyze efficiency from a compute perspective, consider FLOPs with commonly used estimate model size x output length (Snell et al., 2024). In Figure 7(b), we also incorporate the setting introduced in Section 3.4, extending the context length to 128k tokens and allowing up revision iterations ('Ext. + Rev.). Meanwhile, we also add a baseline that only extends the context rounds of revision ('Ext.). )). The results demonstrate that, for the same
length but does not allow volume of output tokens, Goedel-Prover--V outperforms all baselines, with self-correction yielding further efficiency gains. Notably, while rounds of revision increase the average output length by less than 20%, the model achieves performance on par with doubling the number of passes in the vanilla setting. Furthermore, when extending the context window and allowing more rounds of self-correction, the model at pass @32 surpasses the performance of the vanilla setting at pass @ 8188199 192, despite utilizing only 1/218 of the compute. Comparing 'Ext. Rev.' and 'Ext.' we can also see that simply extending the context length does not help; the improvement comes from revision. This indicates that scaling revision more effective than scaling passes in the vanilla setting.
We provide detailed data of model performance and average output lengths in Appendix B.
3.6 RL AND MODEL AVERAGING
We systematically evaluate the impact of RL steps and model averaging strategies applied to them on the performance of the final models. Specifically, for RL checkpoints steps 60, 80, and 90, we apply model averaging with coefficients = 0.6, 0.7, 0.8, 0.9 (where a is the weight of the base model). We assess each averaged model in both vanilla (whole-proof generation) and correction (with self-correction) settings, evaluating both pass@) I and @ as visualized in Figure 8.
Vanilla Performance
Correction Performance
RL steps
91
steps=60
RL steps=80
90
RL steps=90
pa5s@32 (96)
Averaging
a=0.66
0
a=-.77
0
a=0.80
a=1.00
87
a=1.0 RL steps trend
trend (fixed RL steps)
62.5
65.0
67.5
70.0
72.5
62.5
65.0
67.5
70.0
72.5
Performance
pass@1
pass@1
SeeeSeel-Provee--V
Figure 8: The effects of varying RL steps and model averaging ratios on the pass@) and pass 32 performance, both with and without correction, along with the DeepSeek-Prover- Pronneee--Pove-WWee V2-671B Pro7ee---oo baseline.

---

Published as a conference paper at ICLR 2026
For both vanilla and correction settings, pass I consistently increases the number of RL steps grows. For vanilla pass@N, performance stabilizes at higher RL steps, whereas in the correction setting, pass @ N continues to improve. This indicates that correction benefits more from RL, likely due to the shortage of high-quality self-correction data in the SFT stages.
Examining different values of o; observe that higher proportion of the base model (i.e., lower o) leads to lower pass @ I, but pass@ N first rises and then falls as a increases. There exists an optimal model averaging ratio that maximizes pass @ N, which holds for both vanilla and correction settings.
4 RELATED WORKS
Recent advancements in ATP with LLMs have explored several distinct strategies, apart from raw end-to-end generation (Xin al., 2024a; Lin et al., 2025; Wang et al., 2025), where model simply generates a complete formal proof from a theorem statement.
Proof search methods. To improve correctness over single-pass paggle-passppe generation, many systems employ proof search to incrementally construct proofs with verifier feedback at each step (Wu et al., 2024; Li et al., 2024; Xin et al., 2024b; 2025). Hybrid approaches combine a powerful LLM for high-level sketching with dedicated provers for detailed steps (Cao et al., 2025; Zhou et al., 2025). Similarly, Seed-Prover (Chen et al., 2025) relics on extensive test-time search and refinement, demanding substantial computational resources.
Verifeer-Guided refinement and self-repair. A growing body of work focuses on verifier-guided refinement. Some methods
auxiliary signals, such as informal sketches (Jiang et al., 2023; Gloeckle et al., 2024; Cao et al., 2025) or retrieved theorems (Yang et al., 2024), to guide generation. Another trend enables models to iteratively revise candidate proofs based on feedback Ji al. (2025); Baba et al. (2025); Zhou et al. (2025); Ren et al. (2025); Wang et al. (2025); Chen et al. (2025), improving success rates more efficiently than exhaustive search. Goedel-Prover-V. V2 builds directly on this trajectory by adopting a self-revision framework. It adapts general self-repair paradigms from coding and reasoning (Yao al., 2023; Shinn et al., 2023; First et al., 2023; Olausson al., 2024; Chen et al., 2024; Bouzenia et al., 2024) to the domain of formal mathematics, enabling the model to propose and refine proofs iteratively until they are formally verified.
5 CONCLUSIONS AND FUTURE DIRECTIONS
Even though Soedel-Prover:: V2 advances the SOTA in open-source performance, several promising directions remain for future improvement.
Reasoning versus knowledge retrieval. Our evaluation on ProofNet reveals distinction between cognitive reasoning and library-dependent knowledge (see Appendix G). While our model excels on caasoning-intensive benchmarks, it faces challenges on ProofNet, which emphasizes the utilization of abstract tactics from Mathlib. Our experiments show that while Retrieval-Augmented Generation (RAG) significantly boosts performance on ProofNet, it does not improve (and may even hinder) performance on MiniF2F. This suggests that future models must balance intrinsic reasoning with the ability to dynamically retrieve and apply complex library-speeific tactics, addressing the trade-off between self-contained problem solving and knowledge-intensee formalization.
Generalization across domains and environments. Regarding the domain, current works are influenced by benchmarks like MiniF2F that skew towards algebra and number theory. This introduces topic bias that hinders generalization to underrepresented fields like geometry, combinatorics, and advanced analysis. Integrating rich supervision from textbooks and journals would be beneficial. Regarding the environment, our models are standardized on Lean 4.9. Generalizing to newer Lean and Mathlib versions would allow the model to leverage more powerfull tactics and optimizations, though this requires addressing the challenge of continuously adapting the models to new tactics.
Metacognition and self-improvement, Recent work on LLM metacognition (Didolkar al., 2024) suggests that models can benefit from explicitly reflecting on their reasoning process and augmenting the missing skills. Applying these ideas to theorem proving could allow Goedel-Pron V2 to better assess when its reasoning is on track, when to generate subgoals, or when to seek additional cnormation--otentiaan reducing reliance on brute-force sampling.
10

---

Published as a conference paper at ICLR 2026
ACKNOWLEDGEMENT
This project was the result of a close collaborative effort by all authors, and every major component benefited from joint discussion and iteration. The author would like to thank Igor Gitman for support with the curation of self-correction data.
HZ and SA acknowledge the support from Schmidt, Darpa, ONR, and NSF. CJ acknowledges the support from NSF-OAC-241 1299, NSF-I1S-2239997, and Princeton Al Lab Seed Fund.
REFERENCES
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.1243: 2023.
Kaito Baba, Chaoran Liu, Shuhei Kurita, and Akiyoshi Sannai. Prover agent: An agent-based framework for formal mathematical proofs. arXiv preprint arXiv:2506. 19923, 2025.
Islem Bouzenia, Premkumar Devanbu, and Michael Pradel. Repairagent: An autonomous, Ilm-based agent for program repair. arXiv preprint arXiv:2403, 17134, 2024.
Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, and Fan Yang. Reviving dsp for advanced theorem proving the era of reasoning models. arXiv preprint arXiv:2506.1145 2025.
Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang. Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang, Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, and Thomas Hanwen Zhu. Seed-prover: Deep and broad reasoning for automated theorem proving, 2025. URL atggabbs////eooooooo//gog///oo/p https: arriv.vivvv org/ alss 2507 23726.
Xinyun Chen, Maxwell Lin, Nathanael Schärli, and Denny Zhou. Teaching large language models to self-debug. The Twelfth International Conference on Learning Representations, 2024.
Yuri Chervonyi, Trieu H Trinh, Miroslav Olšák, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Vikas Verma, Quoc V Le, and Thang Luong. Gold-medalist performance in solving olympiad geometry with AlphaGieometry2. arXiv preprint arXiv:2502.03544 2025.
Xingyu Dang, Christina Back, Zico Kolter, and Aditi Raghunathan. Assessing diversity collapse in reasoning. In Scaling Improving Foundation Models without Human Supervision, 2025.
Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction-CADE- 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp. 378-388. Springer, 2015.
Aniket Didolkar, Anirudh Goyal, Nan Rosemary Ke, Siyuan Guo, Michal Valko, Timothy Lillicrap. Danilo Jimenez Rezende, Yoshua Bengio, Michael Ć Mozer, and Sanjeev Arora. Metacognitive capabilities of Ilms: An exploration in mathematical problem solving. Advances in Neural Information Processing Systems, 37:19783-1981 2024.
Kefan Dong and Tengyu Ma. STP: Self-play LLM theorem provers with iterative conjecturing and proving. In International Conference on Machine Learning (ICML), 2025.
Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole- proof generation and repair with large language models. In ACM Joint European Software Engineering Conference and Symposium the Foundations of Software Engineering (ESEC/FSE), 2023.
Bofei Gao, Feifan Song, Zhe Yang, Zefan Cai, Yibo Miao, Qingxiu Dong, Lei Li, Chenghao Ma, Liang Chen, Runxin Xu, et al. Omni- math: A universal olympiad level mathematic benchmark for large language models. arXiv preprint arXiv:2410.07985 2024a.

---

Published as a conference paper at ICLR 2026
Guoxiong Gao, Haocheng Ju, Jiedong Jiang. Zihan Qin, and Bin Dong. A semantic search engine for mathlib4. arXiv preprint arXiv:2403.13310 2024b.
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.
Google DeepMind. matical olympiad problems. ai sil-sovves-ae solves-imo--- peeeepprooosseeeeeeeeeeeeeeeeeee at sat-silverr medla-er-eddllleeeeeeee 2024.
Al achieves silver-medal standard solving international mathe-
https://deepmine http///deppminn.ooogl.... google/ooeeoooooooooooooo discover/blog
Daya Guo, Dejian Yang. Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et Deepseek-rl: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501. 2025.
Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, et al. Openai ol system card. arXiv preprint arXiv:2412.16720, 2024.
Xingguang Ji, Yahui Liu, Qi Wang. Jingyuan Zhang, Yang Yue, Rui Shi, Chenxi Sun, Fuzheng Zhang, Guorui Zhou, and Kun Gai. Leanabell-prover-ee Verifier-integrateed reasoning for formal theorem proving via reinforcement learning. arXiv preprint arXiv:2507.08644 2025.
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023.
Alex Kontorovich. The shape of math to come. arXiv preprint arXiv:2510.15924 2025.
Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang. Tao Yang, and Haitao Mi. Hunyuanprover: scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.2001 20735, 2024.
Yong Lin, Hangyu Lin, Wei Xiong, Shizhe Diao, Jianmeng Liu, Jipeng Zhang, Rui Pan, Haoxiang Wang, Wenbin Hu, Hanning Zhang, et al. Mitigating the alignment tax of rlhf. arXiv preprint arXiv:2309.06233 2023a.
Yong Lin, Lu Tan, Yifan Hao, Honam Wong, Hanze Dong, Weizhong Zhang, Yujiu Yang, and Tong Zhang. Spurious feature diversification improves outo---disttiuttion generalization. arXiv preprint arXiv:2309. 17230, 2023b.
Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang. Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-Prover: A frontier model for open-source automated theorem proving. arXiv preprini arXiv:2502.07640. 2025.
Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309. 039.42309. 04295, 2023.
Zichen Liu, Changyu Chen, Wenjun Li, Penghui Qi, Tianyu Pang, Chao Du, Wee Sun Lee, and Min Lin. Understanding rl -1-zero-like training: A critical perspective. arXiv preprint arXiv:2503.20783, 2025.
Ivan Moshkov, Darragh Hanley, Ivan Sorokin, Shubham Toshniwal, Christof Henkel, Benedikt Schif- ferer, Wei Du, and Igor Gitman. Aimo-2 winning solution: Building state-of-the-art mathematical reasoning models with openmathreasoning dataset. arXiv preprint arXiv:2504. 16891, 2025.
Leonardo de Moura and Sebastian Ullrich. The Lean theorem prover and programming language. In International Conference on Automated Deduction (CADE), 2021.
Theo X. Olausson, Jeevana Priya Inala, Chenglong Wang. Jianfeng Gao, and Armando Solar-Lezama. Is self-repair a silver bullet for code generation? In The Twelfth International Conference on Learning Representations, 2024.
12

---

Published as a conference paper at ICLR 2026
Bowen Peng, Jeffrey Quesnelle, Honglu Fan, and Enrico Shippole. YaRN: Efficient context win- dow extension of large language models. In The Twelfth International Conference on Learning Representations, 2024. URL https: http:///ppeeeeeieeeeeeeeeeeeeeee For.::/e
ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Seepseek-prover-vee Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504221811, 2025.
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, YK Li, Y Wu, et al. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint 2xXi:22402.03000 2024.
Guangming Sheng, Chi Zhang, Zilingfeng Ye, Xibin Wu, Wang Zhang, Ru Zhang, Yanghua Peng. Haibin Lin, and Chuan Wu. Hybridflow: A flexible and efficient rihf framework. arXiv preprint arXiv:
2024.
Noah Shinn, Federico Cassano, Ashwin Gopinath, Karthik R Narasimhan, and Shunyu Yao. Reflexion: language agents with verbal reinforcement learning. In Seirty-seventh Conference on Neural Information Processing Systems, 2023.
Charlie Snell, Jaehoon Lee, Kelvin Xu, and Aviral Kumar. Scaling IIm test-time compute optimally can be more effective than scaling model parameters. arXiv preprint arXiv:2408.033114 2024.
Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625(7995):476-482, 2024.
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin. Michelle Ding, Michael Jennings, Ami- tayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provent on the putnam mathematical competition. arXiv preprint arXiv:2407.1122 2024.
Haiming Wang. Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying. Zekai Zhu, al. Simina--prvee preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.1 / //544 2025.
Mitchell Wortsman, Gabriel Ilharco, Samir Ya Gadre, Rebecca Roelofs, Raphael Gontijo- Ari S Morcos, Hongseok Namkoong, Ali Farhadi, Yair Carmon, Simon Kornblith, al. Model soups: averaging weights of multiple fine-tuned models improves accuracy without increasing inference time. In International conference on machine learning, pp. 23965-239988 PMLR, 2022a.
Mitchell Wortsman, Gabriel Ilharco, Jong Wook Kim, Mike Li, Simon Kornblith, Rebecca Roelofs, Raphael Gontijo Lopes, Hannaneh Hajishirzi, Ali Farhadi, Hongseok Namkoong, et al. Robust fine-tuning of zero-shot models. Proceedings of the IEEF/CVF conference on computer vision and pattern recognition, pp. 7959-7971, 2002_
Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. InternL.M2.5-SSePProvee Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700 2024.
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-provers Advancing theorem proving in 1lms through large-scale synthetic data. arXiv preprint 243.::2405..3333 2024a.
Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang. Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. beepseck-prover-y 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08//5 2024b.
Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Ming Ding. BFS-prover: Scalable best-first tree search for LLM-based automatic theorem proving. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics, 2025.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval- -aggeeeed language models. Advances in Neural Information Processing Systems, 36, 2024.
13

---

Published as a conference paper at ICLR 2026
Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Thomas L. Griffiths, Yuan Cao, and Karthik R Narasimhan. Tree of thoughts: Deliberate problem solving with large language models. In seieth- Conference on Neural Information Processing Systems, 2023.
Qiying Yu, Zheng Zhang, Ruofei Zhu, Yufeng Yuan, Xiaochen Zuo, Yu Yue, Weinan Dai, Tiantian Fan, Gaohong Liu, Lingjun Liu, et al. Dapo: An open-source IIm reinforcement learning system at scale. arXiv preprint arXiv:2503.14476, 2025.
Kunhao Zheng. Jesse Michael Han, and Stanislas Polu. Minif2f: cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.001 10, 2021.
Yaowei Zheng, Richong Zhang, Junhao Zhang, YeYanhan YeYanhan, and Zheyan Luo. Llamafactory: Unified efficient fine-tuning of 100+ language models. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics ( (Volume 3: System Demonstrations), pp. 400-410, 2024.
Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang, Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jie, Xinbo Zhang, et al. Solving formal math problems by decomposition and iterative reflection. arXiv preprint arXiv:2507. 15225, 2025.
14

---

Published as a conference paper at ICLR 2026
APPENDIX
A DETAILS OF MATHOLYMPIADBENCE
Construction. MathOlympiadBenchi is cuman-prooesseed to eliminate several issues presented in the source problems: incomplete problem statements, distribution across multiple files, multiple theorems per problem, and 4. incompatibility with the commonly used Mathlib. The verification process ensures that each problem contains exactly one formal theorem with its corresponding informal statement, and confirms that all formal statements can pass the compilation with the sorry tactic.
Comparison with MiniF2F. There are 20 IMO problems in the test set MiniF2F. We manually examined all problems shared between MathOlympiadBench and MiniF2F and identified 3 cases in MiniF2F exhibiting issues such as: 1. the formal statement to be proved is strictly weaker than the informal statement, and 2. the formal statement does not match the informal statement.
In the following, we present these cases comparing the problem formalizations in MiniF2F and MathOlympiadßench.
A.1 IMO 1981, PROBLEM 6: SPECIFIC VALUE vs. GENERAL FORMULA
MathOlympiadBench
International Mathematical Olympiad 1981, Problem 6
Suppose that N satisfies
MiniF 2F
1) f (0, y) + 1
/--
2) f (x 1, 0) f (x, 1),
The function f(r,)) satisfies
3)
1, y
(x, f
+ 1, y))
4 (1) 100,y)-y-
for all E N.
(2) f(r 1,0) -,0+=,))_(...1
Determine (4, 1981)
8 (3) f(x + (1x++ly+1)== f(x +1,))
-/
for all non-negative integers y,y Determine f(4, 1981).
def no_ eval (x N) N :=
abbrev solution value
-/
17
no no_eval ((2"))(1988) [1984]
12
18
theorem 1981_191_6p___1 (E
N N
19 theorem 1mo1981_p6 (f N + +N+
N)
N)
(ho
Y1
y
Y
(hl : Y, Y
= =
15
(hi :
X
(x
+
1)
x 1)
21
(h2 : x, (x
+ 1)
1)
16
(h2 :
x
Y
f
(x
1)
(y + 1)
22
(h3 : V x y, (x 1) (y 1)
E
11
(x
11
11
23
f (E (x 11 y))
Y,
1y
(E
f 1981 solution_
3)
1=
by
sorry
The informal statement requires computing the exact value of f4, 1981), a specific number. However, the MiniF2F formalization only asks to prove general recurrence relation, which is an intermediate step in the solution process. This discrepancy can make the formal proof substantially easier than solving the original problem. In contrast, MathOlympiadBench faithfully translates the original problem into formal language, requiring the proof of the final numerical value as demanded by the IMO statement.
15

---

Published as a conference paper at ICLR 2026
A.2 IMO 1983, PROBLEM 6: INCOMPLETE vs. FULL CONDITION
MathOlymmiadBench
/-!
International Mathematical Olympiad 1983, Problem 6
Suppose that a, b, are the side lengths of a triangle. Prove that
b c) + clalc a) 2.
Determine when equality occurs.
-/
10
abbrev EqualityCondition (a b
2
R) Prop :-
a =
/-- Let b and be the Lengths the sides of triangle. Prove that
theorem imo1983_p6
(I Affine Affine.Triangle K
(BucliceanSpace K (Fin 2)1) :
3 a abb(a - 6) + 6e((b - c) + ca(c- a) 0.
16 1et a := dist (I.points 1)
(r.points 2)
Determine when equality occurs.
1et b dist (T.points 0)
-/
(T.points 2)
18 let a i= dist (I.points 0)
8 theorem imo 1983
p6 imo_1983
(a b c R)
(T.points 1)
(ho 0 < A
A 0 c)
o < a a"2*b+
b"2+c* (b-e) +
(hi
b) (h2 b
2*2*a> (c-a) A
C)
20 10 = a (a-b) b-2+c+ (b-c)
u
(ha : a aa<bba
(--aa+ +
12
(2 + b (b-c)
21
EqualityCondition a b c) :=
0"2xax(c-a) by
sorry
The informal statement has two parts: proving inequality and determining the condition for equality. The MiniF2F version only formalizes the inequality, completely omitting the second part of the problem. In contrast, MathOlympiadBench provides complete formalization.
16

---

Published as a conference paper at ICLR 2026
IMO 1962, PROBLEM 2: INFORMAL & FORMAL STATEMENT MISMATCH A.3
MatholympiadBench
/-!
MF
International Mathematical Olympiad 1962, Problem 2
Determine all real numbers a which satisfy the inequality:
Determine all real numbers which satisfy
V/3- - - v
v3 V v -/
Show that it is
-1, 1
V127 32
-/
abbrev SolutionSet Set R :-
Seo. (-1) v31
theorem imo__962____ p2 (x R) (ho
< 3 (h1 0 < 1)
(h2 2 Real..ll............ sgrt
11
theorem imo1962 p2 (x : R) :
x E SolutionSet +>
x) Real.aqrt (x + 1)) :111 <
x A < Real.sqrt 31
x S -1 x A 1/2 2
sorry
((++)) sorry
For this problem, the original inequality appears in two different versions one v3
v 1 1 and another as VV3 vx +/++1> > 3. MiniF2F, the informal statement uses the latter (the nested square root version), but the formal statement is based on the former (the simpler difference of square roots), resulting mismatch between the informal and formal statements. In contrast, MathOlympiadBench ensures that both the informal and formal statements consistently correspond to the same version the problem.
2
B SCALING BEHAVIOR
Table 5 reports the performance (%) of Goedel-Prover-Ve V2 (8B and 32B) on MiniF2F under varying inference budgets, both in vanilla and self-correction modes. As shown, self-correction consistently improves accuracy at all compute levels, and both model sizes demonstrate strong scaling behavior.
Model
32
64
128
256
512
1024
2048
4096
8192
32B (self-correction mode)
90.4
91.4
91.9
92.3
92.4
92.6
32B
88.1
89.8
90.5
91.0
91.6
91.8
92.0
92.2
92.2
(self-correction mode)
86.7
86.9
87.4
88.0
88.5
89.3
8B
84.6
86.1
86.5
87.0
87.4
87.9
88.5
89.3
90.2
Table 5; The performance (%) of Goedel-Prover-Vy V2 on MiniF2F across different compute budget.
Table 6 shows the average number of output tokens per sample for each model and revision setting. precise estimate of computational cost, since FLOPs are commonly estimated as model size multiplied by output length. Notably, even with two rounds of revision, the increase in average output length is less than 20% compared to the vanilla setting, showing that self-correction provides efficient use of compute.
These statistics allow for
Model
Vanilla
Revision
Revision
PrepSeek-Prover-V222
3930.8
DeepSeek--Proer--222 V2-67
5588.3
Goedell-rover--22..0
7641.9
8551.0 7587.2
8878.0 7978.2
Spedel-Prover--e
6847.7
Table 6: Average tokens per sample across different models and settings.
PPlaase refer to:
emsol ving.com/wik. w /ineex /tndex.ppp/1/9// hthp/196__1g
17

---

Published as a conference paper at ICLR 2026
As shown, revision-baar based self-correction achieves better performance with only moderate increase in output length, highlighting its computational efficiency.
Overall, these results indicate that Goedel-Provert V2 efficiently internalizes reasoning during training, requiring fewer inference samples and output tokens to achieve comparable or superior accuracy. The consistent gains from parffie-guiide self-correction across all inference budgets underscore the value of combining error correction with
reasoning in formal theorem proving.
C FORMAL NEGATION
We attempt to disprove unsolved statements by proving their logical negation. This is achieved by parsing the Lean statements as follows.
theorem fourIsPrime (a : N) (ha : 4) a.Prime :- by sorry
theorem TourIsPrimeNcg : (a : N) (ha : 4), a.Prime :- by sorry
D DETAILS FOR TRAINING FORMALIZER
We initialize the pipeline by fine-tuning Qwen3-32B on 70K statements distilled from OMR using Claude-4-Sonnee yielding
This model formalizes 300K OMR statements, which are filtered through syntax and semantic checks to create the training set for Fordel-Formalizer- V2.
iterl. Repeating this process results in our final model,
For semantic verification, we employ Qwen3-32B as a judge. We enforce strict consensus mech- anism: a formalization is considered faithful only if the judge approves it across four independent queries.
To validate this judge, we manually evaluated sample of 30 problems. After excluding 5 syntactically incorrect instances, we analyzed the remaining 25. While the LLM correctly rejected 3 inappropriate formalizations, it failed detect 2 subtle errors identified by humans. Overall, this yields a 92% (23/25) agreement rate between the LLM and human annotators, confirming the judge's reliability.
Here is the exact prompt for LLM judging the faithfulness of formalization.
You will receive math problem consisting of its natural language statement along with its formal statement in LEAN 4.
Please evaluate whether the fornal LEAN statement appropriately translates the natural language statement based on the following criteria:
1. Key Elements: The problem's essential components are correctly represented in LEAN code.
2. iathematical Accuracy: The translation preserves the accuracy of the mathematical cal content.
3. Structural Fidelity: The translation aligns closely with the original problem, maintaining its structure and purpose.
4. Comprehensiveness: All assunptions, conditions, and goals present in the natural language statement are included in the LEAN translation.
Your answer should be in the following format:
Thought:
[Your Answer]
Judgement:
[Your Answer, one (Appropriate, Inappropriate!]
The following ng are the example probl labeled for the reasonability of their lranalation.
18

---

x-intercept at 0) other x-intercept at Published as a conference paper at ICLR 2026
Example 1:
## Original natural language statement of the problem:
For the graph of a certain quadratic == ba t the vertex of the
parabola is (2,10), and one of the z-intereopts is (1,0). what is the e-coordinate of the other æ-intercept?
## Translated formal statement: ''lea
theorem quadratic_othert interrrr
intercept
(f
R)
(a p
(h_quad : x, f x * x b 8 + c)
(h_vertex f 10 A V X, f S 2)
-- vertex at (2,10)
(h ih_interceptl f 0)
3 := by (3
Thought:
The Lean translation of the problem is appropriate because it accurately captures the intent and reasoning the criginal problem. The problem's s key elements, such as the vertex, axis of synnetry, and x-intercepts of the quadratio function, are correctly translated into Lean code. The logical flow of the proof mirrors the original reasoning, starting with the symmetry property of the quadratic function and using it to determine the second x-intercept. The mathematical accuracy is preserved, as the proof correctly applies the vertex property and symmetry to arrive at the solution. Furthermore, the translation aligns well with the original problem in natural language, maintaining fidelity to its structure and purpose. Overall, the translation is both faithful and complete, making it an appropriate representation of the original problem.
Judgement: Appropriate
Example 2:
## Original natural language statement of the problem:
Draw tangent line from the point (4,3) to the circle 2x + (v 1)2 =1
What the equation the 1ine that passes through the two tangent points?
## Translated formal statement: 'leen
theorem tangent_ling
(x y RR
let P R
x R := (4, 3) - Point P
let C R
R (2, 1) Center of first circle
let Points (x,y) satisfying both circle equations let on_tirst_circle == (x 2) + - 1)
Radius of first circle
let cirrecond_circle := (x 3) + (y 2)
If point is both circies
on_first_circle on_second_ciiee role
rhen lies on the line 2x 2y 7 2+x 2xy - 7 = by
Thought:
The Lean translation of the problem is inappropriate because it fundamentally changes the intent of the original problem. The original problem asks to derive the equation of the tangent line
19

---

Published as a conference paper at ICLR 2026
passing through the intersection points of two circles, but the translation assumes the equation (2x + 2y - and instead asks to prove that the intersection points lie on this line. This shifts the problem from a construction task to a verification task, losing the original problem's focus on deriving the result through geometric and algebraic reasoning. Additionally, the translation omits the key reasoning step of subtracting the ei rale equations to derive the line equation, which is central to the original problem. As a result, the translation fails to accurately represent the problem's intent and educational value, making it incomplete and inappropriate representation.
is already given
Judgement: Inappropriate
Example3:
## Original natural language statement of the problem:
If a,b,d, and abed = prove that Anln 1 athte+1 + bectat1 + otdta+1 + 4444041 S 1 1 +
I
at3 +
643 043
+ d-3 Anin -/
## Translated formal statement: 'leand
theorem lean_workbook, 49553 (a b d : (habe : a
1)
(1 / (a b +o+ 1) + 1 (b c d 1)
1 (c
+
+
a + 1)
1 (d + a b + +1) S (1 (a + 3) + 1 (b 3) + / (c 3)
(d 3))
by sorry
Thought:
The Lean translation of the problem is inappropriate because the condition a, 0 is ignered in the formal statement.
Judgement:
Inappropriate
Example4:
## Original natural language statement of the problem:
If so Egye = We' prove that 1 the answer.
## Translated formal statement:
'''eean
theorem workbook Alus_1478 (a b K) tha a 21 (ho b 2) 1) -
(he
2 (a
2
2)
(b
2) ...
(c 2) 1 2 : by sorry
Thought:
The Lean translation of the problem is appropriate because it accurately captures the assumptions and the goal in the natural language statement.
oudgement: Appropriate
## Original natural language statement of the problem:
(informal tinformal_statesn 1_stmmmmetttttt
## Translated formal statement:
'''eand
20

---

Published as a conference paper at ICLR 2026
E DETAILS FOR INFORMAL-BASEE SCAFFOLDED DATA SYNTHESIS
In this section, we provide all the details for informal- scaffolded data synthesis. We start with the prompt template for different L.M queries, including the prompt template to generate harder variant, simplet/sub-probbet Then, we provide more details for the synthesis pipeline.
well as the prompt template to judge the simplicity and correctness.
Prompt template for solving the original problem Note that for both input with natural language problem and statement written in Lean, we use the same prompt because we find that general ceneral-purpose models can understand the Lean, although they cannot generate the whole proof correctly.
Solve the following math problem probably writter: in Lean 4: (problem)
Provide a detailed solution. Note that you don't need to prove the problem in Lean 4, just provide a detailed solution in natural language or math notation.
Prompt template for generating sub/simpler problems
I will give you math problem along with its full solution. Your task is generate simpler problems which may enable student to build up the skills to solve the given problem. Each simpler problem should reflect the idea of core step in the solution. Each generated problem must:
(1) Be completely self-containes and standalone, it should be clearly stated
independent question that someone could read and work on without seeing the original problem and the other generated problems.
(2) Be purely proof-based: stated explicitly as question of the form "Prove that...".
(3) Be related to the core steps the solution of the original problem or reflect the core idea, and should not be just a trivial and straightforward derivation, plug-in calculation, or solving simple equations.
After generating the problems, carefully evaluate your own output and perform the following checks:
(1) Ensure each problem is fully self-contained: check that it does not rely on undefined variables, terms, or concepts from the original problem other problems.
(2) Ensure the set of problems is diverse, covering different steps or aspects of the original reasoning.
(3) Ensure that the problems are not too simple or trivial, and that they require meaningful proof. Avoid trivial and straightforward derivation, plug-in calculation, Wrap each final selected problen between the tags <newproblem> and </rewpzoblem> to make it easy to extract. Do not include anything clse. Problem: (problem)
solving simple equations.
Solution: [solution]
Prompt template for generating harder variant of problems
now have math problem and its solution at hand, and would like you to modify the problem to generate a diverse set of new problems based on it. Below is the problem (probably written in Lean 4):
(probl
21

---

Published as a conference paper at ICLR 2026
Below is the solution:
(solution)
Now would like you generate least 10 new math problema, each clearly di fifrent from the original. For example, you can make the following modifications to make the problem different:
Change the number in the original problem to generate a new problem. Transform the algebraic formula such that it needs For example, change cos (x) the original problem inte (x/2)
simplification.
Add more terms to the inequality. For example, the original problem needs to show that (x) is non-negative, you transform the problem into (x) + (1/x a) "2 is non-negative, nogaaeeivv
fxx) \edet "2 is
Lift a real variable into a complex number, vector or even a matrix. For example, previously when solving a quadratic equation in real space, you would now change it to complex fiela, which might lead slightly different solutions. I the original problem considers planar geometry, you modi fy the problem into 3-dimensi onal geometry. Substitute a variable into a more complex a algebraic form, which includes but is not limited to changing variable into
polynomial, exponential, logarithm, or trigoncmetric form. For example, you change variable x the original problem into y'2 or even y'n in the new problem. Another example is that you are given some condition like and you need to show f b, is non-negative. You condition into y + +
b.b + c where a, b, are all positive,
change the = 2 with x, y, positive, which equivalent to 1/x + 1/y 1/z 1, and modify the statement to show that f(1xx, 1/y, 1/2) is non-negative.
Use the conclusion in the problem as step to solve another problem. For example, the original problem needs to solve the equation (x) C, where x the variable. Now you change it to solve E( exp 0.
C, El (x(x) ) 0, or E( cos (x) = 0, or even f( x"2 These are just sore example transformations you can try, and you are not limited to these transformations
not overoomplicate the The
problem, and it is acceptable new math problem should not be simpler than the example problems provided, i.e., you should not simplify the original problem and make it the new problem.
make simple transformations
Each generated problem must:
(1) Be purely proof-based: stated explicitly as question the form "Frove ...thar", Do not generate problems that ask to "determine", "compute", "evaluate", "find", or similar.
(2) Be completely self-contained and standalone.
(3) Be mathematically valid and sol vable...
(4) Be meaningfully different to ensure diversity.
Wrap each generated problem between the tags <newproblem> and </rewproblem> to make it easy to extract. Do not include anything else.
Prompt template to judge the correctness and simplicity the synthesized statement
I will give you a math problem written in Lean 4, and I will ask you to determine (1) whether the problem is correct or not; and (2)
whether the problem is too simple prove disprove in Lean Here is 1ist too simple problems Lean 4: simple
calculations, simple algebraic manipulations, solving single variable linear equations (by just 1-step calculation), and irequalities proved by easy sum-of-squares technique. However not include inequality proving with the square reet since that mi might be more complex. Please do not 1abe1 other problems, such as
22

---

Published as a conference paper at ICLR 2026
other more complex inequalities, limits, and integrals, as simple problems. Also, please do not label problems that deals with integers (more related to number theory), higher order roots, complex numbers, matrices, polynomials, group, finite-sum, or functional equations (e.g. Let f be a function such that fxx (x) for all Win R. Prove that is odd function, i.e., f(-x) (x) for all Win R .), since these problems might shed lights on other hard problems.
Please carefully analyze the probl em and provide an applanation of your reasoning.
For judging the correctness, if the problem is correct, respond with "yes"; the problem incorrect, respond with "no"; if you are not sure, reapond with "unsure".
For judging the simplicity, if the problem is too simple to prove or disprove in Lean 4, respond with "yes"; if the problem is not too simple, respond with "no"; if you "unsure". Please refer to the list of too-simple problems provided.
not sure, respond with
Wrap your judgment between <judge> and </judge> to make it easy to extract. You should first answer yes no to the correctness and then answer yes or no to the simplicity, separatea by comma, For example, if you think the problem is correst and not too simple, you should d respond with <judge>yes, nodgeude If you are not sure about the correctness, you can respond with <judge>unsure, no</judge> because least this problem is not simple. I$ you think the problem is incorrect but it not too easy to disprove, you can respond with <judge>no, no</judge>. If you think the problem is correct but too simple to prove or disprove, you can respond with <judge>yes, yes</Judge>, Again, when judging the simplicity, please not label inequality proving with the square root as simple, since that might be more complex than expected. Please do not include problems such as more complex inequalities, problems that include limits, and integrals. Alsc, please do not label problems that deals with integers (more related to number theory), higher order rosts, complex numbers, matrices,
polynomials, group, finite-sum, or functional equations, as simple problems, since these notions are more likely to related to hard problems and proving problems related to these concepts in Lean 4 might not be easy even the problem straight-forward natural language. Do not include anything else.
Problem:
More details for informal-based scaffolded data synthesis In the following part, we discuss some of the design choices and details for the scaffolded data synthesis pipeline.
1. (Informal statements generation.) For the informal statements generation, one design choice whether to generate multiple questions during the same inference, or to generate multiple times while only generating 1 (or very few) questions during one inference. From our experiment, we observe that for the Qwen3-32B model, generating multiple questions during the same inference is better, since the generated questions are likely to be different. Otherwise, there might be very similar questions among different generations. Besides, we also find that repeatedly generating single problem multiple times doesn't 't significantly increase the number of different problems. Thus, for efficiency considerations, we only query the LLM (Qwen3-32B) once for generating multiple hard variants/simple problems of a given math problem.
2. (Formalization and quality checking.) For each generated informal statement, we call the trained formalizer to formalize the problem twice. Then, we then query Qwen3-8B for times for each formalization, and decide if the formalization is aligned with the informal statement using majority voting (among three queries). We decide to formalize each informal statement twice in order to balance the efficiency and the number of generated problems. We only keep most one formalization for each generated informal statement.
23

---

Published as a conference paper at ICLR 2026
3. (Negation and difficulty filtering,) For each formalization, we query Qwen3-32B for times, where each inference judges the correctness and the simplicity simultancously. The final correctness is judged by strict majority voting among the 4 judges, while the final simplicity is determined if all 4 judges think the problem easy. We use such strict criteria minimize the probability of discarding hard and valuable problems. The efficiency for the judging is high, even if we call Qwen3-32B 4 times for each formalization, since lot of the time Qwen3-32B enters the "fast thinking" mode (no long chain-of-thought for reasoning).
4. (Final deduplication.) At the end of the pipeline, filter out duplicated statements under exact match.
F RL TRAINING DETAILS
We further explain our RL training in detail.
F.1 RL IMPLEMENTATION
Input
Rollout
Vanilla RL
Single-Task
Question
Answer
Complex Design
Tool-a assisassisted RL
Complex Inefficient
Question
Tool Using
Feedback
Answer
Multi-Task
Question
Answer
{
Efficient
Ours
Verifable
Question
Answer
Feedback
Self Self-Correction
Clean Formulation
Figure 9: Illustrative figure for our multi-task RL. This pipeline improves models' performance on both the whole proof and the self-correction the same time without additional design on the framework or algorithm.
We begin by collecting 50K challenging statements and 50K self-correction samples. Each self-correction sample contains a statement, an output generated by the SFT model, and as- sociated error message. During RL training, we consumed approximately 46K and 64K unique inputs for the 8B and 32B models on epoch, respectively. We use the VeRL framework (Sheng et al., 2024) with several key setups: We adopt a batch size 128 and n of for parallel rollouts and reward function calls (via the Lean compiler), while using mini-batch size of 32, accepting certain degree of off-po off-policy training in exchange for a higher frequency of policy optimization. For the dynamic sampling, set the over-sample batch size equal to three times of train batch size and filter out inputs with a pass rate equal to 0 or higher than 0.75. We use maximum prompt length of 16K for those long inputs in the self-correction task. We set the maximum response length 24K support a reasonably sized reasoning trajectory while staying within the Qwen3 model's native 40K context window, ensuring generation quality. We enable the overlong penalty with a 4K overlong buffer and set the overlong penalty factor to 1. We use token-averaged policy loss and do not use KI. divergence or entropy terms in our training objective.
F.2 FURTHER DISCUSSION ON R..
For the design of training with celf-correction, we explored both tool-use and multi-turn reinforcement learning. However, the former not only requires dedicated tool-calling design but also demands strong model capability follow the tool-calling protocol, especially complex and lengthy formal language scenarios like Lean, which is particularly challenging for our relatively small model. Meanwhile, multi-tum approaches introduce various engineering challenges, especially on the rollout engine side, such asynchronous generation. Moreover, the algorithm side, the effectiveness and efficiency of multi-turn RL still require further validation. We have explored some preliminary approaches, but they remain immature. Therefore, adopt straightforward implementation
24

---

Published as a conference paper at ICLR 2026
Self-Corrcctin Traniing Reward
Whole Proof Iraining Reward
0.50
32.33
Nah Muld Moln ho/ Mal m
32.3
0.50
8B
8B
0.63
0.45
0.53
0.50
0.45
0.20
0.40
0.20
0.35
20
60
80
1.00
120
140
40
60
80
1.00
120
140
Whole Proof Ganeration Length
14000
Self Pelf-Corncttio Generation Length
10000
9000
12000
NN
8000
7000
6000
8000
5000
1m
0000
6000
3000
20
100
120
140
1200
Step
Step
Figure 10: Training curves comparing 32B and 8B models: training rewards (top row) and generation lengths (bottom row) for whole proof completion and self-correction tasks. Note that the rewards averaged over all generated rollouts, including those then filtered by the dynamic sampling strategy, thus reflecting the policy improvement.
that is natively integrated into the current RL framework, illustrated in Figure 9. In this setup, we have two different types of inputs for RI, and detailed training curves are shown in Figure 10. Furthermore, for the algorithmic design, like the advantage estimator, we explored different popular GRPO variants but did not observe significant differences.
G PROOFNET AND RETRIEVAL-AUGMENTEE GENERATION.
ProofNet (Azerbayev et al., 2023) focuses on undergraduate-level pure mathematics, with problems drawn primarily from standard undergraduate textbooks covering subjects such real and complex analysis, lincar algebra, abstract algebra, and topology. Notably, ProofNet constructed based mathlib and primarily tests a model's ability memorize and utilize the tactics from mathlib. The experimental results, as shown in Table 7, show that our model does not perform as well as DeepSeek-Prover-V2 ProofNet.
To explore further, we implement a Mathlib RAG Eetrieval-AAummetted Generation). where we gpt-oss- -20 model to generate informal quesies for LeanSearch (Gao al., 2024b). We test the methods on both MiniF2F and ProofNet. Our results show that Mathlib RAG does not help, and may even hurt model's performance on MiniF2F, but it does improve results on ProofNet by large margin, achieving roughly 6-point accuracy gain and reaching the performance of Prrpeeee-Prove--222..
This demonstrates that ProofNet relies more leveraging complex capabilities from mathlib than on cognitive reasoning skills. ProofNet involves a distribution shift and requires advanced mathematical knowledge typically found in Mathlib; while our model does not natively integrate Mathlib well, augmenting with Mathlib retrieval yields strong gains.
25

---

Published as a conference paper at ICLR 2026
Table 7: Comparison of different methods on ProofNet and MiniF2F under pass @ 32.
Method
ProofNet
MiniF2F
Soxdel-Provee--2-3333
22.6%
88.1%
28.5%
86.5%
DeepSeek-Pront Prooeek--rrve-V--
23.0%
75.6%
DeepSeek- Proverr V2-671B
30.5%
82.4%
26


Reviews:
[{"review_id": "SeUBRyl3OC", "reviewer": "Reviewer_sCYS", "summary": "This paper introduces Goedel-Prover-V2, a family of open-source LLMs for Lean4 theorem proving. The framework integrates three key components: (1) large-scale data generation method that enables large and high-quality data generation; (2) verifier-guided self-correction for proofs; (3) model averaging technique that improves the output diversity. The authors report impressive performance of the model, with the 32B version achieving 88.1% pass@32 on MiniF2F-Test and solving 86 problems (13.03%) on PutnamBench under pass@184. The authors commit to releasing all models, training recipes, and datasets to support future research and reproducibility.", "questions": "This work could be more solid and complete if the authors could address the following questions:\n\n1. Generalization to advanced domains: What is the model’s performance on datasets that require more advanced mathematical knowledge, such as FormalIMO and ProofNet? \n2. This paper could also benefit in the sense of reproducibility from a more detailed description of the training process. Specifically, what are the dataset sizes used for S1, S2, and S3 as shown in Figure 3? What are the GPU hours and API costs associated with dataset generation? Furthermore, what is the total GPU hour cost for the SFT and RL stages, respectively, and what hyperparameters were used for model averaging (e.g., the choice of α values)?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "1. Goedel-Prover-V2 achieves impressive performance, with the 32B model achieving 88.1% under pass@32 on MiniF2F-Test and solving 86 problems on PutnamBench at pass@184. The smaller 8B model also outperforms the larger previous model on MiniF2F.\n2. The experiment section is thorough and complete, covering not only core benchmark evaluations but also scaling laws, ablation studies on verifier-guided self-correction, and analysis of model averaging and reinforcement learning dynamics. This allows the readers to more thoroughly understand the effectiveness of each component of the model.\n3. The authors’ plan to release all trained models, the codebase, and the training datasets will be a valuable contribution to the research community.", "weaknesses": "Despite being a thorough and complete work, I believe the paper could benefit from improvements in the following areas:\n\n1. The evaluated datasets primarily focus on domains where the underlying knowledge is relatively elementary but requires the application of many tricky techniques, for example, the PutnamBench. As a result, the model may achieve strong performance by simply memorizing those techniques from larger models, rather than demonstrating true improvements in cognitive reasoning. It would be valuable to evaluate the model on more complex datasets such as ProofNet or FormalIMO to better assess its generalization and reasoning capabilities.\n2. The paper does not disclose the cost of the training and data generation processes in detail, which limits the reproducibility and transparency of the work.", "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": "Kmm0krVBEE", "reviewer": "Reviewer_BEpZ", "summary": "The paper makes several contributions: \n\n- Releasing a LLM for ATP with impressive @32 accuracy on miniF2F and Putnam Bench.\n\n- Releasing another LLM for autoformalization though it remains unclear how well this model performs.\n\n- A training method that involves RL and model averaging.\n\n- Fine tuning the ATP model so that it can do self-correction on flawed proofs.", "questions": "Please see comments above. I'd be happy to revise my score based on the authors' response.\n\nWhy is the release of training set postponed to the near future?\n\nWhat were the deciding factors behind choosing Lean 4.9? Was this choice influenced by the Lean version used by DSP V2? \n\nHave authors evaluated the accuracy of their model using higher versions of Lean? I would guess that if the model is fine tuned on a more recent version of Lean, its accuracy will increase.", "limitations": "", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 2, "contribution": 2, "strengths": "This paper has the potential to be a high impact paper, in my view, if it releases the code for its training method, and releases its training set. If these two items are not released, my recommendation for the paper will be rejection.\n\nThe training algorithm, especially the model averaging method, is a useful contribution, assuming that code will be released with the paper.\n\nThe release of the ATP model is a useful and significant contribution for the community. However, the mere release of the models without releasing the code and training data does not make a direct contribution towards the CFP of ICLR in my view.", "weaknesses": "Accuracy of the autoformalizer model is only evaluated on 300 Omni math problems. First, it is not clear what these problems are. Second, it is not clear how the 300 problems relate to the training set of this model. Paper should report the accuracy of its model on known benchmarks such as miniF2F. If the model is trained on the miniF2F, paper should report that to the reader. Evaluating a new model on a new dataset does not provide sufficient information.\n\nHow is the accuracy of autoformalizer LLM evaluated? Is the evaluation performed by humans familiar with Lean? Or is the evaluation performed automatically using other LLMs?\n\nAlthough Figure 8 provides some insights, it remains unclear to me how much of the gained accuracy is due to model averaging. For example, if there was no model averaging at all, what would the accuracy of the trained model be pass 32? Would it be close to the accuracy of other similar models such as DSPV2 8B model? A clear set of ablation studies may clarify this.\n\nThe effect of self correction module is not reported for other LLMs. It may be the case that the self correction method is only effective if the LLM is trained to take the Lean compiler feedback into account. I think the paper needs to clarify whether this is correct or not. If it has performed any systemic experiments, such results should be reported. Moreover, the self-correction method can be compared against the methods that repair the proofs and do not require fine-tuning the LLM.\n\nToken budgets should also be reported especially for the experiments that involve self-correction. It remains unclear to me how much computational cost is needed for self corrections.\n\nThe paper lacks any analysis of the training set. Given that the training set is largely extracted out of the rival model, DSP V2, one would expect a clear analysis of the training set. Specifically, a direct comparison against the testing set would be helpful. The abstract and introduction make a big point about the accuracy of GPV2 being higher than the accuracy of DSPV2. In my view, it would have made sense to acknowledge that this paper has used DSP V2 as the base to generate part of its training set, i.e., this paper can mention that it has built on the work of DSPV2.\n\nPaper does not contain supplementary material such as code.\n\nPlenty of abstract is repeated in the first two paragraphs of the introduction.", "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": "0Lfc9hiMRD", "reviewer": "Reviewer_5oHs", "summary": "This paper introduces Goedel-Prover-v2, an open-source theorem-proving LLM , using the Lean proof assistant. Goedel-Prover-v2 incorporates RL with three key innovations: verifier-guided self-correction, scaffolded data synthesis, and model (checkpoint) averaging to recover output diversity late in training. Empirically, Goedel-Prover-v2-32B achieves a relatively high performance in existing benchmarks, such as MiniF2F and Putnambench.", "questions": "1. One of the strengths within Goedel-Prover-v2 would be the quality of the dataset. Will the dataset be open sourced upon acceptance?\n\n2. Following on from Weakness 3, is there any manual annotation on the correctness of the filtering and judging?\n\n3. Are there any potential methods to reduce the bias towards components, as we observe that the model is generally weak at geometry, while stronger at some other components?\n\n4. Could integrating lemma generation/retrieval further boost performance?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "This paper introduces a novel method for generating synthetic data, potentially one of the strongest reasons. The model filters out bad autoformalisations, and integrates compiler-feedback self-repair directly into whole-proof generation. The model uses `extract_goal` to capture unsolved states from a proof attempt too. The model introduces an interesting method for improving test-time exploration through checkpoint averaging, potentially balancing accuracy and diversity. Last but not least, the model achieves strong empirical results, requiring fewer pass@n compared to other existing models to achieve greater performance.", "weaknesses": "1. The model primarily focuses on MiniF2F and PutnamBench. While these are widely used, including more datasets in the comparison would be better, including ProofNet-test, AIME, AMC, IMO, and DeepSeek-ProverBench.\n\n2. The model averaging improves pass@n but introduces another hyperparameter without a principled selection rule. A more detailed explanation of this would be great.\n\n3. The data-synthesis filter uses LLM autoformalisation and judging; is there any manual annotation on the correctness of the statement?\n\n4. While the model relies on training reasoning instances, it would be great to provide the average length per dataset compared to the previous goedel-prover. Does including reasoning, while extending the length, improve the performance?", "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": "NmGfznOLQo", "reviewer": "Reviewer_nJcq", "summary": "The authors present Goedel-Prover-V2, a family of two models finetuned for automated theorem proving with Lean. The models were trained through a series of expert iteration and RL, starting with an initial seed generated by DeepSeek-Prover-V2. Additionally, the models were specifically finetuned to be able to incorporate Lean feedback and underwent a weight averaging scheme to increase diversity in the generations of the models. The results indicate that the models outperform prior open-weight alternatives on popular benchmarks like PutnamBench and Mini-F2F.", "questions": "See weaknesses", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The paper present two new models that outperform prior state-of-the-art in an important field of mathematical applications for LLMs (namely, automated proof generation).\n- The training scheme (weight averaging, expert iteration with RL for Lean feedback, ...) is interesting and novel.\n- Goedel-Formalizer-V2 also outperforms prior formalizers.\n- Comparison with prior work is solid and appropriately uses the two most popular benchmarks in this field for the comparison.", "weaknesses": "I am currently giving a 6, since I believe that while the paper presents a strong contribution, there are significant areas of improvement, especially regarding the paper. Most of these weaknesses can be improved during the rebuttal phase, and I therefore see myself increasing my score if they are appropriately addressed. However, for some weaknesses it could also be that their answer will indicate further problems with the paper (especially regarding contamination and the auto-formalizer). If this is the case, I will decrease my score.\n\nI have split the weaknesses in \"weaknesses\" and \"remarks\", where \"remarks\" are smaller points that only affected my rating in a minor way.\n\n**Weaknesses**\n- It is unclear why MathOlympiadBench is included. The results on this benchmark are only given in Figure 1 for three models and are never even discussed in the experimental section. I do agree that the three examples in the Appendix indicate that MathOlympiadBench is better formalized, but it is unclear what proportion of MiniF2F this constitutes and how difficult it was to find such examples. Furthermore, MathOlympiadBench has the distinct disadvantage that its theorems might have been included in training data of other models, since decontamination procedures for these models might not have included the non-overlapping problems with MiniF2F. Overall, I think the inclusion of MathOlympiadBench in its current state decreases the contribution of the paper, as it takes away the focus from Goedel-Prover-V2 and is missing a lot of details regarding experimentation, argumentation why it is necessary to have such a third dataset, and missing explanations regarding its construction (Appendix A is very unclear, as I have no idea how the issues occured, what kind of human evaluation was done, etc.). The authors should either remove the benchmark or make it a complete part of their paper by adding these details.\n- The comparison between feedback and no feedback version of the models is misleading. pass@n with 2 rounds of feedback allow the model to have $3n$ attempts at the problem, not $n$. As such, comparisons should be made between pass@n of the feedback setting with pass@3n of the non-feedback setting. I do note that this is a back-of-the-envelope calculation, as feedback rounds might spend less compute tokens (but it does have more input tokens), but at least the FLOPs between these settings should be matched for proper comparisons. If I look at the numbers, the feedback settings helps much less when one does this more proper comparison (but one cannot entirely tell from the numbers included in the paper alone).\n- It is not mentioned how the results in Table 1 were obtained. If, as I suspect, correctness was verified by the same LLM judge, how can we ensure that the Goedel-Formalizer did not simply learn to fool this LLM judge better? It was specifically finetuned to do better according to this LLM judge, automatically leading to more true positives and false positives. If these results were indeed obtained using the same LLM judge, it would be required to perform another (mabye smaller-scale) evaluation method to compare the formalizers.\n- It is never mentioned where the training data problems were sourced from. Furthermore, it is never mentioned how decontamination with respect to the test benchmark was performed.\n- Currently, no code is included. It would be appreciated if code could be included to verify some of the statements made etc.\n\n**Remarks**\n- I disagree that including CoT in Figure 7 has any influence on performance. The two lines are clearly within 1 standard deviation of each other and the difference is overall very minimal. Furthermore, including the CoT also leads to more compute that needs to be spent per task, indicating that it is likely the opposite case: It is probably better to not include the CoT because it is basically the same performance for less compute.\n- In Figure 8, it is unclear why we are looking at checkpoints rather than the final model. Also, the differences between the different $\\alpha$'s are tiny, and much less clear-cut than what is discussed in the text.\n- I find Section 2 confusing in places. Specifically, the data generation pipeline is very unclear. It should be more clearly mentioned how:\n  - How the data generation pipeline with scaffolding is used in each stage (is it used all the time, only in some stages, when is it used, how is the data generated to check whether it can be solved, ...). \n  - Where the problems were originally sourced from.\n  - Specifically, 2.4 only ever mentions what happens when you have the formalized statements ready, but it is not clear how these formalized statements are obtained in each stage due to the missing details above.\n- The motivation in the first paragraph of the introduction feels a bit off (especially L45-47): Kimina-Prover has the same number of parameters as Goedel-Prover-V2 so the argument does not really hold there. The motivation is much simpler than what presented there (\"we want to create even better models\"). It would be better to incorporate this argument instead.\n- Kimina-Prover should be included in Fig 1 center and right as well.\n- In L98: \"ultimately bridge the long-standing divide between intuitive human reasoning and formal proof verification.\" -> This feels a bit too grand. To do such a thing, one would at the very least need an informalizer as well, or somehow incorporate informal proofs in the formal verification process. I would remove this sentence.\n- L134-136 either needs a citation or an explanation how this evaluation was performed.\n- It is never mentioned which LLM is used to verify formalizations, not even in Appendix C.\n- The caption of Table 1 should be above the table.\n- There is an asterix in the caption of Table 2, but it is never explained why it is there.\n- It is never mentioned which $\\alpha$ was chosen for the final model.\n- The formatting consistency needs to be improved. In one section, the paper uses bullet points without bolded headers, in another it uses bullet points with bolded headers, or just no bullet points and no bolded headers, or just bolded headers. Some of these bolded headers are capitalized, others are not, ... Plots do not have a consistent format. The discrepancy is especially prevalent between Figure 6 and 7 (different background, label size, title vs no title, ...).\n- The writing in the appendix D needs a pass, it contains several typos and grammatical mistakes.", "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)