Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
Authors: Yong Lin
Shange Tang
Bohan Lyu
Jiayun Wu
Hongzhou Lin
Kaiyu Yang
Jia LI
Mengzhou Xia
Danqi Chen
Sanjeev Arora
Chi Jin
Venue: COLM 2025 (2025)
Keywords: Formal reasoning
verification
Lean
self-improvement
TL;DR: Introduce Goedel-Prover, an open-source language model that achieves SOTA in automated theorem proving in Lean

Abstract: We introduce Goedel-Prover, an open-source language model that achieves state-of-the-art performance in automated formal proof generation for mathematical problems.  A key challenge in this field is the scarcity of formalized mathematical statements and proofs, which we address through the following approaches. First, we train statement formalizers to translate natural language math problems from Numina into the formal language Lean 4, and use an LLM to verify that the formal statements accurately preserve the content of the original problems. This results in a dataset of 1.64 million formal statements. We then iteratively build a large dataset of formal proofs by training a series of provers: each prover is able to prove many statements that the previous ones could not, and these new proofs are added to the training set for the next prover. Despite using only supervised fine-tuning, our final prover (fine-tuned on DeepSeek-Prover-V1.5-base) significantly outperforms the previous best open-source model, DeepSeek-Prover-V1.5, which uses reinforcement learning. 
On the MiniF2F benchmark, our model achieves a success rate of 57.6\% (Pass@32), surpassing DeepSeek-Prover-V1.5 by 7.6\%. 
On PutnamBench, Goedel-Prover successfully solves 7 problems (Pass@512), ranking first on the leaderboard. 
Furthermore, it generates 29.7K formal proofs for Lean Workbook problems, nearly doubling the 15.7K produced by prior work. 
We provide extensive discussion of our training methodology, highlighting the key design choices that contribute to Goedel-Prover’s strong performance. Finally, we explore reinforcement learning on top of Goedel-Prover-SFT, offering insights into its potential benefits and limitations.

Published as a conference paper at COLM 2025
Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
Yong Lin*t
Shange Tang**
Bohan Lyut
Jiayun Wut
Hongzhou Lin
Kaiyu Yang"
Jia Lill Mengzhou Xia*
Danqi Chen"
Sanjeev Arora* +
Chi Jin'
Abstract
We introduce Goedel-Prover, open-source language model that achieves state-of-the-art (as of April 5 2025) performance in automated formal proof generation for mathematical problems. A key challenge in this field is the scarcity of formalized mathematical statements and proofs, which we address through the following approaches. First, we train LLMs to convert natural language math problems from the Numina dataset to equivalent formal statements in Lean 4. This process creates the dataset Goedel-Pset- v1, which includes 1.64 million formal statements. Next, we develop large dataset of formal proofs by training a series of provers. Each new prover can prove many statements that previous ones could not, and these new proofs are added to the training set for the next prover. Finally, we obtain the dataset Goedel-Pset-vi 1-soeet----llvdd,,.. which contains proofs for over 800K statements from Goedel-Pset-vl. Supervised fine-tuning (SFT) of DeepSeek- Prover-V1.5-Base on Goedel-Pset-vl
(i.e., no RL) yields model that achieves a success rate of 57.6% (Pass@32) on miniF2F benchmark, surpassing the previous leader DeepSeek-Prover--V
(trained using SFT RL on a proprietary dataset) by 7.6%. On PutnamBench, Goedel-Prover-SFF successfully solves problems (Pass@512), ranking first on the leaderboard. Further RL training (including DPO) improves Goedel-Prover-SFTT' success rate to over 60% (Pass@32) on miniF2F.
To aid future research, we provide an extensive discussion of our training methodology and design choices. We also fully open-source our codes, models, dataset, and formal proofs for 29.7K problems in Lean Workbook, nearly doubling the 15.7K solved by prior provers.
1 Introduction
Recent advancements in large language models (LLMs) have demonstrated remarkable capabilities in reasoning tasks, especially in solving mathematical problems (Guo et al., 2025; Yang et al., 2024a). These models excel at reasoning through natural language, which we refer to informal reasoning. However, natural language-based reasoning is difficult to automatically verify by machines, which undermines the reliability of informal reasoning in practical applications. This also makes it more difficult to further improve the reasoning capabilities of language models. In contrast to informal reasoning, formal reasoning allows reasoning in machine-verifiable format, opening up new possibilities for verification and automation. In particular, proof assistants such as Lean (De Moura et al., 2015; Moura & Ullrich, 2021), Isabelle (Paulson, 1994), and Coq (Barras et al., 1997) provide formal
"YL and ST contribute equally to this work. {yong. 1in, (eraangetang//rinneetett *Princeton Language and Intelligence, Princeton University.
TTsinghua University.
$ Amazon. This work is independent of and outside of the work at Amazon.
9 Meta FAIR. KY served an advisory role, All experiments were conducted on PLI servers.
Numina.
1

---

Published as a conference paper at COLM 2025
Whole Proof Generation miniF2F (Pass6232)
Performance vs Inference Compute
Lean
70
La
5-8-1
Oxepeenk Pr
DeupSesb Prover 5.L
65
Goodel Shoenshhnn SPT
Existing Work
Crepeask Prowert S.
60.3%
60 5%%
Gowar Phroe IPO
F77
Goode: Prover SFT
60
Godde SFT
57.8%
Gouad-hove--f.
30K
OPP
65
Perfomance
50
55
1%
49.0%
50.0%
20K
25K
46
15
15K
40
10K
38
5K
3.2K
25,
102K
30
Models
Pass
0K
Models
Figure (Left) Pass@32 performance on miniF2F for whole-proof generation, compared to previous SOTA models. (Middle) A comparison of Goedel-Proverand DeepSeek-Provee V1.5 on miniF2F performance across varying inference budgets, ranging from Pass@32, 64, 128, ... to 4 x 6400. (Right) In comparison, InternL.M2.5-Stee -.--e---Pre--eeeroooee (Wu et al., 2024) and Intern..MMMath-PM (Ying et al., 2024b) collectively solved 15.7K samples.
solves 29.7K problems in the Lean Workbook.
languages that can express reasoning in a way that can be mechanically verified. Thus, it is of great interest to train LLMs to write proofs in these formal languages.
A significant challenge in training LLMs for theorem proving in formal languages is the scarcity of formalized math statements and proofs. Writing proofs for theorems expressed in formal languages is highly demanding and necessitates considerable domain expertise. Therefore, existing publicly available datasets for formal languages are limited in size. For example, the Lean Workbook (including Lean Workbook Plus) dataset (Ying et al., 2024a; Wu et al., 2024) comprises a total of 140K formal statements, where formal statements refer to problem statements in Lean without proofs. However, only 15.7K of these statements come with formal proofs, which were found by MieenLLM..--StePrrrver and (Ying et al., 2024a; Wu et al., 2024; Ying et al., 2024b). Additionally, the Open Bootstrapped Theorems dataset (Wang et al., 2024) includes 107K statements with proofs sourced from Mathlib4 (mathlib4, 2023). However, Mathlib4 exhibits significant distribution shift from general problem-solving benchmarks, such as the widely used miniF2F (Zheng et al., 2021). See Section 4 for details.
In contrast to the scarcity of data in formal languages, there is a vast amount of math prob- lems and solutions written in informal language. For example, Numina (Li et al., 2024a) in- cludes 860K high-quality question and answer pairs sourced from MATH (Hendrycks et al., 2021), GSM8K (Cobbe et al., 2021), AMC (aop), AIME (MAA, 2024), the AoPS Forum (aop), Chinese K-12 Exams (Shao et al., 2024), World Olympiads, and synthetic data (Mitra et al., 2024). We start by training LLMs to formalize the problem statements in this dataset into Lean. To increase the diversity of the formalization styles, we train two formalizers. One is trained on informal and formal (I-F) statement pairs from Lean Workbook, while the other trained on I-f' statement pairs annotated by Claude-sonnet-3.5 (Anthropic, 2024). We use these two formalizers to formalize the statements and then employ LLMs to ensure that the formal statements preserve the content of the informal statements. Our efforts result in 1.64 million formal statements.
Using this extensive dataset of formal statements, we employ expert iteration (Polu al., 2022) to train the prover to generate proofs. Notably, we train a model to generate complete proofs solely based on statements, without interacting with the Lean compiler during the generation process. This approach is referred to as the whole-proof generation method (Jiang et al., 2022; Wang et al., 2024; Xin et al., 2024a;b). At the beginning of the expert iteration, we generate 16 proof candidates using PrepSeek-Prover-Vi..
(the previous SOTA) for each formal statement in our dataset, and then we verify the correctness of each candidate using Lean compiler. The correct proofs are then collected to train our iter-1 prover based on wowokk--ooveee..-----
In subsequent rounds, we utilize our iter-k prover to collect new proofs and add them to the training data. We then perform supervised fine-tuning
2

---

Published as a conference paper at COLM 2025
Mini22 (Pasoge32)
Numinatst (Pase
ProotNet (Passg)32)
Loan Workbook
Dcasecok Provorat..
62.5
Deepsees Prover v1.5
20.0
2000
17.5
17.5
Purfomanco
Parfoman
55.0
15.0
150
12.5
12.5
90.0
Goedek/hoee-511
Goedee//nveeS5
47.5
Deopsens D RL
5.0
Despsesk Proverv1.5 RL
45.0
6 Model Banition
Model Beration
Model lteration
Model lteestoon
The figures show the performance of our model on the four datasets at each iteration. We gradually increase the size of the problem set and add more training data. The details of each iteration are shown in Table 8.
Figure 2:
starting from DeepSeek-Prove Paiieek--Pove--V...5 V1.5-Base for another round, resulting in the iter-(k + 1) prover. We conduct total of 8 iterations and observe consistent improvement starting from the first iteration.
We demonstrate that expert iteration, with large-scale formalized statements, can lead to SOTA performance in formal proof generation. Specifically,
Our model, Goedel-Prover-SST,, outperforms PeepSeeek-rrove--11.5-44 SOTA model) by 7.6% on miniF2F, achieving a Pass@32 score of 57.6% (i.e., the prover generated 32 proofs for a problem, and 57.6% of the problems have at least one correct proof verified by Lean) compared to DeepSeek- SeepSeek-Prover-ae Figure (left). It consistently surpasses DeepSeck-Prover-11.55 budgets, including Pass@32, 64, and up to 25600, as shown in Figure 1 (middle).
(the previous
50.0%, as shown in across all sampling
We have cumulatively solved 29.7K problems in Lean Workbook, significantly increasing the existing 15.7K proofs found by InternL -Step..rrreeee and InternL.-MMat-PIle (Wu al., 2024; Ying et al., 2024b), as shown in Figure (right).
Goedel-Prover-SFY solves 7 problems on PutnamBench by Pass@512 securing the #1 position on the leaderboard (Table 2).
We open source codes?, models 5.6 datasets? 8, and the new proofs discovered in the Lean Workbook to facilitate future research.
To understand the factors behind Goedel-Prover's strong performance, we provide in-depth discussion of our training recipe, analyzing the effects of scaling up training data, the diversity introduced by autoformalization. correlations among datasets, and alternative data synthesis strategies. Furthermore, although our final model is trained purely through supervised fine-tuning, we also explore direct preference optimization (DPO) and reinforcement learning (RL) techniques built on top of it. Our Goedel-Prover- DPO and Groede-Proveer-A. achieve a success rate over 60% (Pass@32) on miniF2F. However, we also find that DPO and RL-trained models tend to overfit to "shortcuts" and benefit less from increased inference-time compute.
We initially solved 8 problems on PutnamBench. However, after discussing with the authors of PutnamBenee we discovered that one the problems was formaizrd.i.dd. Therefore, this problem not included in our count, and we report a total of 7 problems here.
3

---

Published as a conference paper at COLM 2025
2 Method
We begin by translating informal statements (expressed in natural language) into formal statements (represented in Lean). Using these formal statements, we iteratively train our prover with proofs generated by the prover and verified by the Lean compiler. The details of each step are elaborated the following parts.
2.1 Statement Formalization
We first train the statement formalizers to translate informal statements in Numina into formal statements shown in Figure 3. To enhance the diversity of formalized statements, we train two models to formalize informal statements.
Formalizer A: We train the Formalizer A model using Formal and Informal (F-I) state- ment pairs sourced from Lean Workbook.
Formalizer B: We employ Claude-sonnet-3.5 to formalize 230K statements from Numina. From this set, extract 170K statements that successfully passed Lean compilation. These 170K F-I statement pairs are then used to train Formalizer
Both Formalizer A and B are trained using supervised fine-tuning with Qwen2.5-Coder- T0 The training of these two formalizers takes less than 24 hours on 8 H100 GPUs. See Appendix A.1 for examples of formalized statements from these two formalizers, where we observe that even for the same problem, the style of the formalized statement can impact the prover's 's performance.
(F-I) statement pair
F-I statement pairs
Informal
let by and be real numbers that sstiafying 3 -3, a a430++-- and
a b+ 30 Prove Chal Uhe product abc 36. 36.
theores wihdaatsrra. (a
back.
Formal
-3) Gh b c (ts 3
Qwen2.5-
Training
Formalizer
bba
Coder-32B
Figure 3: This figure illustrates the training of the formalizers. The term "F-1 statement pairs" refers to pairs consisting of Formal and Informal (F-I) statements. An example is shown on the right-hand side. We train two formalizers, Formalizer A and B, using F-I statement pairs sourced from various origins.
Quality assessment. We employ two tests to assess the quality of the formalized state- ments. First, the formalized statement must conform to Lean syntax and can successfully compile, with the potential proof replaced by the placeholder ": by sorry". This syntax check is known the Compiling Correctness (CC) Test in the literature (Ying et al., 2024a). Second, the formalized statement must accurately capture the original informal problem, incorporating all assumptions, conditions, and implicit definitions. We refer this second test as the Faithfulness and Completeness (FC) Test. For the FC test, we use Qwen2.5-72B- Instruct" details are presented in Appendix A.2. We also conducted study comparing LLM and human ratings for the FC test and found an agreement rate 85.7%.
In addition to formalizing the 860K open-sourced Numina (Li et al., 2024a) datasets, we also formalize a private 68K collection of math problems from Art of Problem Solving (AOPS), which has been collected and processed by the Numina group (Li et al., 2024a). Out of total of 928K informal statements, 760K have two valid formalized statements generated by Formalizer A and while 123K contain only one valid formalized statement. After formalizing both the Numina and AOPS datasets, we further incorporate 140K statements
"Phttps://hugginggfacc httttpss//eegiiggaeeee.////////
wwttw/w///wwe....../m 5-Coder- 322B
htttps::///ht "htttss//huuggingffae co/ co//wen/wwwnn2.cmmmmm --722-Instrue
4

---

Published as a conference paper at COLM 2025
from Lean Workbook, including Lean Workbook Plus. As result, we have total of 1.78M formal statements.
2.2 Expert Iteration
After obtaining large collection of formalized statements in Section 2.1, we employ expert iteration to train the prover (Liu et al., 2024; Wu et al., 2024; Li et al., 2024b), which is illustrated in Figure 4. Specifically, 16 proofs for each statement. We then verify these proofs with the Lean compiler. at least one proof solves the statement, we retain one proof per statement. In cases where multiple proofs are available, we randomly sample one solution. These collected proofs are used resulting in the iter-1 prover. We continue this expert iteration process; each time, we use the iter-k prover to generate answers and cumulatively collect correct solutions to train DeepSeek-Prove V1.5-Base for the next iteration, the iter- + +) prover. To prevent data leakage, we ensured that statements in the training set were identical to those in the evaluation benchmarks. Refer to Appendix for more details on each iteration.
first utilize
PrreSeek-Prove--11.555
to generate
for supervised fine-tuning (SFT) based on DeepSeek-Provee Prover-V...---as
We experiment with learning rates of x 10 and 5 x 10 training for either or 2 epochs. We use the packing trick (Tunstall et al., 2022) with small batch size of to speed up the training. In each iteration, the training time for 1 epoch is approximately 12 hours using 4 H100 GPUs. The inference time for the 1.78M statements set by P'as@116 16 is hours, utilizing 64 H100 GPUs. Additionally, the verification time for these proofs requires 10 hours with 8,000 CPUs.
Proof
Formalized statements
Inference
Generated proofs
Proof
Proof 3
Goedel- Prover
LEAN verification
Iterating
Proof
Base Model
Training
Verified
Proof
X X
proofs
Proof
Proof 1
Figure 4: This figure illustrates the process of expert iteration. Each time, we utilize our iter-k prover to collect new proofs and add them to the training data. We then conduct supervised fine-tuning starting from DeepSeek-Prove Proeeek--rrve--i- Palover-V1.5-Bass for another round, resulting the iter-(k + 1) prover.
3 Results
Benchmarks. Following the works of (Wang et al., 2024; Xin al., 2024a; Wu al., 2024; Li et al., 2024b), primarily use miniF2F (Zheng et al., 2021) our main evaluation benchmark. We also track the problems solved by our prover in Lean Workbook (Ying et al., 2024a) and investigate the performance on ProofNet (Azerbayev et al., 2023) and PutnamBench (Tsoukalas et al., 2024). Additionally, we uniformly sample a subset from our formalized dataset to create held-out evaluation dataset. Below, provide descriptions of each dataset.
12nttps://huggingfe http://wwgiinfaaaccccco/eeeeeeee iPhttps://hugginge deepseek wtt///eeseeeeaiaeeeeeeeeeeeooooe D

---

Published as a conference paper at COLM 2025
Whole-Proof Generation Model
Pass
Performance
TheoremLamma (Wang et al., 2024)
128
33.6%
Deepseek-Provers (Xin et al., 2024a)
32
46.1% +: 0.5%
(Xin et al., 2024b)
32
48.2% = 0.6%
DeepSeek-Prover-V1.55 (Xin et al., 2024b)
32
50.0% + 0.5%
Goedel-Prover-SFT
32
57.6% + 0.7%
DeepSeek-Prrove--11.552 (Xin et al., 2024b)
3200
53.3%
Deepseek-Prover-V1---- (Xin et al., 2024b)
3200
54.9%
Goedel-Prover-SFT
3200
62.7%
DeepSeek-Proverr-V1.555 Prover-V1.5-SFF (Xin et al., 2024b)
X 6400
55.8%
DeepSteek-Provee-11---... (Xin et al., 2024b)
X 6400
58.5%
Goedel-Prover-SFT
x 6400
64.7%
Table 1: Whole-proof generation performance on miniF2F.
miniF2F (Zheng et al., 2021) is formal theorem proving benchmark, consisting of 488 problem statements (244 validation and 244 test problems) in Lean. The problems are drawn from high-school exercises, well high-school level competitions including the AIME, AMC, and the International Mathematical Olympiad (IMO). The original benchmark released in Lean 3, and for analysis, use the version of miniF2F in Lean 4.9.0 provided by Xin et al. (2024a).
ProofNet (Azerbayev et al., 2023) is a formal theorem proving benchmark of undergraduate--lve mathematics, consisting of 371 problem statements in Lean (185 validation and 186 test problems). The problems are primarily drawn from undergrad- uate pure mathematics textbooks, covering topics such as real and complex analysis, linear algebra, abstract algebra, and topology. The original benchmark was released in Lean 3, and for our analysis, we use the version of ProofNet in Lean 4.9.0 provided by Xin et al. (2024a).
Lean Workbook (Ying et al., 2024a) is large-scale Lean 4 problem set formalized from natural language math problems (mainly from the forum AOPS), which consists of 140K statements in Lean 4. We also monitor the problems solved by model during the expert iteration process. Notably, the problem set from Lean Workbook is included in this training, which is consistent with PrepSeek-Prover-Vee (Xin et al., 2024a) and Intemm..2.5-SeeeProoer (Wu et al., 2024).
PutnamBench (Tsoukalas et al., 2024) is formal theorem proving benchmark on compe- tition mathematics problems sourced from the William Lowell Putnam Mathematical Competition years 1962 2023. Putnam Beiiaammenchooprisss 644 Lean 4 statements, covering algebra, analysis, number theory, geometry, combinatorics, probability and set theory.
NuminaTest.. We randomly sample 250 statements from our formalized Numina dataset and use them as a held-out testing set. We refer to this subset as NuminaTest..
Main results. The performance on miniF2F is shown in Table 1. The Pass@32 performance of our Goedel-Prover-SFT is 57.6%, surpassing the previous SOTA open source model, by 7.6%. We observe that our Goedel-Prover-SFT'ss Pass@32 even better than PreeSSekk-Provr--Il.5-5.
Pass@3200 by 2.7%. Furthermore, when both evaluated by Pass@3200, our model achieves 62.7%, surpassing DeepSeek-Prover- V1.5- RL's 54.9% by 7.8%. Figure illustrates the inference time scaling curve for our Goedel- Sro, SeepSeek-Prover-- V1.5-LL and DeepSeek- BeerSeek-PPrvee-VVe Provver-V..5-Sh Goedel-Prover-SFT demonstrates significant improvements over both PeepSeek-Prover- Prover-V1.5-SFT across all inference compute budgets. Figure 2 illustrates the performance of our model during each iteration. Overall, we observe a relatively consistent improvement in performance across iterations.
and DeepSeek-
Goedel-Prover-SFT solves out of 644 problems in Putnam- Bench (Pass@512), achieving the first place on the PutnamBench leaderboard. The previous SOTA method ABEL (Gloeckle et al.) solves 7 with slightly higher inference budget
PutnamBench performance.

---

Published as a conference paper at COLM 2025
Ranking
Model
Type
Num-solved
Compute (Pass)
Size
1
Goedel-Prover-SFT]
WPG
7
512
7B
1
ABEL (Gloeckle et al.)
TS
7
596
8B
3
WPG
6
32
7B
3
InternI S225--te (Wu et al, 2024)
xx02
InternLM 7B (Ying al., 2024b)
WPG
4096
6
GPT-4o
WPG
1
10
N/A (API)
7
COPRA (GPT-4o) (Thakur al., 2023)
WPG
1
N/ A (API)
8
ReProver w/ retrieval (Yang et al., 2024b)
WPG
0
1
0.6B
9
ReProver /o retrieval (Yang et al., 2024b)
WPG
0
1
0.6B
Table 2: Number of problems solved on PutnamBench statements (out of 644). Goedel- Prover-SFT achieves the first place the leaderboard. The performance numbers for existing works are taken from the leaderboard. Here inidicates open-source models. Type abbreviations: WPG = Whole-Proof Generation, TS Tree Search Method.
Formalization Model
miniF2F
ProofNet
NuminaTest
Average
Formalizer A only
56.5%
13.8%
59.6%
43.3%
Formalizer B only
56.2%
15.2%
60.0%
43.8%
Formalizer A and B
57.6%
15.2%
61.2%
44.7%
Table 3: An ablation study on using two formalizers to formalize the statements. Using statements formalized by both formalizers improves the model's performance, illustrating the value of diverse formalization styles.
(Pass0596) and Snter-e (Wu et al., 2024) solves (Pass@2 32 600). The performance is summarized in Table 2.
Proofs found in Lean Workbook. The Lean Workbook, which includes Lean Workbook- plus (Ying et al., 2024a; Wu et al., 2024), formalizes 140K high-quality problems sourced from AOPS and the Compfiles data. Currently, proofs for only 15.7K statements in Lean Workbook have been found and made open-source 2024) and InternLM-Math-PPi a significantly larger set of proofs within Lean Workbook, cumulatively solving 29.7K problems, as shown in Figure 1 (right). We open-source all the proofs found by our model to benefit the research community.
M.emLLLM...SttpPrrvw (Wu et al., (Ying et al., 2024b). In contrast, model has discovered
Tactic Usage and Proof Quality. We conducted a detailed analysis the proofs generated by Goedel-Prover- to examine its tactic usage, proof quality, and the sources of its performance gains. We found that its most frequently used tactic is have, which is used to introduce and prove intermediate lemmas, indicating capacity for structured, multi- step reasoning. This contrasts with baseline models that more heavily favor automation tactics like norm.num Furthermore, Goedel-Prover-SFT employs more diverse set of tactics. While powerful automation tactics like linarith and simp are utilized, their frequency of use comparable or even less than baseline models. These findings suggest that the performance gains are due to more nuanced proof strategies and deeper reasoning capabilities, rather than simply exploiting built-in automation. See Appendix for further details the comparison of tactic usage and proof quality.
Dissecting the training recipe
Scaling up the number formal statements improves model performance. Figure shows the performance of provers (average miniF2F, ProofNet and Numina Test) trained on different sizes of the formal statement set. For each statement, the corresponding proof is obtained using performance as the size of the statement set increases, underscoring the value scale in training effective provers.
We observe consistent improvement in model
7

---

Published as a conference paper at COLM 2025
Model
Training Dataset
miniF2F
ProofNet
NuminaTest
Average
Deepseek-RL
50.0%
16.0%
53.6%
39.9%
Iter-6 prover Iter-5 proofs
56.6%
13.3%
59.2%
43.0%
Iter-6 prover proofs + Mathlib4
54.1%
15.6%
58.8%
42.8%
Table 4: Incorporating Mathlib4 into the training data enhances performance ProofNet but reduces performance on miniF2F and Numina Test, suggesting distribution shift between Mathlib4/Prooffet and other datasets.
Correlation Matrix
Pass@32 Performance
mine:
SFT model
1,00
0.86
0.55
-0.51
Average Performance (%)
45
0.5
0.88
1.00
0.81
-0.32
0.4
40
NomivaTedt
35
0.56
0.81
1.00
-0.23
Pesttiel
0.2
-0.51
+0.
-0.20
1,00
-0.4
25
manarge
Lamsektook
HominaTed Teat
Prouhiel
10"
10
10
Size of statement set (log scale)
Figure 5: Model performance under differ- ent sizes of training statement set, illustrat- ing the value of scale.
Figure 6: Correlation of model performance across datasets. ProofNet shows low corre- lation with the others.
Increasing the diversity of formalization styles is beneficial. Table 3 presents the performance of iter-8 provers trained on different formalization styles of statements, with proofs generated by the iter-7 prover. We find that a prover trained on a mix- ture of styles combining statements produced by both Formalizer A and Formalizer B-outperforms provers trained on single formalization style. This result suggests that ex- posure to diverse formalization patterns improves the model's generalization and reasoning ability.
We evaluate model performance across different training iterations and hyperparameter settings, and compute the correlation performance across multiple datasets (see Figure 6). We observe that the model performance on ProofNet is negatively correlated with the perfor- mance on miniF2F, Lean Workbook, and Numina Furthermore, we investigate the effect of including Mathlib4 in the training data. As shown in Table 4, incorporating Mathlib4 improves performance on ProofNet but leads to a performance drop on miniF2F. These findings suggest distribution shift between ProofNet Mathlib4 and the other datasets. Specifically, Mathlib4 and ProofNet tend to focus on the manipulation of mathematical concepts, whereas datasets like miniF2F, Lean Workbook, and Numina Test contain more Olympiad-style problems that emphasize complex reasoning over formal mathematical content. Illustrative examples are provided in Appendix D. Despite the observed distri- bution shift, we continue to include Mathlib4 in the training set from the sixth iteration onward, following the approach of DeepSeek-Provers V1..5er-V..5RL. (Xin et al., 2024b) and Theo- remLamma (Wang et al., 2024), with the aim of enhancing the model's 's general capability across a broader range of mathematical domains. Additional training details can be found in Appendix B.
Alternative approach for data synthesis. In addition to autoformalizing statements and use the prover to provide proofs, we also explored alternative strategies for constructing training datasets, focusing solving difficult problems by a divide-and-conquer strategy.
8

---

Published as a conference paper at COLM 2025
Pass@B32 (minif2f)
Pass@3200 (minif2f)
Average proof length
Average number of tactic "try"
Training method
SFT
57.5%
62.7%
298
1.50
DPO Length-penalized DPO
60.3%
64.6%
486
10.89
59.8%
63.1%
308
1.11
GRPO
60.5%
63.1%
355
5.16
Table 5: Models' behavior under different training methods. RL methods show improvement on miniF2F at Pass@32, but the improvement at Pass@3200 limited. Furthermore, RL models are prone to excessively favor patterns such as try, which also causes the proof length to increase.
Inspired by Jiang et al. (2022), implemented the following pipeline: (1) generate a proof for a formal statement using OpenAl's ol-preview model, (2) extract a high-level "sketch" of the proof and (3) apply DeepSee--Prover-11..A..
to prove the subgoals provided by the sketch. If all the subgoals are successfully completed, we obtain a valid proof for the original problem. Implementation details are provided in Appendix E. However, this pipeline turned out to be ineffective in practice. When applied to the miniF2F validation set (244 problems), successfully solved only 76 problems by
Pookk-Prver--11..5 problems-consideraas considerably fewer than the 158 problems solvable alone. Moreover, out of the 76 problems solved, only one is not solved by PrepSeek-Prover--1.---. implying that the marginal gain from this pipeline is limited.
Exploring DPO and RL training. We further explored DPO and RL training on top of Goedel-Prover-SFI We implemented offline Direct Preference Optimization (DPÒ) (Rafailov et al., 2023) and online Group Relative Policy Optimization (GRPO) (Shao et al., 2024), implementation details are provided in Appendix F. Table 5 shows that although DPO and GRPO improve the model's Pass@32 performance, the average proof length grows substantially, and the frequency of certain patterns increases sharply. This phenomenon indicates that the model is overfitting to some syntactic patterns or "shortcuts", which is related to "reward hacking" (Chen et al., 2024). For example, the Lean tactic try allows trying a tactic and continuing execution regardless of whether it works not. Although often harmless and occasionally useful-its overuse can lead to ineffective proofs and substantial verification costs. The RL-trained model begins to excessively favor this pattern, ultimately impairing its reasoning and generalization capabilities.
Further experiments show that adding a length penalty during DPO training helps reduce this overfitting. However, we observe that scaling up inference-time compute yields sig- nificantly smaller gains for models fine-tuned with either GRPO or length-penalized DPÒ, compared to the SFT model. As shown in Table 5, these models achieve 3% improvement over Goedel-Prover-SFF on Pass@32, but this gain diminishes when increasing inference- time compute-for for example, at Pass@3200. This indicates that RL training may reduce output diversity, leading to less efficient inference- timee scaling.
5 Related Work
Automated theorem proving. Automated theorem proving (ATP) is a long-standing problem in symbolic Al (Robinson & Voronkov, 2001). Traditional approaches represent theorems in first-order logic and prove them using decision procedures (De Moura & Bjorner, 2008; Barbosa al., 2022) and search (Kovács & Voronkov, 2013; Schulz et al., 2019). The proof search has been enhanced by replacing handcrafted heuristics with machine learning techniques (Urban et al., 2011; Kaliszyk et al., 2018). However, approaches based on first- order logic struggle to scale to complex theorems and often do not yield human-readable proofs.
In recent years, learning-based theorem proving has undergone significant transformation. notable approach, introduced by Polu & Sutskever (2020), involves leveraging large language models to assist in theorem proving with proof assistants such as Lean (De Moura

---

Published as a conference paper at COLM 2025
et al., 2015; Moura & Ullrich, 2021) and Isabelle (Paulson, 1994). Follow-up research has explored various avenues, such as retrieving useful lemmas (Irving et al., 2016; Mikula et al., 2024; Yang et al., 2024b), utilizing Monte Carlo tree search for proof discovery (Lample et al., 2022), and harnessing the capabilities of large language models (LLMs) for natural language reasoning (īiang et al., 2022; Lin et al., 2024). Notably, Polu et al. (2023) was the first to apply expert iteration (Anthony et al., 2017) to theorem proving. This method alternates between two phases: (1) attempting to prove unsolved theorems and (2) enhancing the prover by incorporating newly discovered proofs into its training data. Expert iteration has yielded significant improvements in several recent provers (Wu et al., 2024; Xin al., 2024b), including our Goedel-Prover.
Most automated theorem provers operate in a stepwise manner, generating individual proof steps that are then assembled into complete proofs using proof search algorithmss. Recently, researchers have shown that generating entire proofs feasible (First al., 2023; Xin al., 2024a; Wang et al., 2024). This approach avoids the costly search process, resulting in lower latency and potentially offering a more efficient use of computational resources during testing. While Goedel-Prove also generates whole proofs, data and methodology can, in principle, be adapted to develop stepwise provers as well.
Autoformalization and synthetic data generation. The shortage of high-quality formal mathematical data poses a significant bottleneck in training theorem-proving models. While techniques like reinforcement learning may reduce the reliance human-writter proofs (Google DeepMind, 2024), there remains a need for a substantial number of formal theorem statements. A promising approach is synthesize formal statements through autoformalization, where large language models (LLMs) translate informal mathematical statements into formal ones (Wu et al., 2022; 2024; Xin et al., 2024a;b).
DeepSeek-Proves (Xin et al., 2024a) and InternLM2..-StePPrrve (Wu et al., 2024) have successfully implemented this strategy formalize large volume of statements into Lean for expert iteration. We adopt similar approach. The difference is: while Liu et al. (2024) focuses on formalizing their internal dataset, we concentrate on formalizing the Numina dataset (Li et al., 2024a) alongside a privately collected dataset. Additionally, we train two formalizers to enhance the diversity of formalization styles, which we demonstrate to be beneficial in Section 3.
6 Conclusion and Discussion
We introduced Goedel-Prover, a new state-of-the-art open-source model for automated theorem proving. Our main contribution is method to overcome the prevalent issue of data scarcity. By autoformalizing natural language problems and applying expert iteration, created massive dataset of over 800,000 formal statements with verified proofs. Our model, trained via supervised fine-tuning (SFT) on this data, achieves a 57.6% Pass@32 success rate on miniF2F, surpassing the previous leader by 7.6%, and ranks first on the PutnamBench leaderboard. We are open-sourcing our models, code, datasets, and the 29.7K new proofs we found for the Lean Workbook to spur further research.
While we explored reinforcement learning based algorithms (DPO/RL) we found that these methods, despite initial gains, encouraged "reward hacking" (e.g., overfitting to shortcuts like the try tactic) and scaled poorly with increased inference compute. This underscores the robustness of our SFT approach on large-scale, high-quality data.
Future work can build on this strong foundation by incorporating online interaction with the proof assistant for dynamic proof generation, by integrating external symbolic tools like SymPy to handle complex calculations, and by incorporating O1 (Jaech et al., 2024)/R1: R1- like (Guo et al., 2025) long chain-of- offthhughttht capabilities to enhance the model's 's multi-step reasoning abilities when tackling complex theorems. By making we aim to provide a powerful new resource to accelerate progress in open-source automated theorem proving. Detailed discussions are provided in Appendix G.
entire pipeline public,
10

---

Published as a conference paper at COLM 2025
Acknowledgments
CJ acknowledges the support from NSI-OAC-2411299, NST-11S222999 and Princeton Al
Lab Seed Fund. SA acknowledge the support from Schmidt, Darpa, ONR, and NSF.
We thank Haoyu Zhao, Hubert Strauss and Suozhi Huang for their helpful discussions.
References
Art of problem solving wiki. https: http:://aartoforoollmmms///i www/wwki/. Accessed: 2025-01- 24.
Thomas Anthony, Zheng Tian, and David Barber. Thinking fast and slow with deep learning and tree search. In Neural Information Processing Systems (NeurIPS), 2017.
Anthropic. Claude 3.5 sonnet, 2024. URL https://ww.aathhroiccccomm
claude-3-3 -ruude-3-5-onnee sonnet..
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduuate-lvel mathematics. aiv preprint arXiv:2302.12433 2023.
Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. cvc5: A versatile and industrial-strengthh smt solver. In International Conference on Tools and Algorithms for the Consfruction and Analysis of Systems, pp. 415-442, Springer, 2022.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The Coq proof assistant reference manul:: Version 6.1. PhD thesis, Inria, 1997.
Lichang Chen, Chen Zhu, Davit Soselia, Jiuhai Chen, Tianyi Zhou, Tom Goldstein, Heng Huang, Mohammad Shoeybi, and Bryan Catanzaro. Odin: Disentangled reward mitigates hacking in rlhf. arXiv preprint ar Xix:2440..07319, 2024.
Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, al. Training verifiers to solve math word problems. Xiv preprint ar xrXi:22110.14168 2021.
Leonardo De Moura and Nikolaj Bjorner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340. Springer, 2008.
Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction-CADE-22 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Springer, 2015.
Proceedings 25, pp.
Emily First, Markus Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole- generation and repair with large language models. In ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2023.
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 AT at NeurIPS'24.
Google DeepMind. AT achieves silver-medal standard solving international /ttpss:/deepmiinn hww.:pmiinn.ooge/ddideeeeoooomee /oogge///sssoovr//bbllg///// 2024.
mathematical olympiad problems.
Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-rl: Incentivizing reasoning capability in llms via reinforcement learning. Xr preprint arX:::200 12948, 2025.
11

---

Published as a conference paper at COLM 2025
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. ar Xiv preprint arXi::2103.03874, 2021.
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. Advances in neural information processing systems, 29, 2016.
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. Xrviv preprint ar arXio:2412.16720 2024.
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210. 2022.
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. In Neural Information Processing Systems (NeurIPS), volume 31, 2018.
Laura Kovács and Andrei Voronkov. First-order theorem proving and vampire. In Interna- tional Conference on Computer Aided Verification, pp. 1-35. Springer, 2013.
Guillaume Lample, Timothee Lacroix, Marie anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Processing Systems, 2022. URL https://openrevia net
Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Huang, Kashif Rasul, Longhui Yu, Albert Q Jiang, Ziju Shen, et al. Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions. Hugging Face reposilory, 13, 2024a.
Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hun- yuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint ar arXio:2412.20735, 2024b.
Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-STaR: Learning to interleave thinking and proving. arXiv preprint arXit:2407.10044) 2024.
Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, al. Deepseek-v3 technical report. arXiv preprint ar 214:2771..19937, 2024.
MAA. American invitational mathematics examination aime. In American Invita- tional Mathematics Examination AIME 2024, February 2024. URL: https: htt////ma.orro. org/
math-commetiiioos//mmrcccam http://mmrmrrniiiiiittttttaaaaaa www.eommaaammmtttaaaaeaaaatteeee www.iisieeiiiiioo----- aime.
mathlib4. mathlib4: The math library of lean 4, 2023. URL https://githhn www.iittbb.oo..o.. com/ leanprover-communityy cotommunity//mtthibb4 Accessed: 2025-01-14.
Aaron Meurer, Christopher Smith, Mateusz Paprocki, Ondřej Čertík, Sergey Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K Moore, Sartaj Singh, et al. Sympy: symbolic computing in python. Peer] Computer Science, 3te103, 2017.
Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Q Jiang, Jin Peng Zhou, Christian Szegedy, Lukasz Kuciñski, Piotr Miloš, and Yuhuai Wu. Magnushammer: A transformmer-bsed approach to premise selection. International Conference on Learning Representations (ICLR), 2024.
Arindam Mitra, Hamed Khanpour, Corby Rosset, and Ahmed Awadallah. Orca-math: Unlocking the potential of sims in grade school math. arXio preprint arXiv:2402.14830, 2024.
12

---

Published as a conference paper at COLM 2025
Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming
language. In International Conference on Automated Deduction (CADE), 2021.
Lawrence C Paulson. Isabelle: A generic theorem prover. 1994.
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. ar Xiv preprint är arXi::2009.03393, 2020.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint ar arXie:2202.01344, 2022.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and llya
Sutskever. Formal mathematics statement curriculum learning. In International Conference on Learning Representations (ICLR), 2023.
Rafael Rafailov, Archit Sharma, Eric Mitchell, Christopher D Manning, Stefano Ermon, and Chelsea Finn. Direct preference optimization: Your language model is secretly reward model. Advances in Neural Information Processing Systems, 36:53728 28-2444 2023.
Alan JA Robinson and Andrei Voronkov. Handbook of automated reasoning, volume 1. 2001.
Stephan Schulz, Simon Cruanes, and Petar Vukmirović. Faster, higher, stronger: 2.3. In International Conference on Automated Deduction (CADE), 2019.
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 ar ktw::442.03300, 2024.
Amitayush Thakur, Yeming Wen, and Swarat Chaudhuri. A language-agent approach to formal theorem-proving. Xiv preprint ar arXiv:2310.0435. 2023.
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem- provers on the putnam mathematical competition. ar Xiviv preprint ar arXio:2407.11 11214, 2024.
Lewis Tunstall, Leandro Von Werra, and Thomas Wolf. Natural language processing with transformers. O'Reilly Media, Inc.", 2022.
Josef Urban, Jiří Vyskočil, and Petr Stěpánek. MaLeCoP machine learning connection prover. In International Conference on Aulomated Reasoning with Analytic Tableaux and Related Methods, 2011.
Ruida Wang, lipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theoremilama: Transforming general-purpose Ilms into lean4 experts. arxio preprint arXiv:2407.03203, 2024.
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Processing Systems, 2022. URL https: hitps://opeens http///wpeeeeee.eeeeeeeeeee ftw.ee.etooorrmm/ii IUikebJ1Bf0.
Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. SttemmLM2.--ttePPooeer Advancing automated theorem proving via expert iteration on large-scale lean problems. Xiv preprint ar xriv:24400115700 2024.
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in 1lms through large-scale synthetic data. ar Xiv preprint arXiv:2405.1433 2024a.
Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Dl 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arv preprint *Xit:2408.08152. 2024b.
13

---

Published as a conference paper at COLM 2025
An Yang, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chengyuan Li, Dayiheng Liu, Fei Huang, Haoran Wei, et al. Qwen2. technical report. arxio preprint #Xii:2442.155115, 2024a.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with aetreetalaugmmented language models. Advances in Neural Information Processing Systems, 36, 2024b.
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean work- book: A large-scale lean problem set formalized from natural language math problems. arXiv preprint 40X4:2200.03847, 2024a.
Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. Internlm-math: Open math large language models toward verifiable reasoning. ar preprint ar arXiv:2402.06332, 2024b.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arv preprint ar Xiee21009.0,,,,,, 2021.
14

---

Published as a conference paper at COLM 2025
Appendix
A Statement Formalization Details
A.1 Examples of formalized statements
Table 6 presents two examples in which both Formalizer and Formalizer B yield reasonable formalizations. However, our final prover exhibits varying performance these formalized statements, highlighting the influence of formalization style on model effectiveness.
Example
Example 2
Informal Statement
The function f(x) = 2 3x2 +
and log10 x are real numbers and log x <
ax is an even function, then equals = O.
show that <
<<<<1 1.
theoren lab_style_ekamplet (a R)
tel.style..xanple2
(f
(a axaa R)
2tabs (hs 1. (-x) x)
Regl. x
(hr 0 sarry
Formalizer A Output
a=0 te by sarry
Pass rate: 14/16
Pass rate: 0/16
def IsEvon R a R) Prop :- 7 (-x)
theorem sommet.style.cxample. (f : B)- (hudef K.K, x 2*([x]) 3ex*2 sex (hLeven IsEven f) R)
theorer sonnet_style.exapte
[x a
10fa)
a 8<xAax1 by sorry
Formalizer B Output
serry
Pass rate: 0/16
Pass rate: 5/16
Table 6: Comparison of formalizer outputs for two examples. Example 1, Formalizer A defines the "even function" directly by stating f(-x) fx). In contrast, Formalizer B first introduces function called "IsEven" and then defines the even function using "IsEven" Notably, our prover successfully solves the statements provided by Formalizer A but fails with those from Formalizer B. Example is similar; however, our prover fails to solve the statement provided by Formalizer A but succeeds with the one from Formalizer B.
A.2 Quality Assessment Details
For the FC test, we use Qwen2.5-72BIInstruud with prompt shown in Figure 7. For each formalized statement, generate four independent judgments, and the FC score is calculated as #[" Appropriate" in four Judgments}/ / /4. For example, if the four judgments produced by
include three "Appropriate" and one "Inappropriate"" the overall FC score is calculated as 0.75. We filter out formalized statements with an FC score less than 0.5.
For each informal statement in Numina, we generate eight formalized statements from each formalizer, resulting in 16 formalized statements per problem. Each statement undergoes the CC and FC Test, and we retain only those valid statements. We then randomly select one valid statement from each formalizer. For example, five out of eight statements from Formalizer A and three from Formalizer B are valid, randomly choose one from each. If a formalizer produces no valid statements, we exclude all its statements for that problem. The statistics for each test conducted on both formalizers are summarized in Table 7.
B Expert Iteration Details
The main training pipeline is illustrated in Section 2.2. When we implement the expert iteration algorithm, we gradually add the data. From iter-0 to iter-3, gradually add
h wwttwee//wwe2..e55e5e Instruct
15

---

Published as a conference paper at COLM 2025
You will receive math problem consisting of its natural language statement and, in some cases, natural language proof or solution, along with its formal statement in LEAN 4.
Please evaluate whether the formal 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. Mathematical Accuracy: The translation preserves the accuracy of the mathematical content.
3. Structural Fidelity: The translation aligns closely with the original problem, maintaining its structure and purpose.
4. Comprehensiveness: assumptions, conditions, and goals present the natural language statement are included in the translation.
should be in the following fornat:
Thought: [Your Answer]
Judgement:
[Your Answer, one of (Appropriate, Inappropriate]]
Figure 7: Prompts for Faithfulness and Completeness (FC) Test.
Model
Pass
Formalizer A
Formalizer
CC Test
Pass@1
76.74%
88.48%
CC Test
Pass@8
95.93%
98.59%
FC Test
Pass@1
48.06%
80.42%
FC Test
Pass@8
88.01%
97.22%
CC + FC Test
Pass@1 Pass@8
45.72% 82.33%
76.41%
CC + FC Test
95.78%
Table Quality assessment of the formalized statement
the statements formalized by Claude-sonnet-33. At iter-3, train the Formalizer B and add the formalized statements generated by Formalizer for iter-4 to iter-6. At iter-7, we begin add the statements generated by Formalizer A. We also add Mathlib4 data into the training dataset for better Prooffett performance when starting from iter-6.
Statements
Training Data Formalized Solved
Iteration
Lean Workbook
Formalized
Lean Workbook Solved
Mathlib4
Iter-0
140K
20.6K
0
Iter-1
140K
20.6K
72.4K
Iter-2
140K
270K
23.0K
128.7K
Iter-3
140K
270K
24.4K
161.2K
Iter-4
140K
882K
25.4K
425.8K
Iter-5
140K
882K
27.0K
436.5K
Iter-6
140K
882K
27.8K
443.2K
104K
Iter-7
140K
1.64M
28.8K
887.7K
104K
Iter-8
140K
1.64M
29.7K
915.7K
104K
Iter-9
140K
1.64M
30.3K
928.2K
104K
Table 8: Expert iteration details.
16

---

Published as a conference paper at COLM 2025
C Analysis of Tactic Usage and Proof Quality
In this section, provide detailed analysis of the proofs generated by Goedel-Prover-SFF focusing on the diversity of tactics used, the reliance on high-level automation, and overall proof quality. This analysis studies whether performance improvements of model might solely stem from better exploitation of Lean's 's built-in automation rather than from enhanced reasoning capabilities. We compare our model against the DeepSeek-Prover-VV RL baseline on the miniF2F benchmark.
C.1 Tactic Diversity and Frequency
To understand the strategic differences between the models, we first examine the most frequently used tactics. Table 9 lists the top 10 tactics for both Goedel-Prover-SFF and the baseline. Notably, the most used tactic for our model is have, which is crucial for constructing structured proofs by introducing and proving intermediate lemmas. This contrasts with the baseline, which most frequently uses norm num, powerful but more opaque automation tactic. This suggests that Goedel-Prover-Se
not simply overusing automated tactics but is capable of producing more interpretable and structured proofs.
Prapseek-Prover-11551..
Goedel-Prover--FI
Rank
Tactic
Count
%
Tactic
Count
%
1
nom
193
18.9%
have
200
16.8%
2
have
121
11.9%
linarith
116
9.7%
3
linarith
94
9.2%
96
8.1%
4
simp
52
5.1%
simp all
54
4.5%
5
decide
42
4.1%
simp
49
4.1%
6
simp_all
35
3.4%
only
44
3.7%
7
omega
30
2.9%
omega
36
3.0%
8
only
30
2.9%
nlinarith
32
2.7%
9
with
25
2.5%
ring-m nf
28
2.4%
10
nlinarith
23
2.3%
Finset
27
2.3%
Table 9: Top 10 most-used tactics on miniF2F for Goedel-Prover-SFT and the baseline.
Furthermore, Table 10 provides a direct comparison of the usage of common high-level automation tactics. For most of these tactics, Prover-Prove--SFT either uses them less frequently or at similar rate the baseline. This evidence further supports the conclusion that our model's improved performance comes from more nuanced and varied proof strategies rather than simple over-reliance automation.
DeepSeek-Prover-Vl..A.
Goedel-Prover-SFTT
Tactic
Count
% of Proofs
Avg per Proof
Count
% of Proofs
Avg per Proof
aesop
0
0%
0
1
0.7%
0.01
decide
42
8.1%
0.34
21
4.9%
0.15
linarith
94
40.7%
0.76
116
33.1% %
0.82
nlinarith
23
13.0%
0.19
32
19.0%
0.23
norm num
193
46.3%
1.57
96
43.7%
0.68
omega
30
17.1%
0.24
36
20.4%
0.25
ring
8.1%
0.09
20
9.9%
0.14
simp
52
30.1%
0.42
49
26.1%
0.35
Table 10: Frequency of common high-level automation tactics used in successful proofs on miniF2F.
17

---

Published as a conference paper at COLM 2025
C.2 Problem Difficulty and Proof Complexity
To assess whether Goedel-Prover--e is solving more difficult problems, we analyze the length of the generated proofs and the number of solved problems from challenging com- petition sources like AIME and AMC. As shown in Table 11, Goedel-Provver-FFT not only solves more problems overall but also generates higher proportion of multi-step proofs (>33 lines) and solves more problems from the AIME and AMC categories. This indicates that our model indeed tackling more complex problems that require deeper reasoning.
Model
Total Solved
1 line
2-3 lines
>3 lines
AMC/ AIME Solved
123
6
31
86
15
Goedel-Prover-SFT
142
10
37
95
19
Table 11: Analysis of proof length and problem difficulty miniF2F.
Finally, we examined the overall diversity of tactics employed by each model, as summarized in Table 12. Goedel-Prover-Sh utilizes a significantly broader range of unique tactics, further demonstrating its ability to formulate more varied and sophisticated proof strategies. This wider tactical repertoire allows it to address a broader spectrum of mathematical challenges beyond those solvable by more limited set of automated tactics.
Model
Total Proofs
Total Tactics Used
Unique Tactics
PhepSeek-Prover-V..3 Goedel-Prover-SFT
123
1019
112
142
1190
158
Table 12: Tactic diversity in successful proofs on miniF2F.
D More examples on style difference
D.1 Mathlib4 and miniF2F
We observe a notable difference in the distribution of Mathlib4 compared to that of general problem-solving benchmarks, such as the widely used miniF2F (Zheng et al., 2021). For instance, miniF2F largely consist of competition and Olympic-style problems, which require complex reasoning, while only depending integers, real numbers, counting, and geometry. On the contrary the statements in Mathlib4 focus the simple manipulation of advanced mathematical concepts. Figure 8 and 9 show the statement and proof in Mathlib4 and miniF2F respectively. It can be easily seen that both the statement and proof rely on pre-defined objects. Unlike miniF2F statements, the example in Figure 8 can not even pass the lean compilation, given that pre-defined objects are missing.
relatively small set of elementary facts about
theorem ndrec_eq_ndrect :
@Acc.ndrecC := by funext a r motive intro rw nAcec, rec_eq_recC, Acc.ndrecC]
Figure 8: A Mathlib4 example which relies on pre-defined objects nAcc.ndrec and @Acc.ndrecC.
D.2 ProofNet and miniF2F
The problems in ProofNet are primarily drawn from undergraduate pure mathematics textbooks, covering topics such as real and complex analysis, linear algebra, abstract alge- bra, and topology. These topics largely rely on the abstract and general formulations of mathematical definitions in Mathlib4 (mathlib4, 2023). We show two examples Table 13 to illustrate the style difference between ProofNet and miniF2F.
18

---

Published as a conference paper at COLM 2025
Jor (f $lo -i osdbic aibide 196, then find tates, show thas st 16 odh.nt thezran wrthd.atestra..00 250 La R) (he a a (hu + -
(hh b a te
equatiore:
anibulations and Unear
sotan
uxing equetiors.
will ose torse algenra teclnigass selae these exsetione.
seer by
eds
io sill use ridnarith to ssive the systen of Linsar aeuariorn derived from the given conditians. ci,
-Line-tth tnalaas)laumm Wol_seef.nseer bi.
selt manneg
Firelly cerclude
axt
Figure 9: A miniF2F example which does not rely on pre-defined objects
Example from ProofNet
Example from miniF2F
Informal Statement
Prove that no order can be de- fined in the complex field that turns it into an ordered field.
Show that for any natural num- ber n, does not divide 2" +
theorem exercise_1_8
(T C + [ Prop),
theorem 1mo_1964_p1_2 (n := by sorty
Tsl ielirnerrreer r := by sorry
-7
Formal State- ment Comments
This problem involves the no- tion of order, which is un- dergraduate level. Its formal statement uses the definition IsLinearOrder in Mathlib4.
This problem comes from IMO
but only involves division.
Table 13: Comparison of Examples from ProofNet and miniF2F. ProofNet largely relies on the abstract and general formulations of mathematical results Mathlib4. In contrast, miniF2F largely consists of high-school competition and Olympic style problems, which require complex reasoning.
Alternative approach for synthesizing data
We also considered other pipeline beyond autoformalizing statement and expert iteration for collecting proof data. Inspired by Jiang et al. (2022), implemented the following pipeline:
Step 1. We prompt OpenAl's ol prevveww model to generate proof for formal statement. We ask the model to generate the proof step-by-step, use "have" tactic to structure the proof. For each proof step, the subgoal of this step is indicated by "have", following by proofs for this subgoal.
Step 2. We remove the proofs for the subgoal provided by ol-preview in each "have" block (these proofs often involves detailed lean syntax, and is usually incorrect). That is, we only keep the "sketch" of the proof. We then put this proof sketch into Lean com- piler, to automatically extract each subgoal and corresponding conditions, form several subproblems.
Step 3. We apply ReepSeek-Prover-V1.555 to try to proof the subproblems. We try each subproblem for 32 times. If all subproblems are successfully proved, assembling these subproofs into the sketch gives valid proof for the original problem.
19

---

Published as a conference paper at COLM 2025
Figure 10 shows the only problem solved by this pipeline that PrepSeek-Prover-VLie does not solve, which is non trivial problem that requires relatively complex reasoning. Though this pipeline has shown potential, the efficiency is quite low. Only one additional problem is proved using this pipeline, among 244 problems in miniF2F validation set. This might due to the fact that this pipeline is overly complicated, since failure of each subproblem might lead to the failure for the entire problem.
thooron 31 (X The 2 x 5253 (Th Vini 3.
2 1.1. 1113 (hh x. 2 375) (h. X 429) (n 2) (n 5)
530 a 263 375 553 1- by
Porse, compute be voing the recurrance relation
have ha 3.0 257 to
here by
(by norm.mma))
Next,
every
will have perdon_20
(n
by
intro tn
Inducttonn in with
zero es
simp_all
succ
will (Met. suse.uce.uue one)
Linamith
Winritth), linarssh), 12 (by (inomith), 53 Linarith), Lirarstn),
(by linerath), linwrath), Linarichi, (by Linerkth)]
Compute
have x831.aq : 331
sirpa (hay hts hay hay has personsio) usong (shov 631 3 10 1. by note_nus)
Compute xoex
have 2753.09 : 755 a to
TW [show 753 10 a 75 a nemarrun)
ximp [per in,..nn, has has hs. hx] Compute
975
[pented_10, 4531, v7)
volues
have sunuez 2 551 + 793
noreunue (Ta, hoy Ita, hi, ha, 1551..o, x753L00, a595_00)
using the periosicityy conditton, ve simslify the sum to 2.2 X.5
Linorith [hi, he, na]
Figure 10: A non trivial problem solved by the divide-and-conquer pipeline
RL training details
E1
DPO training
For DPO training, we construct pairwise data on problems with pass ratio in (0,1/4) (from previous training dataset). To be specific, for each problem, we do Pass@16, and the pass ratio (0, 1/4] means we select samples where Goedel-Prover-SFT generates 1-4 correct proofs within 16 trails. We construct DPO pairs by randomly select a correct proof and wrong proof from the 16 trials. We sample 508K proved problems from the original dataset, and among which 30K problems with the aforementioned pass ratio is selected. We use a learning rate 5 x 10-6 and train for two epoches.
Our experiments reveal that through DPO training, the model is easy learn "shortcuts". Figure 11 shows one typical output of the DPO model. It repeatedly use tactics all goals and try, which might be shortcuts learned in DPO training. To mitigate the model's tendency to produce verbose, lengthy proofs by repeatedly utilizing these shortcuts, we implement length regularization in our DPO framework. Specifically, when multiple correct answers are available for given statement, select the one with the shortest length. All other settings remain unchanged from the original DPO implementation.
E2
GRPO training
We collect 80K problem statements whose pass ratio is within (0,1/2). We will also explore different design choices for the included problems in the subsequent discussion. Using these problem statements, we employed the Goedel-Prover-SFF as our base model and conducted reinforcement learning (RL) training within the OpenRLHF framework, utilizing the GRPO algorithm. During the RL training, we generated 16 proofs for each problem and verified their correctness through compilation. Correct proofs received reward of +8, while
20

---

Published as a conference paper at COLM 2025
theoren
(n. A M) the nin 3 + 10) (h: 1
(h2 : [A, B, Pa.iiiie (+ +)] (hr [A, B, [3 Finset. 9) (he : Odd Odd c)
-3 (.B) (hx : Nat.digits
C, A, Al)
100 A -10 C 129
digits_of_nunber n [8, A, R, C, G, A, G, B, A] in by
simpa [het.ddgitt..egnn3....... using he
simp
have := ha
simp-all [fat.digitt..f..4]]
all.-goals
try normunum
try decide
a.l.gools
try reases this with (h, ht)
try contradiction
a.l_goaas
try Linarith
atl.goals
try ying-nf
all..goas
try ring.nf at
atl.gools
try
al L.gals
try
s.l-goals
try normunum
Figure 11: Example of output of DPO model. The model is repeatedly using all goals and try.
incorrect proofs received a penalty of -8. We search for the learning rate among x 10 5 x 10-6, 2 10-6, and 1 x 10-6 and choose the learning rate 5 x 10-6, We explored initial KL penalty values of 0.03, 0.003, 0.00003, and O. Our findings indicate that the KL penalty does not significantly impact training. Consequently, we selected 0.003 as the penalty weight. used batch size of 256 and also tested a batch size of 128, which achieved very similar performance. After training the RL model for one epoch, we found that increasing the number of epochs does not enhance the final testing accuracy.
Mismatch between reinforcement learning (RL) reward and test accuracy. Figure 12 plots the average training reward and Pass@16 accuracy across training batches. Notably, we observe a mismatch between the reward and accuracy trends: while the average reward continues to increase throughout training, the Pass@16 accuracy plateaus after approxi- mately 20 training steps. This discrepancy may stem from the misalignment between the optimization objective and the evaluation metric. GRPO encourages generating successful proofs more frequently, rewarding higher success rates across samples. In contrast, the Pass@N metric only considers whether a problem solved least once, irrespective of how many successful attempts occur. As a result, improvements in reward do not necessarily translate into better Pass@N performance.
Exploration of included prompts for training RL. We previously mentioned that we use statements with a pass ratio within (0, 122 for training the RI. model. This selection is based on the fact that these samples are challenging yet manageable for the current checkpoint. We also conducted experiments with pass ratios of (0,1 (0,3/4) /4, and (0, 1]. Our findings indicate that balancing the difficulty of the chosen prompts crucial, and we compared their performance in terms of final testing results in Table 14.
Exploration on the reward design for timeout samples. Typically, when using the Lean compiler to verify Lean proof, we encounter three possible outcomes: successful com- pilation, failure with returned errors, or timeout within the predefined time limit. We experiment with various rewards for the timeout samples, while maintaining a fixed reward of +8 for correct proofs that compile successfully and -8 for incorrect proofs that fail to compile. The results in Table 15 demonstrates that setting the reward for timeouts to be the same as that for failures results in improved performance across these experiments.
21

---

Published as a conference paper at COLM 2025
GRPO Training Reward/Accuracy Curves
2-
0.900
0.875
Reward
0-
0.825
-1-
Revard Raw
-0,000
Rewerd Smoothedd
Accuraty - Raw
0.775
-3-
Accuraty Smoothed
0.750
50
100
300
350
Training Steps
Figure 12: This figure illustrates the average reward/ accuracy of each batch during GRPO training. A correct proof corresponds to reward +8, while failed one has reward -8.
Prompt Pass Ratio
Prompt Number
mini-F2F Accuracy(%)
(0, 1/4]
30K
58.2
(0, 1/2]
62K
60.4
(0, 3/4]
115K
59.8
(0,
(sub-sample) 200K
59.2
Table 14: Results of included different prompts for training RL.
G
Discussion
We delve into the characteristics of proofs generated by Goedel-Prover-SFT and discuss potential directions for improvement, particularly regarding the proof style adopted by the model, the role of search as well as online interaction in proof generation, and the integration of external symbolic computation tools such SymPy.
The Proof Style. We observe that the proofs provided by Goedel-Prover-SFT often rely on high-level tactics such as nlinarith and simp all among others. These high-level tactics handle multiple reasoning steps internally, delegating the resolution of intermediate steps to their built-in automation. For example, the nlinaritt tactic can automatically solve certain linear and non-linear equalities and inequalities. Figure 13 shows typical proof generated by our prover. The first several steps involve only trivial transformations of the original problem, whereas the final line uses nlinaritt th to immediately achieve the goal. Whether this style of proof sufficient for complex reasoning remains an important area for exploration.
Search and online interaction. Currently, Goedel-Prover-SFT generates the entire proof for the problem at once, without receiving further feedback. While our current approach is appealing in terms of computation, incorporating search and interaction in future work could enhance performance. For example, once tactic is generated by our prover, can interact with the Lean compiler to receive feedback how the goal changes after the tactic is applied. This information can then be utilized in generating the next tactic, potentially improving the overall proof strategy (Wu et al., 2024).
Timeout Reward
Testing Timeout Ratio
Testing Accuracy
4.5%
58.7%
-8
1.7%
60.2%
-16
0.8%
59.2%
Table 15: Investigation on the reward for timeout samples
22

---

Published as a conference paper at COLM 2025
Theorer lean.norkbeok.130 y
8) (hz 2
/ (x x +
y y- +
Establish that the deroninaters positive. have hi have h2
x
nliinrith
1. by nlinarith
have h3 0 2
by nlinarith
Clear the denonirators by miltiplying through by the product of the denominators, field.simp [hi, 12, h3]
Rewrite the inequality in forn suitable for Linesr arithretic.
rw [le.di__iff (by positivity)]
Linear arithnetic to
inequality.
nlinarith [sq_nerneg (x z), squnorne (x y), sq_nomeg (y c), sq.nonneg (2
x)]
Figure 13: Example of proof style, where intermediate steps are absorbed in high-level tactics
SymPy. Future work may aim to leverage other software packages to enhance Lean's capabilities. For instance, Lean's ring tactic can handle algebraic simplifications by applying axioms such as distributivity, associativity, and commutativity. However, a combination of tactics is required for non-algebraic transformations of transcendental functions, such as log- arithmic and trigonometric functions, and other advanced simplifications beyond commuta- tive rings. We explored using Python-basee computer algebra system, SymPy (Meurer et al., 2017), to simplify complex expressions in theorem statements and feed the simplified form into the prover: Specifically, we parse equations of the form
within the goals
of Lean theorem statements, construct the SymP' expression A B, and then apply the simplify method Lean. This procedure directly solves 9.4% of miniF22 by simplifying the statements to 0 = 0. In addition, it solves 0.8% of the problems in miniF2F that were unsolved by Goedel-Prover-S55 Pass@3200. Thus, Symly simplification is not part of any of our reported results. However, we think such procedures need further exploration.
with Pass@32, but did not improve Goedel-Prover-SFF with
23


Reviews:
[{"review_id": "5Uz4AwhEIr", "reviewer": "Reviewer_Zigm", "summary": "This paper describes a methodology for iteratively augmenting a corpus of informal (= natural language) mathematical proofs, using a formalizer (trained on informal/formal proof pairs), a prover, and a verifier together. This augmentation process allows their prover to achieve new state of the art results on several mathematical reasoning benchmarks.", "questions": "", "limitations": "", "rating": 8, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "This is an impressive engineering effort that leads to impressive results.", "reasons_to_reject": "I don't have major concerns (this is outside my area of expertise).", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "NCHDFq2cnM", "reviewer": "Reviewer_r5wC", "summary": "The paper tackles the problem of automated theorem proving by introducing a dataset of formal statements and proofs built by iteratively training a series of models. The authors introduce a model trained on this dataset, a finetuned version of deepseek-prover-1.5-base. The authors compare this model to RL-tuned and SFT versions of the base model.", "questions": "", "limitations": "", "rating": 7, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "- The paper is clearly written and well motivated\n- The list of benchmarks tested is pretty comprehensive\n- Across different benchmarks, the Goedel prover outperforms other models\n- The experiments with the training recipe were particularly good:\n    \n    1) I liked the analysis on scaling the size of the statement set.\n    \n    2) correlation between the datasets was also pretty insightful.\n    \n    3) The analysis RL training (GRPO, DPO) and alternate proof generation strategies do a good job of making the paper more complete.", "reasons_to_reject": "- A huge part of the synthetic data generation pipeline relies on closed models.\n- Only one base model is used for most experiments in the paper.\n- Rater reliability for the FC test is missing. It would be good to see how much Qwen and humans agree.\n- I know that the space is a little limited, but it would be useful to move the discussion into the main section of the paper.\n\n**Minor:**\n\n- Missing citations for expert iteration:\n    - STaR Bootstrapping reasoning with reasoning\n    - Reinforced Self-Training (ReST) for Language Modeling\n    - Training Chain-of-Thought via Latent-Variable Inference", "questions_to_authors": "- What happens when you switch the Formalizer B model for an open source model instead of claude?\n- Can you benchmark training with a different base model?\n- Can you also compare size of the models or flops in table 2?", "extra_scores": {}}, {"review_id": "SHv7JTEGnK", "reviewer": "Reviewer_e6im", "summary": "The paper presents Goedel-Prover, a language model for formal theorem proving in Lean 4. To address the scarcity of formal data, the authors autoformalize 1.64 million informal math problems—primarily from the Numina dataset—using two distinct formalizers, and verify their alignment with a separate LLM. The resulting dataset is used to iteratively fine-tune a base prover model (DeepSeek-Prover-V1.5-Base) through expert iteration. The paper reports consistent performance improvements across iterations, with strong results on benchmarks such as miniF2F, PutnamBench, and the Lean Workbook, particularly in whole-proof generation settings.", "questions": "", "limitations": "", "rating": 6, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "- The results look quite strong, on miniF2F the model gets 57.6% Pass@32 which is ~7% better than DeepSeek-Prover-v1.5-RL, and also performs best on PutnamBench (at the time of submission, now the record is much higher).\n- I liked the way they constructed the dataset — using two different formalizers and also verifying the alignment using another LLM is a solid idea, and probably helps robustness. The scale (1.6M formalized statements) is impressive too.\n- The training pipeline is pretty clean. It’s all supervised fine-tuning via expert iteration, no complex RL tricks in the main model. The description is clear and makes sense overall.\n- They did some good ablations — like showing the benefit of using diverse formalizations and of scaling the dataset. There’s also some thoughtful analysis on RL overfitting, reward hacking, etc which I appreciated.\n- One interesting observation was that applying RL like DPO or GRPO made the model write longer and sometimes repetitive proofs by overusing tactics like try. It’s useful that they highlight these drawbacks instead of just showing the gains — adds some nuance to the field.", "reasons_to_reject": "- The paper lacks significant novelty. The idea that expert iteration improves performance was already shown in Polu et al. (2022) [arXiv:2202.01344], and it’s well known in general that scaling data helps. This work mainly extends those ideas at scale rather than introducing new techniques or architectural improvements.\n- The open-source claim is unverifiable at review time. There is no anonymous link, supplementary code, or dataset. It's unclear whether the entire expert iteration pipeline will actually be released. Prior work often only releases models or inference scripts; without clarity on whether the full training and data generation setup will be included, it's hard to assess how open this effort really is.\n- The autoformalization quality checking just uses an LLM to assess alignment. Unlike Jiang et al. (2023) [arXiv:2311.03755], which included human evaluation of a subset of outputs, this work does not conduct any manual or crowd-sourced study. This weakens confidence in the quality of the 1.6M formalized statements.\n- The paper does not analyze the quality of the proofs themselves. How many rely on high-level automated tactics like linarith, simp, or ring? How long are the average proofs? Are they interpretable or just exploiting Lean’s built-in automation? These questions are especially relevant given that such tactics can solve many miniF2F problems in one line.\n- miniF2F itself is becoming a dated benchmark. Many of the problems can be solved with simple tactics and don't reflect deeper or multi-step mathematical reasoning. It's not clear whether Goedel-Prover performs well because of actual improvements in reasoning or just better exploiting Lean 4’s automation.\n- There’s no detailed discussion of potential data leakage. How distinct are the problems in the training dataset from the ones in miniF2F or other benchmarks? Given the overlap with Lean Workbook and other sources, the generalization claims are hard to judge.\n- The performance on PutnamBench is only marginally better than prior work (e.g., it solves the same number of problems as ABEL, just with fewer samples), so the improvement is not very substantial outside miniF2F.\n- While the observation that RL techniques like DPO and GRPO can lead to longer or degenerate proofs is interesting, it’s more of a side note and not enough to carry the contribution on its own.", "questions_to_authors": "Most of my questions are covered in the \"Reasons to Reject\" section. I would be willing to increase my score if the authors can address some of the concerns I have raised.", "extra_scores": {}}, {"review_id": "C9t7sIDduy", "reviewer": "Reviewer_Jesv", "summary": "The paper describes Goedel-Prover, a state-of-the-art large language model that can generate a proof for a given Lean 4 theorem. The contribution is two-fold: (1) the pipeline for creating formalization (translating natural language theorems to Lean4) datasets and training the Goedel-Prover model by expert iteration (~rejection sampling), and (2) valuable resources for the field, namely the Goedel-Prover model, a large auto-formalization training data (1.73M), and ~30k proofs for the Lean Workbook theorems (for context, the original Lean Workbook only contains theorems without corresponding proofs).", "questions": "", "limitations": "", "rating": 7, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "1. **Empirical performance.** The performance of Goedel Prover is impressive, with an unprecedented success rate in common benchmarks like MiniF2F and Lean Workbook. The authors have effectively shown that simple strategies like rejection sampling can dramatically boost the performance.\n2. **Significant model/data contribution.** Goedel-prover model, ~1.8M proposed formalization data, and ~15k new Lean Workbook proofs will be a fundamental resource for future research in LLM-for-formal-proofs. I personally find Lean Workbook data a significant contribution to the community, since it is currently the largest dataset where one can find natural language questions mapped to their formal proofs.", "reasons_to_reject": "1. **Technical novelty**. The Goedel-Prover's key methods are (1) translating Numina's abundant NL problems to Lean 4, and (2) applying multiple rounds of rejection sampling to improve the performance. I see the development of Goedel-Prover as a scaled-up version of DeepSeek-Prover v1 (Xin, 2024) with minimal technical innovation. The only novelty of this work I can find is that it uses two formalizer models (Section 3.1) that increase the performance by adding diversity to the input format (Table 3), which is an interesting analysis but significantly underexplored to be a strong contribution. This is the critical reason why I did not give a higher score.\n\n2. **Cannot solve general math problems. (nice-to-have)** Current form of Goedel-Prover takes *formalized theorems* as input, which introduces two limitations.\n\n- (1) It needs autoformalization to prove a theorem given in natural language. Therefore, if the theorem description is given in natural language, the autoformalizer's error can propagate, further reducing the success rate.\n- (2) It cannot solve math problems where the answer is not yet known (e.g., *What is the answer?* or *Is this conjecture true or false?*). To solve these problems, the autoformalizer should first find the answer candidate (*The answer is likely 5.*) and prove if that answer is correct (*What is the answer? Prove that it is 5.*).\n\nWhile these criticisms generally apply to all previous Lean 4 proof generators, it would be nice to explore these new directions with NL-only theorems or open-ended questions. Note: This did not affect the rating a lot.", "questions_to_authors": "1. **Regarding `try` tactic in RL-trained models** It is quite interesting that models trained with RL use `try` more frequently. Can you observe a similar trial-and-error behavior in the *CoT comments*, e.g., using words like 'wait' or 'alternatively' more often [1]?\n\n2. **Effects of RL in low inference budget.** RL is known to boost performance when sample size (Pass@K) is small, but the gain converges when K gets larger [2]. Indeed, Table 5 shows that the gain by RL is larger in Pass@32 than Pass@3200. How do default and RL-trained models perform in a highly constrained setting, e.g., Pass@1 or Pass@4?\n\n3. **Human eval on Faithfulness & Completeness** I intuitively understand that Claude or other LLMs will do a good job for F&C eval, based on my personal experience. However, I wonder if there is a human evaluation result on a small test set.\n\n[1] Yeo, E., Tong, Y., Niu, M., Neubig, G., & Yue, X. (2025). Demystifying Long Chain-of-Thought Reasoning in LLMs. arXiv preprint arXiv:2502.03373.\n\n[2] Shao, Z., Wang, P., Zhu, Q., Xu, R., Song, J., Bi, X., ... & Guo, D. (2024). Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300.", "extra_scores": {}}]

Author rebuttal:

Meta-review: Thanks to the authors/reviewers for their engagement during the discussion period!

_Quality_: The approach proposed in the work yields solid empricial results (all reviewers), is comprehensively evaluated across a range of benchmarks (Reviewer r5wC), and is accompanied with interesting analyses and ablations (Reviewers r5wC and e6im). Reviewers r5wC, e6im, and Jesv pointed out the need for (small-scale) human evaluation, which the authors provided during the discussion. The amount of datapoints analyzed was small, which is understandable given the time constraints, but I agree with Reviewer e6im that this eventually needs to be scaled up at least slightly beyond n=28. The authors have also followed up with several additional analyses following reviewer requests, and these will be nice additions to include in the subsequent revision.

_Clarity_: No major clarity issues were raised and several reviewer questions were address adequately during the discussion period. Further clarity on which parts of the pipeline relies on closed source models and how the proposed approach relates to prior work would be helpful to have in the subsequent draft (most of this has already been discussed here). 

_Originality_: While a few reviewers questioned the methodological originality of the work, I agree with the authors that an open source release of the training/data recipe and the dataset itself, combined with strong empirical results (as acknowledged by all reviewers), is a valuable original contribution.

_Overall significance_: Solid paper with on a topic of interest to the COLM audience with useful open source contributions.

[Automatically added comment] At least one review was discounted during the decision process due to quality]
Decision: Accept