ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
Authors: Alex Gu
Bartosz Piotrowski
Fabian Gloeckle
Kaiyu Yang
Aram H. Markosyan
Venue: ICLR 2026 Poster (2026)
Keywords: ai for math
proof simplification
Primary area: foundation or frontier models, including LLMs
TL;DR: we train a model to simplify AI-generated Lean proofs

Abstract: Neural theorem proving has advanced rapidly in the past year, reaching IMO gold-medalist capabilities and producing formal proofs that span thousands of lines. Although such proofs are mechanically verified by formal systems like Lean, their excessive length renders them difficult for humans to comprehend and limits their usefulness for mathematical insight. Proof simplification is therefore a critical bottleneck. Yet, training data for this task is scarce, and existing methods—mainly agentic scaffolding with off-the-shelf LLMs—struggle with the extremely long proofs generated by RL-trained provers. We introduce ProofOptimizer, the first language model trained to simplify Lean proofs without requiring additional human supervision. ProofOptimizer is trained via expert iteration and reinforcement learning, using Lean to verify simplifications and provide training signal. At inference time, it operates within an iterative proof-shortening workflow, progressively reducing proof length. Experiments show that ProofOptimizer substantially compresses proofs generated by state-of-the-art RL-trained provers on standard benchmarks, reducing proof length by 87% on miniF2F, 57% on PutnamBench, and 50% on Seed-Prover's IMO 2025 proofs. Beyond conciseness, the simplified proofs check faster in Lean and further improve downstream prover performance when reused as training data for supervised finetuning.

Published as a conference paper at ICLR 2026
PROOFOPTIMIZER: TRAINING LANGUAGE MODELS TO SIMPLIFY PROOFS WITHOUT HUMAN DEMONSTRA- TIONS
Alex Gu MIT CSAIL gua@mit edu
Bartosz Piotrowski Axiom Math
Fabian Gloeckle
Meta FAIR & Ecole des Ponts Paris fgloeckle saalocckeeemea...... com.
baxtosspp..troosskeppot.. pl
Kaiyu Yang'
Aram H. Markosyan
ka kaiyuy@aluma www.iirrinnntooo. edu
Axiom Math am& axi ommat ai
ABSTRACT
Neural theorem proving has advanced rapidly in the past year, reaching IMO gold- medalist capabilities and producing formal proofs that span thousands of lines. Although such proofs mechanically verified by formal systems like Lean, their excessive length renders them difficult for humans to comprehend and limits their usefulness for mathematical insight. Proof simplification is therefore a critical bottleneck. Yet, training data for this task is scarce, and existing -manlyy agentic scaffolding with off-the-shelf L.MMs struggle with the extremely long proof's generated by RL-trained provers. We introduce ProefOptimizer, the first language model trained to simplify Lean proofs without requiring additional human supervision. ProofOptimizer is trained via expert iteration and reinforcement learn- ing, using Lean to verify simplifications and provide training signal. At inference time, it operates within an iterative proof-shortening workflow, progressively reduc- ing proof length. Experiments show that ProofOptimizer substantially compresses proofs generated by state-of-the-art RI RI-trieeed provers standard benchmarks, reducing proof length by 87% on miniF2F, 57% on PutnamBench, and 50% on Seed-Prover's IMO 2025 proofs. Beyond conciseness, the simplified proofs check faster in Lean and further improve downstream prover performance when reused as training data for supervised finetuning. We release our evaluation dataset and proofs generated by our model here.
INTRODUCTION
Theorem proving formal environments such as Lean (de Moura al., 2015) provides an excellent testbed for training large language models (LLMs) in mathematical reasoning via reinforcement learning (RL). Since Lean can mechanically verify proofs, filters hallucinations and provides reliable reward signals, and enables enables unlimited high-quality synthetic reasoning data. Leveraging these benefits, LLMs finetuned with RL have achieved near gold-medal performance on the International Mathematical Olympiad (IMO) (Chen et al., 2025) and shown strong results on difficult college-level benchmarks like TutnamBench (Lin et al., 2025b).
However, RL-trained provers often generate proofs that are correct but excessively long and in- scrutable. Since their only reward signal is the correctness of generated proofs, the resulting models produce proofs that correct yet suboptimal: convoluted, bloated with redundant steps, reliant unnecessarily strong automation where simple step would suffice. For example, Seed- Seed-Prover (Chen al., 2025)'s Lean proof of IMO 2025 Pl consists of 4,357 lines of code, 16x longer (by character count) than its informal counterpart. Such proofs pose several practical drawbacks: they are (1) difficult for humans to comprehend, limiting their value as a source of mathematical insight: (2) less
Work done Meta Superintelligence Labs (FAIR).

---

Published as a conference paper at ICLR 2026
suitable synthetic training data, since models may struggle to learn from convoluted proofs; and (3) computationally inefficient to compile in Lean, which is especially problematic when integrated into existing formal libraries like mathlib (mathlib Community, 2019).
These challenges highlight the need for proof simplification: transforming existing formal proofs into simpler forms while preserving correctness. In this work, we adopt natural notion of simplicity: proof length, measured by the number of Lean tokens. However, our approach is agnostic to the choice of simplicity metric: it is not restricted to proof length, but applies any automatically computable measure (Kinyon, 2018).
Prior work on proof simplification (Ahuja et al., 2024) focuses agentic scaffolding around API- only LLMs such as GPT-4o. While these methods can shorten human- Lean proofs, they are ineffective at simplifying the long proofs generated by SoTA RL-trained LLM provers such as Seed-Prover and Goedel-Prover V2 (Lin et al., 2025b), precisely the setting where simplification is most valuable. A natural alternative is to finetune LLMs directly for proof simplification, but progress in this direction is limited by the lack of suitable training data, namely aligned pairs of proofs before and after simplification.
We introduce ProofOptimizer, an LLM-based system for simplifying long and convoluted proofs in Lean. ProofOptimizer integrates three components: (i) a symbolic Lean linter that identifies and removes redundant steps. (ii) 7B parameter language model finctuned specifically for proof simplification. and (iii an iterative inference- time algorithm for progressively shortening proofs. Given input proof, the Lean linter first eliminates the most obvious redundancies. The language model then generates multiple candidate simplifications, and the iterative algorithm repeatedly applies the model to the currently shortest proof, further reducing its length. Training follows two paradigms. In expert iteration, the model proposes simplifications that are verified by Lean and incorporated into the training data for supervised finetuning. In reinforcement learning, proof length and correctness serve as the reward signal. Both approaches enable continual improvement without requiring any human-annotatee annotated simplification data.
First, we evaluate ProofOptimizer on long proof' generated by state-of-the-ar neural theorem provers. Specifically, we consider proofs produced by Goedel-Prover- V2 on two standard benchmarks- MiniF2F (Zheng et al., 2021) and PutnamBench as well as four proofs released by Seed-Prover for IMO 2025. Our final models achieve significant results (Fig. 1), shortening MiniF2F proofs by an average of 63% in a single shot and PutnamBench proof' by 26% with 32 attempts, substantially outperforming Semmini-255-Pra (Sec. 4.1). At inference time, test-time RL improves single-shot miniF2F performance to 72%. With with iterative shortening, achieve further per- per-proof average reductions of 87% (MiniF2F) and 57% (PutnamBench) and reduce the length of three out of four Seed-Prover IMO 2025 proofs by more than half.
Second, we conduct ablation studies to evaluate the effect of key design choices. During training, RL achieves the best single-same sample performance but reduces sample diversity. At inference time, using the same RL recipe further improves single-shot performance (Sec. 4. Repairing incorrect simplifications from execution feedback with EGoddel-Prover effectively corrects errors, but leads to repaired proofs even longer than the originals (Sec. 4.2). Overall, iterative proof shortening offers the best balance between performance and diversity, achieving the strongest results (Sec. 4.3).
Third, we conduct preliminary experiments suggesting two downstream benefits of proof shortening. Training our base model on shortened proofs leads 2% better performance on miniF2F relative to training on unshortened proofs (Sec. 5.1). Also, shortening proofs often decreases their execution time, with 28% of proofs showing at least a 1.5x speedup after shortening (Sec. 5.2).
2

---

Published as a conference paper at ICLR 2026
Before ProofOptimizer
After ProofOptimizer
theores putnoee 1968
22/7 pi in (9)..1, xM4
(1
Jahoe
(x
223 by
metuce
Meldd.sopp
intro
ring]
ring.nf
nora,
pl.poo)
Figure I: ProofOptimizer reduces the shortest generated proof of Putnam problem from 1097 to 76 tokens.
2 PROOF SIMPLIFICATION: TASK AND METRICS
Task Definition We formalize the proof simplification task as minimizing the complexity of a given proof. Specifically, for valid formal statement with proof p, the goal produce alternative proof pa of that minimizes complexity measure L: arg mill (xx)
proves
Our method is agnostic to the choice of complexity measure L, provided that is deterministic and be automatically computed from the proof. This flexibility encompasses the metrics used in prior work (Ahuja et al., 2024). In the rest of this paper, we adopt proof length as the measure of complexity, defined the number of tokens produced by Lean-specific tokenizer. Our proof length measure correlates with character count but does not penalize long identifier names, and it ignores comments and line breaks. We denote the length of a proof x by | i.., [(x) |z].
Evaluation Metrics Given an original proof and & candidate simplifications generated by the model, P1 Pi.P2..... P/.. we define 4 min(1p], (p()) if pl valid proof and |pl otherwise. (Intuitively, an invalid attempt reverts to the original proof length). We evaluate proof simplification using two metrics:
min @k A min; (4) denotes the minimum shortened proof length (lower is better).
@ed@k & max; { [p--4
lpl = 1 min@kk denotes the maximum relative proof length reduction Ip]
from the original proof (higher is better).
Note that these metrics may not always be correlated: method that only excels at shortening long proofs has lower min @k k and red@k k than one that only excels at shortening short proofs. As with the @ass@k metric (Chen et al., 2021), we report our metrics via an unbiased estimator using n > samples (see Appendix J). We average min @k and red @k across samples in dataset to get overall length and reduction metrics.
PROOFOPTIMIZER: LLMS FOR PROOF SIMPLIHICATION
3.1
TRAINING
Lean Base Model First, we train a general-purpose Lean model by fine-tuning Owen-2.5- 5-BB- Instruct on combination of five tasks: natural language problem solving, Lean 4 code completion, auto-formalization (problems and solutions), formal theorem proving, and tactic/proof state prediction.
Dataset for Proof Simplification We employ a four-stage pipeline to generate high-quality proof simplification training data.
1. Problem Collection: We first compile dataset of theorem proving problems from Goedel-Pset. filtering out simple computational problems. Each problem consists of
natural language problem, solution, and Lean problem statement.
2. Proof Sketching: We train model that formalizes problem's natural language solution into Lean proof sketch consisting of a few high-level proof steps (usually 2-10) with lower level details omitted and filled in with Lean's sorry tactic.
3

---

Published as a conference paper at ICLR 2026
3. Theorem Extraction and Filtering: For each proof sketch, extract each proof step into its own separate theorem. At the core, we are taking longer proofs and breaking them down into separate sub-theorems. We collect total of 518K theorems this way. As found some of these theorems to be trivial, we design an automation tactic to filter these out, leaving 307K theorems remaining.
4. Proof Generation: We use Goedel - Provvrr - -e-r---2--- V2-32B to generate proofs of these theorems. The model successfully produces Lean proofs of 145K theorems, which we use as our dataset for training.
For more details about our base model and dataset collection, see Appendix B. Next, we describe our two training recipes: expert iteration and online reinforcement learning.
3.1.1 PROOFOPTIMIZER ExxII: EXPERT ITERATION
We leverage STaR-like (Zelikman et al., 2022) iterative training algorithm to improve our model. At high level, we start with our base model To and the collection of 145K proofs Po. each iteration, we attempt to simplify each proof, train our model successful proof simplifications, and use the collection of simplified proofs as seed proofs for the next iteration. More precisely, at each iteration i, we do the following:
1. Sample: For each proof E P.. use m. sample simplifications Y, (1er Uzz Ve v2d (T).
2. Filter:
Use the Lean compiler find the shortest correct simplification y22 E {x} U yg Create training dataset of proof simplifications D; = {xx y2) len(ye) S 0.8 len(z), E P.). The length constraint designed to encourage the model learn more substantial simplifications rather than trivial ones. For iterations after the first, as may have been simplified from more complex proof x' Po. we also add (x', (z)) pairs to D,, which are valid and larger proof yz)
simplifications. Also, collect simplified proof's TT+1
{s x E P.) for the next iteration.
3. Train: Fine-tune Ty on D; to get T++1-
3.1.2 PROOFOPTIMIZER
ONLINE REINFORCEMENT LEARNING
In addition to expert iteration as described in the previous section, we train a proof optimizer model with online reinforcement learning. Using the same dataset as in expert iteration, the reinforcement learning task consists in producing a valid but shorter proof y for a statement given an initial proof
a. The reward is defined as the relative shortening R(x,y) = [ if is valid and |y/ S |ar|. and R(x, y) otherwise. We employ an asynchronous variant of the GRPO algorithm (Shao al., 2024) with advantage A; = R, Σj<r R, baselined with the average reward of k = 8 samples, no ad advantage normalization by standard deviation (Liu et al., 2025b), no KL regularization, and omitting sequences with zero advantage.
3.2 AFERENCE-TIME TECHNIQUES
First, implement symbolic linter that removes extraneous tactics via Lean's wwwter..nnneeeeeeeeeee wwwsedTacticc linter, which detects tactics that do not change the proof state and provides messages like norm-num' tactic does nothing. We then compare the following techniques on the linted proofs:
Test-Time RL:
We the setup described Section 3.1.2 and perform reinforcement learning our two evaluation sets (jointly). Our test-time RL keeps the input proof fixed, meaning improvements occur solely in the model's parameters.
Repair with Execution Feedback: In this scheme, if ProofOptimizer fails to simplify proof, we collect the execution feedback and ask Goedel Bondee-Prroeee -Prover-vev -32B to repair the proof with the error messages. Then, we apply the symbolic linter on the new proofs to further shorten successful repairs.
Iterative Proof Shortening: For given proof, sample & candidate shortenings and take the shortest correct one. Then, we sample shortenings of the new proof, take the shortest correct and on.
4

---

Published as a conference paper at ICLR 2026
4 EXPERIMENTS
For all evaluations, we use proofs generated by Goedel-Prover-Ve V2 (Lin et al., 2025a) on two popular datasets in formal math, miniF2F (Zheng et al., 2021) and PutnamBench (Tsoukalas al., 2024). For miniF2F, we use 194 proofs (average length 334), and for PutnamBench, we use = 75 proofs (average length 1468). More details and examples of proofs our evaluation set can be found in Appendix G.
4.1 EXPERT ITERATION VS. RL VS. TEST-TIME RI.
First, we compare our two training schemes: expert iteration and RL. Starting from our Lean base model, we train ProofOptimizer-EE Explt by performing three rounds of expert iteration (Sec. 3.1.1) and ProafOptimizer-Rl by performing online RL (Sec. 3.1.2) after two rounds of expert iteration. Table shows min @k and red@k scores with respect to linted proofs. We observe steady improvements during each round of expert iteration for both @ and @32 metries. Our final model outperforms Gemini-2.5-Pro, a strong reasoning model, even when given proof state annotations similar to Chain-of-Starn -f-ttess ImProver (Ahuja al., 2024).
Next, we see that ProofOptimizer-He RL significantly improves single sample (@ 1) metrics at the expense of diversity collapse, an issue commonly identified during RL training (Gehring et al., 2024; Walder & Karkhanis, 2025; Yuc et al., 2025). In Fig. (a, b). show the evolution of red during training, observing that miniF2F reduction steadily rises while PutnamBench reduction experiences oscillations. This tension is likely because the distribution of training data is more similar in length to miniF2F than PutnamBench, which has a mean proof length of 4x that of the training set.
Finally, we find that test-time RL leads expected, as the model is able to directly tune its weights to learn from successful simplifications test-time. However, like ProofOptimizer-RL.
further improvements on min @ and red@ This is
observe an smaller gap between @ I and @ 32 metrics. In Fig. 2 (c, d), we observe much more stable evaluation red curve because the distribution gap between the training and evaluation
eliminated.
Table 1: Min@k and Red@k throughout expert iteration and online RL. Our RL model has strong results, while our Explt model has strong @32 results. RL metries are Gaussian-smotthed.
Dataset
Category
Model
Min Min @32
Red@ 1
Red@32 f
Linted
302
0.0%
Gemini-2.5-Pro
280
207
24.3%
57.2%
Gemini-2.5-Pro + States
283
207
26.4%
58.7%
Base (7B)
283
202
17.6%
56.2%
miniF2F
Base It
266
178
33.4%
67.0%
Explt
Basc It
251
166
45.1%
70.6%
ProofOptimizer-Fiye
241
153
49.0%
72.3%
ProofOptimizer RI.
190
152
63.6%
70.9%
RL
It 2 Test-Time RI.
160
154
72.5%
73.4%
Linted
1359
0.0%
Gemini-2.5-Pr Gemini-2.5-Pro States
1348
1303
5.5%
18.0%
1371
1319
6.1 %
19.2%
Base (7B)
1341
1222
3.9%
20.5%
Putnam Bench
Base It
1341
1215
5.2%
22.5%
Expli
Base 2t
1335
1186
6.9%
24.7%
ProofOptimizer Exxpl
1328
1161
8.2%
26.3%
ProofOptimizer-Rl
1303
1258
14.9%
21.1%
RL
2 Test- Test-Time RL
1260
1255
23.8%
24.2%
5

---

Published as a conference paper at ICLR 2026
Table 2: Step-by-step success rates, revealing the main bottleneck of long repaired proofs.
Dataset
Simplitication
Repair
Shorter than best (before/after linter)
miniF2F
7852
(63.2%)
2840
(62.2%)
137
(2.7% + 4.8%)
12416
1561
2810
2840
PutnamBench
1288
(26.8%)
613
(17.4%
5
11
(0.8% - 1.8%)
613
Rebniive aorternng
12
130
50
102
190
Stop fJ)
Stop 02
Stop 0J)
Stop 03
miniF2F (train)
(b) Putnam (train)
(c) miniF2F (test-time)
(d) Putnam (test-time)
Figure 2: Evolution of proof reduction (red@) 1) during RL training (a, b) and test-time RL (c, d). We use Gaussian smoothing (o evaluation intervals for RL training and 3 for test-time
RL). See Fig. 9 for the corresponding red @ 32 metrics.
4.2 ANALYSIS OF REPAIR WITH EXECUTION FREDBACK
As described in Sec. 3.2, (1) sample 64 simplifications for each proof with ProofOptimizer-Exxy (2) repair incorrect proofs with Goedel-Prover- Proeeel-Pover- and (3) shorten successful repairs with our linter. Overall, find while repair with execution feedback leads to improvements, underperforms resampling because repaired proofs are often even longer than the original proofs. Fig. 3 (left) shows the average proof length and reduction % after sampling, repair, and linting. We our linter to be effective on repaired proofs, decreasing the average repaired proof length from 644 - 576 (miniF2F) and 877 788 (PutnamBench). In Fig. (right), we plot the proof length of the original proofs (before Step 1) against simplified proofs (Step 1) and repaired proofs (Step 2). majority of the repaired proofs (green dots) are above the y = x line, meaning they are longer than the original proof's let alone the simplified proof's (blue dots).
Simplffee (Wrong) Simpll wnd (Cameet) (Comect) y-x
ProerOpt
ProefDitt
Wonggeepaired Length (log scale)
Repair
10"
Repar Unter
Repair Unter
ProofOpt (0 128)
ProofOpt 1281
188442)
188442]
1100
1110
1120
10'
10"
Original Length scale)
Figure 3: Analysis execution-based repair with Goedel-Prover-VV V2 on PutnamBench.
In Table 2, we analyze the success rate of each step of our pipeline. However, the key issue remains be the high length of the repaired proofs. Even after linting, only 4.8% (miniF2F) 1.8% (Putnam) of post-linted proofs are shorter than the best proof found by ProofOptimizer during simplification. We refer the reader to Appendix for further analysis and examples.
4.3 ITERATIVE PROOF SHORTENINGG
In Fig. 4 (left), show the results of iterative proof shortening miniF2F and PutnamBench proofs using ProofOptimiiee-EEphhe First, we do 64 samples per iteration for iterations, observing steady improvement each iteration. To demonstrate the potential of further scaling, we do 1024 samples

---

Published as a conference paper at ICLR 2026
at iterations 7 and 8 and see significant improvement (see Appendix D.2 for analysis on sample size). Overall, ProofOptimizer combined with iterative proof shortening is very effective on miniF2F and PutnamBench, as average proof length is reduced from 334 + 75 and 1468 - 811, for average per-proof reduction of 87.9% 37.9%/57.22 55.2%. In Fig. 4 (right), we plot the overall shortening against the length of the original proof, observing that longer proofs remain challenging simplify.
Ming64 (minIF2F)
Ming64 (Putnam)
Reduction Proof Length
300
1350
Proof Length (4)
240
1.0
1050
80
902
% Reduction (1)
60
Dataset MiniF2F
Redg64 (miniF2F)
Redg64 (Putnam)
% Reduction (T)
80-
40
60-
60-
30
20
15
10
50
100
500 1000
5000
Ieration
Iteration
Original Proof Length (log scale)
Figure 4: Iterative Shortening:
per-iteration improvement (left) and effect of proof length (right)
Finally, Table 3, we demonstrate the effectiveness of ProofOptimizer on an out-of-distribution dataset,
four IMO 2025 proofs. With an order of magnitude higher sampling budget, we achieve a significant reduction in the proof length for all four problems, showcasing the potential of our model and technique. Details about our full setup are in Appendix D.3.
Table 3: Iterative shortening achieves significant reduction for Prover's IMO 2025 proofs.
P1
P3
P4
P5
Original Proof Length
36478
16377
29147
8658
Simplified Proof Length
20506
7907
14531
4002
Length Reduction
43.8%
51.7%
50.1%
53.8%
5 ADDITIONAL BENEFITS OF PROOF SIMPLIFICATION
5.1 TRAINING ON SIMPLIFIED PROOFS IMPROVES GENERATION
Next, we investigate whether fine-tuning on simplified proofs can be advantageous compared to fine-tuning on longer, raw proofs. To do so, we prepare two datasets of identical problems, the first containing set of proofs generated by Goedel-Prover--e proofs simplified by ProofOptimizer-Expe
and the second containing the same The average proof length of the original and simplified proofs is 147 and 85, respectively. We do continued supervised fine-tuning (SFT) starting from our base model (Sec. I) with a standard negative log-likelihood (NLL) loss.
In Fig. (left), we compare the training loss between the two datasets. As expected, the initial loss when using original proofs is higher, as models have not seen such long proofs during initial fine-tuning. However, the losses quickly converge. We observe that training on original proofs causes occasional loss spikes, which we suspect are due to several data batches that are hard to learn (e.g. extremely long proofs). Decreasing the learning rate mitigated these training loss spikes but did not improve validation accuracy. In Fig. 5 (right), during SFT, showing that training on simplified proofs results in slightly higher evaluation accuracy despite the two settings having identical training losses.
compare the miniF2F scores of the two models
7

---

Published as a conference paper at ICLR 2026
Training Loss
miniF2F Pass@32 (T=0.8)
0.15
Original Simplified
Original Simplified
63
61
60
59
400
800
1200
1600
2000
0
400
800
1200
1600
2000
Step
Step
Figure 5: Training loss (left) and m2niF2F score (right) after SFT on simplified vs. original proofs.
5.2 SIMPLIFIED PROOFS HAVE SHORTER EXECUTION TIME
We also observe that proofs simplified by ProolOptimizer often exhibit a faster execution time. We measure proof execution time with lake env lean --profill excluded library import time (imports are always the same but actual time may vary due to caching effects). We compare the execution times of each proof before and after iterative shortening Fig. (scatter). For both datasets, we visibly observe that majority of points lie below the y = x line, signifying speedup. Fig. 6 (histograms) also show the distribution of speedup ratios timeur
Of the 75 PutnamBench proofs, 50/75 have a speedup of over 10%, and 22/75 of those have speedup of over 50%. We also observe that proofs with a higher original execution time tend to show more speedup. The same trends hold for miniF2F, where 114/19h and 56/194 proofs have a speedup over 10% and 50%, respectively. Finally, we observe 25% and 81% speedups Seed-Prover's proof' for P3 and P4 of the IMO 2025 (Sec. D.3).
Upon qualitatively analyzing the proofs, we observe that the original proofs often have extraneous tactics that are eliminated by the simplified proofs. However, we also find several cases where the simplified proofs are much slower than the original proof. which usually occurs when a faster proof algorithm is replaced by a shorter but slower method (e.g. brute force with i interval 1 ca ses). We provide two examples of each in Appendix 1.2. Finally, we remark that all of our training and inference pipelines can also be applied to proof speedup as well by adjusting the reward function from proof length proof execution time.
Execution (Pumann
Speedup Dearibution (Putran)
Exccution (2in
Speeduu bution (min
35
Smmplted
0.5
3.5
10
25 Speedup Rano
155
Original Time
Speeous Radi
Original Time (4
Figure 6: Simplified proofs are frequently faster than original proof's on miniF2F and PutnamBench.
5.2.1 OPTIMIZING FOR HEARTBEATS INSTEAD OF PROOF LENGTH
As stated in Sec. 2, our complexity measure L generalizes beyond proof length. Next, we L to be the number of Lean heartbeats! a proxy of execution time that can run efficiently in parallel. With this metric, we run eight iterations of the same inference-time algorithm using ProofOptimizer-EExplt In Fig. 7 (a. b), we show analogous plots as earlier for miniF2F. Observe that this time, all the points are now on or below the y = x line, eliminating the short but slow proofs we saw in Fig. 6. Overall, we observe faster proofs, with 138/194 and 81/194 miniF2F proofs showing a speedup over 10% and 50%, respectively (compared to 114/194 and 56/194 before using the length metric). In Fig. 7 (c), we see that while the lengths of the proofs found with this metric are slightly longer than before, there still considerable shortening. Finally, Fig. (d) explains this by showing that proof length and number of heartbeats are generally correlated. In the future, optimizing for combination of proof
We use count heartbeats with set option Elab. Elabbasync false
8

---

Published as a conference paper at ICLR 2026
length and heartbeat count could lead to improvements in both readability and execution time. Full results can be found in Sec. I.1.
Times
Spsedap
Heartboebs vn, Proot
15
2250
Length Metre Meariscats Midr
80
Prout Leegghh 143
12200
8
16
3003
603
mi0 Putram
30 Or gin (5)e
05
23
255
30
101
13"
22'
Speedup Rarlo
Reration
To eene Jog sovie)
Figure 7: Using heartbeats instead of proof length complexity measure
6 RELATED WORKS
LLMs for Theorem Proving in Lean Formal theorem proving a rapidly growing frontier in AI for mathematics and software verification (Yang et al., 2024b; Li et al., 2024). Progress is typically measured with benchmarks of mathematical theorems Lean such as miniF2F (Zheng et al., 2021), 1), PutnamBench (Tsoukalas al., 2024), and ProofNet (Azerbayev et al., 2023). Recently, there have been many L.MS developed for Lean such as Seed-Prover (Chen et al., 2025), Goedel-Prover (Lin PaapSSeek-Proee (Ren al., 2025), and Kimina-Prover (Wang al., 2025). There
al., 2025a), have also been post-trad post-training techniques built on top of these models, such as with expert iteration (Lin et al., 2024), proof sketching (Cao al., 2025), tree search (Lample et al., 2022; Zimmer et al., 2025), self-play (Dong & Ma, 2025), proof repair (Ospanov et al., 2025), and RL (Gloeckle et al., 2024).
AI for Program Simplification A related line of work makes programs shorter or more efficient (Schkufza et al., 2013; Mankowitz et al., 2023; Shypula et al., 2023; Gautam al., 2024). In parallel, library learning aims to discover reusable abstractions, often eliminated repeated code and shortening programs (Ellis et al., 2023; Grand et al., 2023; Kaliszyk & Urban, 2015; Wang et al., 2023; Zhou et al., 2024; Berlot-Attwell et al., 2024). Finally, symbolic reasoning techniques like program slicing (Weiser, 2009), super-optimization (Sasnauskas et al., 2017), or partial evaluation (Jones, 1996) can also shorten and optimize low-level code.
Automated Proof Shortening Frieder et al. (2024) study factors that make Lean proofs casier to understand, motivating shorter proofs for maintainability. Classically, there have also been many symbolic methods targeting shortening proofs in SAT and first-order logic languages (Rahul & Necula, 2001; Vyskočil et al., 2010; Wernhard & Bibel, 2024; Gladshtein et al., 2024; Kinyon, 2018). On the neural side, GPT-f (Polu & Sutskever, 2020) generated 23 verified proofs shorter than those in the Metamath library. Most related to our work, ImProver (Ahuja et al., 2024), is an inference-tine method for proof shortening using GPT-4o with proof states and retrieval. In contrast, we use training-time approaches (expert iteration and RL), analyze complementary inference-time
techniques, and focus on shortening longer proofs generated by SoTA LLMs.
7 CONCLUSION
We present ProofOptimizer, the first language model trained to simplify Lean proofs. Unlike prior work that wraps existing LLMs around agentic scaffolding, we train a model using expert iteration and RI., coupled with symbolic linter and iterative proof shortening at inference time. Although simple, our approach already yields nontrivial results, reducing proof length by an average of 87% on MiniF2F, 57% on PutnamBench, and over 50% on Prover'sss''s ' IMO 2025 proofs. In addition, our methodology, framework, and insights generalize beyond Lean proof shortening and apply to other domains and metrics as well. As AI becomes more tightly integrated with mathematics, we envision future where Al- Al-generated proofs are not only correct but also concise and readable, with simplification serving as a critical bridge between rigorous formal proofs and human intuitive understanding.

---

Published as a conference paper at ICLR 2026
ACKNOWLEDGMENTS
We thank Heather Macheth for suggesting the experiments in Sec. 5.2.1 and writing the code count heartbeats, Albert Jiang and Melanie Matchett Wood for discussions regarding desiderata in proof simplification, Amaury Hayat for providing guidance throughout the project. Kunhao Zheng for providing insights on the RL experiments, and many other members at FAIR for various technical contributions, suggestions, and insightful discussions.
10

---

Published as a conference paper at ICLR 2026
REFERENCES
Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. GPT-4 technical report. arXiv preprint 23xx:23333.87744
2023. (Cited on pg. 24)
Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, and Sean Welleck. Improver: Agent-based automated proof optimization. arXiv preprint arXiv:2410.04753, 2024. (Cited on pg. 2, 3, 5,5,9
Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. Pantograph: A machine- to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in Iean 4. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 104 123. Springer, 2025. (Cited on pg. 16)
Hugh Leather Aram H. Markosyan, Gabriel Synnaeve. Leanuniverse: A library for consistent and scalable lean4 dataset management. htttps://githin com/ facebookresearchh LeanUniverse, 2024. (Cited on pg. 16)
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-Ieer mathematics. arXiv preprint arXiv:2302/24333 2023. (Cited on pg. 9, 16)
Ian Betlot-Attwell, Frank Rudzicz, and Xujic Si. Library learning doesn't 't: The curious case of the single-use" library". arXiv preprint 2rXiv:2410.20274, 2024. (Cited on pg. 9)
Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, and Fan Yang. Reviving dsp for advanced theorem proving in the era of reasoning models. arXiv preprint at 250. 2025. (Cited on pg. 9)
Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma. et al. droderrover: Deep and broad reasoning for automated theorem proving, 2025. URI. https://arxiv. org/abs/2507.23776, 2025. (Cited on pg. 1, 9, 23)
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Ka- plan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings. Matthias Plappert, Fotios Chantzis, Elizabeth Barnes, Ariel Herbert- Voss, William Hebgen Guss, Alex Nichol. Alex Paino, Nikolas Tezak, Jie Tang. Igor Babuschkin, Suchir Balaji, Shantanu Jain, William Saunders, Christopher Hesse, Andrew N. Carr, Jan Leike, Josh Achiam. Vedant Misra, Evan Morikawa, Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katie Mayer, Peter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and Wojeiech Zaremba. Evaluating large language models trained on code, 2021. URL peetts::/aarxie wttp/org//aab//oooe/oe 03374. (Cited on httpt:/s///aaiii..ogg///////////
pg. 3, 40)
Gheorghe Comanici, Eric Bieber, Mike Schaekermann, Ice Pasupat, Noveen Sachdeva, Inderjit Dhillon, Marcel Blistein, Ori Ram, Dan Zhang, Evan Rosen, et al. Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities. arXiv preprint arXiv:2507.06611 2025. (Cited on pg. 24)
Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp Automated Deduction CADE-25 25th International Conference on Automated Deduction. Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pp. 378 388. Springer, 2015. doi: 10.10077978-3-331 3-188-33319-2111111 18119-214011 2000-2140-6))) 26. URL https: //doi.org/1001 1007/978--111 3- 319 20-01 6_26. (Cited on pg.
Kefan Dong and Tengyu Ma. Stp: Self Self-play Ilm theorem provers with iterative conjecturing and proving. arXiv preprint wrXiv:2502.00212. 2025. (Cited on pg. 9, 16)

---

Published as a conference paper at ICLR 2026
Kevin Ellis, Lionel Wong, Maxwell Nye, Mathias Sable-Meyer, Luc Cary, Lore Anaya Pozo, Luke Hewitt, Armando Gezar-Lezama, and Joshua B Tenenbaum. Dreamcoder: growing generalizable, interpretable knowledge with wake-sleep bayesian program learning. Philosophical Transactions 2023. (Cited on pg. 9)
of the Royal Society A, (8815)2))
Simon Frieder, Jonas Bayer, Katherine M Collins, Julius Berner, Jacob Loader, András Juhász, Fabian Ruehle, Sean Welleck, Gabriel Poesia, Ryan-Rhys Griffiths, al. Data for mathematical copilots: Better ways of presenting proofs for machine learning. arXiv preprint arXiv:2412. 15/84 2024. (Cited on pg.
Dhruv Gautam, Spandan Garg, Jinu Jang, Neel Sundaresan, and Roshanak Zilouchian Moghaddam. Refactorbench: Evaluating stateful reasoning in language agents through code. In NeurIPS 2024 Workshop Open-Worle Agents, 2024. (Cited on pg. 9)
Jonas Gehring, Kunhao Zheng, Jade Copet, Vegard Mella, Quentin Carbonneaux, Taco Cohen, and
Gabriel Synnaeve. Rlef: Grounding code Ilms in execution feedback with reinforcement learning. arXiv preprint arXiv:2410.0208/
2024. (Cited on pg. 5)
Vladimir Gladshtein, George Pirlea, and Ilya Sergey. Small scale reflection for the working lean user. arXiv preprint arXiv:2403. 2024. (Cited on pg. 9)
Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. Abel: online reinforcement learning for neural theorem proving. In The 4th Workshop on Mathematical Reasoning and Al at NeurlPS'22 '4, 2024. (Cited on pg. 9)
Sample efficient
Gabriel Grand, Lionel Wong, Maddy Bowers, Theo X Olausson, Muxin Liu, Joshua B Tenenbaum, and Jacob Andreas. Lilo: Learning interpretable libraries by compressing and documenting code. arXiv preprint arXiv:2310. 2023. (Cited on pg. 9)
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.1 12283,, 2022. (Cited on pg. 16)
Neil Jones. An introduction to partial evaluation, ACM Computing Surveys (CSUR), 28()):80-5533 1996. (Cited on pg. 9)
Cezary Kaliszyk and Josef Urban. Learning-assien assisted theorem proving with millions of lemmas. Journal of symbolic computation, 69: 199-119,2,, 2015. (Cited on pg. 9)
Michael Kinyon. Proof simplification and automated theorem proving. CoRR, /wtp//888.0421,, 2018.
URL http: /ttp:///axiiii org/ abs 1108 04251. (Cited on pg. 9)
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. Advances in neural information processing systems, 35:26337-26344 2022. (Cited on pg. 9)
Jia LI, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang, Kashif Rasul, Longhui Yu, Albert Jiang, Ziju Shen, Zihan Qin, Bin Dong. Li Zhou, Yann Fleureau, Guillaume Lample, and Stanislas Polu. Numinamath. [https:/ /huggingface. 1.51 (attps://githuu) wttp://teooooopoooeeeeooeoeeo
co MOO/AI-MO/Numinenn (Cited on pg. 16, 17)
2024.
Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. arXiv preprint 2444v92404.09939, 2024. (Cited on pg. 9)
Haohan Lin, Zhiqing Sun, Sean Welleck, and Yiming Yang. Lcan-star: Learning to interleave thinking and proving. arXiv preprint arXiv:2407. 10040, 2024. (Cited on pg. 9)
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 preprint arXiv:2502.07644 2025a. (Cited pg. 5, 9, 16, 17)
12

---

Published as a conference paper at ICLR 2026
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al. groedel-poover-o Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508.03000 2025b. (Cited pg. 1,
Junqi Liu, Xiaohan Lin, Jonas Bayer, Yael Dillies, Weijie Jiang, Xiaodan Liang, Roman Soletskyi, Haiming Wang, Yunzhou Xie, Beibei Xiong, et al. Combibench: Benchmarking Ilm capability for combinatorial mathematics. arXiv preprint arXiv:2505.03171: 2025a. (Cited on pg- 16)
Zichen Liu, Changyu Chen, Wenjun Li, Penghui Qi, Tianyu Pang, Chao Du Wee Sun Lee, and Min Lin. Understanding rl-zero-like training; A critical perspective, 2025b. URL https:
//aaaxi..rggab////...aaaa 2503 20783. (Cited on pg. 4)
Daniel Mankowitz, Andrea Michi, Anton Zhernov, Marco Gelmi, Marco Selvi, Cosmin Paduraru, Edouard Leurent, Shariq Iqbal, Jean- WannBappistt Lespiau, Alex Ahern, et al. Faster sorting algorithms discovered using deep reinforcement learning. Nature, 618(7964):257-266) 2023. (Cited on pg. 9)
The mathlib Community. The lean mathematical library. CoRR, abs/1910.09336, 2019. URL
http::/ org/abs//////ooooooo.......o.. 1910. 09336. (Cited on pg. 2)
Azim Ospanov, Farzan Farnia, and Roozbeh Yousefzadeh. Apollo: Automated Ilm and lean collab- oration for advanced formal reasoning. arXiv preprint arXiv:2505.05755, 2025. (Cited on pg. 9)
Stanislas Polu and lla Sutskever. Generative language modeling for automated theorem proving. arXiv preprini arXiv:2009.0339) 2020. (Cited on pg. 9)
Shree Prakash Rahul and George C Necula. Proof optimization using lemma extraction. Computer Science Division, University of California, 2001. (Cited on pg. 9)
ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Decpseek-prover--2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21811, 2025. (Cited on pg. 9)
Raimondas Sasnauskas, Yang Chen, Peter Collinghourne, Jeroen Ketema, Gratian Lup, Jubi Taneja, and John Regehr. Souper: synthesizing superoptimizer. arXiv preprint arXiv:1711 111111111444 1.04422, 2017. (Cited on pg.
Eric Schkufza, Rahul Sharma, and Alex Aiken. Stochastic superoptimization. ACM SIGARCH Computer Architecture News, 41(1):305-316, 2013. (Cited on pg. 9)
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models, 2024. URL 2402. 03300. (Cited pg. 4)
orr.aiiiiorg....ooooooooooooooor orgoorgggaaooo abs/
Alexander Shypula, Aman Madaan, Yimeng Zeng, Uri Alon, Jacob Gardner, Milad Hashemi, Graham Neubig, Parthasarathy Ranganathan, Osbert Bastani, and Amir Yazdanbakhsh. Learning performance- improviingggi code edits. arXiv preprint arXiv:2302.07867, 2023. (Cited on pg. 9)
Qwen Team. Qwen2.5: party of foundation models, September 2024. URL https:://
github. http///////ooeeooeeeeeeoooeeeoee http///lgg/w///..mmmm// qwen2. 5/. (Cited on pg. 24)
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Ami- tayush Thakur, and Swarat Chaudhuri. PutnamBench: Evaluating neural theorem-provers on the putnam mathematical competition. Advances in Neural Information Processing Systems, 37: 11545-11569, 2024. (Cited on pg. 5, 9, 16)
Jifí Vyskočil, David Stanovsky, and Josef Urban. Automated proof compression by invention of new definitions. In International Conference Logic for Programming Artificial Intelligence and Reasoning, pp. 447-462. Springer, 2010. (Cited on pg. 9)
Christian Walder and Deep Karkhanis. Pass@ k policy optimization: Solving harder reinforcement learning problems. arXiv preprint 252. 2025. (Cited on pg.
13

---

Published as a conference paper at ICLR 2026
Haiming Wang. Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.006330 2023. (Cited on pg. 9)
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prove preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint wrXiv:250..133555 2025. (Cited on pg. 9)
Mark Weiser. Program slicing. IEEE Transactions on software engineering, (4):352-357, 2009. (Cited on pg. 9)
Christoph Wernhard and Wolfgang Bibel. Investigations into proof structures. Journal of Automated Reasoning, 68(4):24, 2024. (Cited pg. 9)
An Yang. Baosong Yang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Zhou, Chengpeng Li, Chengyuan Li, Dayiheng Liu, Fei Huang, Guanting Dong, Haoran Wei, Huan Lin, Jialong Tang, Jialin Wang, Jian Yang. Jianhong Tu, Jianwei Zhang, Jianxin Ma, Jin Xu, Jingren Zhou, Jinze Bai, Jinzheng He, Junyang Lin, Kai Dang, Keming Lu, Keqin Chen, Kexin Yang, Mei Li, Mingfeng Xue, Na Ni, Pei Zhang. Peng Wang. Ru Peng, Rui Men, Ruize Gao, Runji Lin, Shijie Wang. Shuai Bai, Sinan Tan, Tianhang Zhu, Tianhao Li, Tianyu Liu, Wenbin Ge, Xiaodong Deng, Xiaohuan Zhou, Xingzhang Ren. Xinyu Zhang, Xipin Wei, Xuancheng Ren, Yang Fan, Yang Yao, Yichang Zhang, Yu Wan, Yunfei Chu, Yuqiong Liu, Zeyu Cui, Zhenru Zhang, and Zhihao Fan. Qwen2 technical report. arXiv preprint arXiv:2407. 1, 2024a. (Cited on pg. 16)
Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: new frontier in ai. arXiv preprint arX1v:2412.16075.
2024b. (Cited on pg. 9)
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. Advances in Neural Information Processing Systems, 37: 17710888--10886, 2024. (Cited on pg. 16)
Zhouliang Yu, Ruotian Peng, Keyi Ding. Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, et al. Formalmath: Benchmarking formal mathematical reasoning of large language models. arXiv preprint arXiv:2505.022 02735, 2025. (Cited pg. 16)
Yang Yue, Zhiqi Chen, Rui Lu, Andrew Zhao, Zhaokai Wang, Yang Yue, Shiji Song, and Gao Huang. Does reinforcement learning really incentivize reasoning capacity in lims beyond the base model?, 2025. URL https: / arxiv. org/ abs 2504 13837. (Cited on pg. 5)
Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah Goodman. Star: Bootstrapping reasoning with reasoning, Advances in Neural Information Processing Systems, 35:15476-15488, 2022. (Cited on pg. 4)
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110 2021. (Cited on pg. 2, 5,
16)
Jin Peng Zhou, Yuhuai Wa, Qiyang Li, and Roger Grosse. Refactor: Learning to extract theorems from proofs. arXiv preprint arXiv:2402. 17032, 2024. (Cited on pg. 9)
Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, Anthony Bordg, Jun Wang, and Haitham Bou Ammar. Bourbaki: Self-generated and goal-conditioned mdps for theorem proving. arXiv preprint arXiv:2507.00272 2025. (Cited on pg. 9)
14

---

Published as a conference paper at ICLR 2026
A DISCLOSURE OF USE OF LLMS (ICLR 2026 REQUIREMENT)
In line with the LLM usage disclosure policy for ICLR 2026 submissions, we report our usage of LLMs the following:
Design and polish matplotlib and seaborn figures in the paper (ChatGPT)
Write LaTeX code for tables, figures, and listings, including aesthetically enhancing the styles (ChatGPT)
Polish and edit text in the paper (ChatGPT)
Find relevant citations for related work (ChatGPT)
Assist in producing code for experiments (GitHub Copilot in VSCode, ChatGPT)
15

---

Published as a conference paper at ICLR 2026
B
LEAN BASE MODEL AND PROOF SIMPLIHICATION DATA DETAILS
B.1 GENERAL BASE MODEL FOR LEAN
we train a general-purpose base model in Lean by fine-tuning Owen-2: 2. 5-.5-7B 7B- Instruct (Yang et al., 2024a) on around IB Lean tokens. The model is fine-tuned on a combination of diverse math and Lean-related tasks, as follows:
First,
Natural Language Problem Solving: The model is trained on natural language mathe-
maties problems with associated solutions so that it has general math capabilities. We use NuminaMath-1. (LI et al., 2024), high-quality set of such pairs.
Lean Code Completion: We use a subset of Lean code from GitHub, using GPT-4o with heuristics classify whether code is Lean 3 or Lean 4. We include only the Lean subset of the code.
Auto-formalization: In order to teach the model to associate natural language with Lean, we train the model to perform nnttoffommaliztion of both problems and solutions from natural language to Lean 4 in our data mix. For problems, we use natural language problems with Lean problem statement formalizations from high-quality datasets: CombiBench (Liu et al., 2025a), Compfiles, FormalMATH (Yu et al., 2025), Goedel-Pset (Lin et al., 2025a), Lean Workbook (Ying et al., 2024), m2niF2 (Zheng et al., 2021), ProofNet (Azerbayev et al., 2023), and PuthamBench (T (Tsoukalas et al., 2024). We include solution autoformaliza- tion data from the Coedel-Psee Pset -v1 Sol ved dataset by mapping Lean solutions with natural language solutions.
We use a set of conjectures and proofs from STP (Dong & Ma, 2025), which is diverse collection of theorems and proofs in Lean generated via expert iteration while training their model.
Formal Theorem Proving:
Tactic and Proof State Prediction: Finally, to teach the model about proof states, we use pre-extracted data from LeanUniverse (Aram H. Markosyan, 2024) and extract additional data using the Pantograph (Aniva et al., 2025) tool. For each proof STP, we extract each tactic, well as the proof states before and after the tactic. The model is given the proof state before the tactic and asked to predict both the tactic and the proof state following the tactic.
B.2 GENERATING A DATASET OF THEOREMS AND PROOFS FOR SHORTENING
After creating a Lean base model, we next describe how we generate a training dataset of proofs to be shortened. To do so, we first present recipe for generating interesting theorems.
Formalizing Proofs with Sketches to Derive Subtheorems While there are many datasets such as Goedel-Pset and Lean Workbook we find that they have a high density of simple computa- tional problems posed as proofs rather than high-quality proving problems. In Goedel-Pset, estimate that only 5% of the problems are proof problems". leading to a lack of high-quality theorem proving data. To combat this, develop a technique generate diverse and interesting theorems based on the idea of proof sketching (Jiang et al., 2022).
The key idea is that can leverage existing natural language solutions identify core steps in proof. We first train our Lean base model to take natural language solution and auto-formalizing into a high-level proof, which we call proof sketch, an example shown in Listing 1. In the proof sketch, core steps are represented via have statements, and lower-level details are omitted and left as 3 sorry statements. We then filter sketches are then filtered by the Lean compiler to remove non-compiling sketches.
Once we have set of compiling sketches, we extract each sorry goal into new theorem via the extract cract.goall 1 tactic, which turns it into theorem that is equivalent to what needs to be proved at that particular sorry. For example, extracting the second sorry in Listing results in the theorem shown in Listing 2. By extracting these sorry statements, we are able to generate 518K theorems.
We estimate whether problem is computational problem via a heuristic filter of whether the problem has any of the keywords: prove, show, establish, demonstrate, verify
16

---

Published as a conference paper at ICLR 2026
Uheozem worn__o www.aoooopuuuuuouoooo 22_32_2532 (a (bo
ta 11 maann (hr Dr
(hg
+ = 1)
(hs
(h4
(hş E Finset. range b
in Finset.range n, la k ia is arichmetic sequence. := by
12 3) 2"a
:- by
1: Prove that the
have lemmal V B. a (n sorry
2: Express ann torma of n. =
have lemnal sorzy
teama 3: Express Bann in borma of D. sarry
2n
Leams d: Calculate the sum of the first Lerma of the sequence fa_a BLok. have lemmad n, in Finset. nr (a sorry
unn A 2"a xm by
Apply Jemmaá conclude exact lemma4 n
Listing I: Example of proof sketch
Lheorem lean_ Beaa__oorbook_pph plus (alel_22522___2 www.22.x.cacceeee....eee.. extracted 1_1 la b. + BJ
(bo 0 A C b)
(hi
(bg V in No, b (n 11 = a Obg 11 (hg =
11 (hs
E k
Pinser sereerraage range 3, 7) (lemmal V N), (n
2)
sorry
Listing Example an extracted theorem
Fine- Sone-Tuning our Model for Proof Sketching In order to fine-tune our model for proof sketching, first curate dataset of natural language problems (with corresponding Lean problem formaliza- tions) and solutions by combining Goedel -Pset-vl (Lin et al., 2025a) with NuminaMath-133 (LI al., 2024). Then, use Qwen 22 5 3-32B-- ----------nntt Instruct produce proof-sketches based these natural language solutions similar to that in Listing 1. We filter out compiling sketches and train our Lean base model on them. In Table 4, we show the results of fine-tuning. Since measure the objective correctness of sketch, we use the proxy of compile rate, finding our model performs better than Owen2. 5-3 and is smaller and can do inference faster.
be tricky to
Table 4: Proof sketching ability of models
Model
compile@1
compile@11 16
Qwen2.5 7B (zero-shot)
3.6
7.0
Qwen2.5 7B (one-shot)
4.9
19.0
Qwen2.5 32B (zero-shot)
21.1
62.0
Qwen2.5 32B (one-shot)
35.1
75.0
Ours (7B)
54.8
89.1
Generating Proofs for Simplification Because proof sketching generate steps sub-theorems that are too incremental, we first filter out trivial theorems that can easily solved by automation tacties in Lean. For example, the first sorry in Listing is just restatement of hypothesis h and can be solved via rfl. While this theorem is correct, it is not challenging for the model. Therefore, we design an AUTO tactic (Listing that tries series of Lean automation tacties such as 1 linaritt tith and a sesop to filter out these simple theorems, leaving 307K of the original 518K theorems (filtering 41%).
17

---

Published as a conference paper at ICLR 2026
For the remaining theorems, attempt generate proofs of these theorems with Goede1-Prover-VZ 32B, strong open-son source proving model. With attempts per theorem, the model is able to prove 145K theorems, which use targets for proof simplification. Statistics and zerexamples of these proofs can found in the next section, Appendix B.3.
"AUTU" tactic =>
(tactic)
repeat
(try rfl
try tauto
assumption
try norm_aum
ring_nf at
try ring_nf!
nat_ve_decide
Lry omega
simp [A]
try field_rimp =t
poaitivity
linarith
try nlinorith
exact?
try aesop!)
Listing 3: AUTO tactic for filtering trivial theorems
B.3 STATISTICS OF PROOF SIMPLIFICATION TRAINING DATASET
The minimum, Q1, median, Q3, and maximum proof lengths of our training dataset are 1, 103, 204, 411, and 10958. The mean is 334. Fig. 8, we show the distribution of lengths, observing its right-skewed nature. Examples of proofs shown in Listings 4 and 5. Compared to the proofs in our evaluation sets, we observe that training proofs often have more unused hypotheses, as they derived from extracting the proof state, which may contain hypotheses that not used for that particular sub-goal.
Histogram of Proof Lengths
25K
20K
Frequency
15K
10K
5K
0
0
25.
500
750
1000
1250
1500
1750
2000
Proof Langth
Figure 8: Histogram of proof lengths.
18

---

Published as a conference paper at ICLR 2026
Lheorem extracted_]
(ha S a)
(aal $ 1) (hb
(1
(1emmal 1
s 1 (1 a)) (1emma2 b 2 21 [1emme]
(lemma4 b $
1 c by
h_main
by_contra
Assume foz contradiction that D E 3/4
have àt
4 linerith
From lamma2, 5 2 1 1-- k0, and from lommal, 1 2 3/4
linarith
have 1amma3,
22 :- by linerith la 3/4
3/4, 30
Solve
1/2
have h4 : a 1 / := by
h41 nlinarith
2
by
have ha2 alinsrith
/
by
have has : a / 2 - 1m by
alingrith
Hnarith
Substitute 1/2 into
1/12
have hs b = 19 / 24 1= by
[hb]
[h4]
mcm
15/24 3/4, s0 3/4, contradiction
have 3g : b :m by
norm_ncm
linarith
exact h_nain
Listing 4: Example of Proof Simplification Training Task (Length 158)
19

---

Published as a conference paper at ICLR 2026
Lheorem extracted_] N) (hn 3 S
(1emmal Nat,oard 7ik & n
0)
n)
4
Nat. 7[k S
k
by
Nat.card tik
A 01
have 31 (k N.
S
01 Set.icc 1 in im by
apply Set.cxt
intro K
simp only [Set. sete mem constructor
intro h
ha have ha k # 0 h.2
h4 I by by_contra
If 1, then &
since & is natural number
have k
omega contradiction
exact (h4, h2)
int
have bi 1 < k h.1
have hy k S n
h.2
have h4
S
have hy k y :- by
byntoni hs
-- TF 9, then S R would be false
have ho : 0 =- by simga using ha
exact (ha, ho)
[h1]
Calculate the cardinallty of the set HI, a 1) have Nat.card
N) -- Use the fact that the cardinailty of the interval 17, 1a have ha n 12 :- by hn
by
have h4
omage
Use formola for cardinality the interval
fact
cardinality
interval [1, n
[Fintype.cm wantype.card_ofie card_ofrinsett]
Convert the set to finset and caiculate its cardinality
<2> simp (einset.
Finset. randeteerrd_aane,, sat.succ_le_iff)
<+> cases n with
contradiction
suce =>
cases
zero => contradiction
succ n =>
with
zero => contradlation
suce
simp_ell
range, Nat. secc__e
<z> ring_nf
<f> omego
FM [h2]
hamain
Listing 5: Example of Proof Simplification Training Task (Length 295)
20

---

Published as a conference paper at ICLR 2026
C TRAINING METRICS THROUGHOUT RL
In Section 1,1, we observed that expert iteration leads to higher diversity as witnessed by better @32 metries, while reinforcement learning with standard reinforcement learning algorithms maximizing expected rewards leads to higher @ metrics, In Figure 9, we show the evolution of proof shortening @ed@1 alongside red@32. Initial @32 metries are slowly distilled into @1, but the improvement on @32 metrics is limited.
Rolative shorteaing (%)
65
Rolaive shar Mharteaing (90
16
60
14
12
55
10
50
50
100
150
50
100
150
Step (k)
Step (k)
(a) miniF2F red
(b) PutnamBench red
Relative shortening (%5)
Rolative Shortening (%)
22
72
20
68
18
25
30
25
Step
Step (k)
(c) miniF2F red 32
(d) PutnamBench red @2
Figure 9: Reduction metries @ and @32 over the course RL. GRPO maximizes red @ cost of diversity, as red @ @32 only marginally increases in comparison.
21

---

Published as a conference paper at ICLR 2026
D FULL RESULTS AND ADDITIONAL ANALYSIS OF ITERATIVE PROOF SHORTENING
D.1 TABLE OF ITERATIVE PROOF SHORTENING RESULTS
Table 5 is tabular form of Fig. 4, showing the proof length after each iteration of proof shortening.
Table 5: Min@64 64 (rounded nearest integer) and reduction (%) of miniF2F and Putnam proofs across inference-time iterations. Iterations are done with 64 samples, and - 8 with 1024 samples.
Dataset
Model
Orig
Lint
It
2
3
1t
5t
6
7
8
Min @ 64
334
302
144
126
121
117
106
104
88
75
miniF2F
Red 64 (%)
0.0
9.2
76.6
80.0
81.0
81.5
82.9
83.1
85.7
87.9
Min @ 64
1468
1359
1123
1061
1024
1007
975
969
811
Putnam
Red@6 64 (%)
0.0
7.4
34.8
40.0
42.5
43.6
46.4
47.1
52.2
57.2
D.2 EFFECT OF к ON MIN @ K AND RED @ K. THROUGHOUT SIMPLIFICATION
In this section, analyze the effect of increasing k on min@k and red@k. First, we analyze this trend when attempting to simplify the initial, linted proof, shown in Table and Fig. 10. We observe relatively log-linear gain in both metries.
For comparison, we analyze the same trend but for simplifying proofs that have already gone many iterations of simplification. In Fig. 11, we analyze proofs that have gone 7 iterations of proof simplification. We see a different pattern, where min @k falls slower for lower & and then log- logliinearly afterwards. Intuitively, as proofs become more simplified, they become harder to simplify low-shot setting, and exploring more diverse simplifications becomes erucial.
Table 6: Min @k and Red @k for increasing values of k
Dataset
Metric
Original
Linter
@2
@4
@8
Min@k Red@k (%)
334
302
142
141
139
137
134
miniF2F
0.0%
9.2%
77.1%
77.3%
77.7%
78.1% 1%
78.6%
Min@k @ed@k (%)
1468
1359
1120
1117
1112
1105
1094
PutnamBench
0.0%
7.4%
35.2%
35.5%
35.9%
36.5%
37.3%
Dataset
Metric
@32
@ 64
@ 128
@ 256
@ 512
@ 1024
Min@k Red@k (%)
130
126
122
118
1 114
1 110 82.4%
miniF2F
79.2%
79.9%
80.6%
81.2%
81.8%
Min @k
1080
1063
1043
1023
1004
987 45.7%
PutnamBench
@ed@k (%)
38.4%
39.7%
41.3%
42.9%
44.3%
Mingk (minif21)
Reddkk (minil 21!
Mingk (Putnsm@ench))
Redøkk (PutnamBench)
B25
136
Radiacti 1961
R1.0
128
Mnnk
Redluction
1250
78.0
37.5
35.0
256
1024
16
64
256
1924
256
1024
66
1028
Figure 10: Effeet of scaling & (sample count) on Min and Red@k (initial iteration)
22

---

Published as a conference paper at ICLR 2026
Mingk (MINIFZF)
Redgk (miniF2F)
Mingk (PutnamBanch)
Redgk (PutnamBench)
570
84-
(50
Mirkk
960
19.5
840
78-
52.5
1004
236
250
Figure 11: Effect of scaling &t (sample count) on Min@k k and Red@k k (later iteration)
D.3 DETAILS ON SEED-PROVER IMO PROOF SHORTENING
Earlier in 2025, Seed-Prover released Lean proofs of four problems that the model successfully solved from the 2025 International Mathematical Olympiad (IMO) (Chen et al., 2025). They solved problems 3, 4, and 5 were solved during the contest window, and problem later after the competition. However, the proof's of these problems extremely verbose, especially compared to their informal counterparts. Using iterative proof shortening, our ProofOptimizer is able to successfully reduce the proof length of their proofs for P3, P4, and P5 by over half, as well as the longer P1 by 43.8%. In addition, we find that our shortened proofs for P4 and P5 show a 25% and 81% (respectively) speedup over the original proofs (Table 7).
Table 7: Results for ProofOptimizer + Iterative Shortening on IMO 2025 Proof Simplification
Length
Runtime
Problem
Original
Simplified
Reduction
Original
Simplified
Speedup
P1
36478
20506
43.79%
399.7
392.3
1.02x
P3
16377
7907
51.72%
39.7
39.1
1.02
P4
29147
14531
50.15%
453.8
362.5
1.25
P5
8658
4002
53.78%
61.0
33.7
1.81
We use proofs from the official GitHub repository using Mathlib 4.14.0 (our model was trained on Mathlib 4.19.0). Before shortening, we replace invocations of exact? and apply? y with the actual proof that is found. Each of the proofs is divided into a collection of smaller lemmas and theorems (problems 1, 3, 4, and have 80, 52, 88, and 14 theorems, respectively). Since running iterative shortening on the entire proof will suffer from long context issues, we treat each sub-lemma/sub- theorem an individual target for shortening. At the end, combine the shortened theorems to produce the complete shortened proof. When feeding a sub-theorem into ProofOptimizer, we include context the theorem definition (but not proof) of all other theorems that occur in its proof. Finally, to ensure the correctness of our simplified proofs, we use Safe Verify to confirm that all four simplified proofs match the specification of the original proof without any environmental manipulation. We remark that our setup does not consider the space of structure-level simplifications, as we retain all sub-theorem statements from the original proof and only simplify their proofs. In addition, as our proof length metric only measures the length of proofs, it does not take into account unnecessarily long or redundant sub-theorem statements.
As this experiment aims to provide simple demonstration of the potential of our approach rather than perform controlled scientific study, we do not fix the number of iterations or samples per iteration across problems. Approximately, we use 15-20 iterations of shortening with 64-4096 samples per iteration. Taking inspiration from the analysis Sec. D.2, we generally use less samples for the first few iterations and increase the number of samples for later iterations to maximize reduction per sample. We also allocate more samples to sub-theorems that show more simplification potential in early iterations. In total, we used approximately 3000 H100 GPU hours per problem.
23

---

Published as a conference paper at ICLR 2026
E COMPARISON WITH QWEN2.5, GPT-40, AND GEMINI-2.5-PH5
In Table 8, we compare ProofOptimizer models with several off the shelf models, namely Qwen 2.5 (Team, 2024), GPT-4o (Achiam al., 2023), and Gemini-2.5-PP (Comanici al., 2025). For all models, we feed the output of the symbolic linter as input, and report overall reduction with respect the original (unlinted) proof.
Table 8: Proof length miniF2F and PutnamBench proofs for various models. Specially trained proof minimization models outperform prompted off-the-shelf models. Reinforcement learning achieves best @ metrics but at the cost of reducing diversity, as witnessed by improved @ 32 metrics with expert iteration.
Dataset
Model
Min@1 Min@32
@ed@1
@ed
Original
334
0.0%
Linter
302
9.2%
Qwen2.5-7B
294
267
25.7%
41.8%
Qwen2.5-32B
288
252
30.0%
47.3%
miniF2F
GPTT-4
283
258
35.2%
47.9%
GPT-4o States
266
290
32.9%
46.5%
Gemini-2.5-Pro
280
207
31.6%
62.0%
Gemini-2.5-Pro- + States
283
208
31.6%
62.0%
ProofOptimizer-Expli
241
153
53.9%
74.9%
ProofOptimizer-RL
190
152
67.1%
73.4%
Original
1468
0.0%
Linter
1359
7.4%
Qwen2.5-7B
1358
1339
9.0%
14.8%
Putnam Bench
Qwen2.5-32B
1353
1304
10.9%
20.7%
GPT-4o
1355
1336
10.9%
18.2%
GPT-4o States
1379
1358
9.3%
15.9%
Gemini-2.5-Pro
1348
1303
12.7%
24.5%
Gemini-2.5-Pro- States
1371
1319
11.5%
24.1%
ProofOptimiize--Expt
1328
1161
15.2%
31.9%
ProofOptimizer-RL. 1303
1258
21.6%
27.1%
In Fig. 12, compare the specific optimized proofs between Gemini and ProofOptimizer. For both data sets it can be seen that the longer the proof, the more challenging it is to shorten This is because although long proofs have more potential for shortening, the models struggle to maintain correctness them. Still, ProofOptimizer able to bring some improvements for the long proofs (see the top right part of the PutnamBench plot). In miniF2F, there is significant number of proofs that can be minimized to just one step, which typically boils down to invoking one proof automation tactic (like linari instead of applying sequence of more explicit proof steps.
24

---

Published as a conference paper at ICLR 2026
miniF 2F
PutnamBench
1000
1000
Optimized
Optimized
10
10
1-
1-
10
100
1000
10
100
1000
Original
Original
Model
Gemini-2.5-Pm
ptmizer
Figure 12: Comparison of optimized proofs between ProofOptimizer (green) and Gemini 2.5 Pro (yellow)
25

---

Published as a conference paper at ICLR 2026
F FULL RESULTS AND EXTENDED ANALYSIS OF REPAIR WITH EXECUTION FEEDBACK
This section contains the full results of the experiments in Sec. 4.2. All simplification attempts done on the set of linted proofs. Table 9, Figure 13, and Figure 14 are extended versions of Fig. 3 for both PutnamBench and miniF2F. The settings are as follows:
ProofOptimizer: ProofOppimiier-Esppii with simplification attempts per proof.
Repair: The previous setting, with attempted repair by Goede -areellrrroeeee Provrr-------2332
Repair Linter: The previous setting, with our linter applied to all proofs.
ProofOptimizer (@ 128): ProofOptimiier-Explt with 128 simplification attempts per proof
ProofOptimizer (@ 64x2): ProafOppimizzr-FExph with 64 simplification attempts per proof, and the best simplified proof for each problem is then fed back for additional 64 attempts.
We remark that these baselines normalizing for sample count rather than running time. Sampling repair from Goedel -eeee---reeryye - takes considerably longer than sampling simplification from our model. This both because is larger model (32B vs. 7B) and because their model relies on CoT, causing their average response length to be significantly longer than ours.
Table 9: Results of execution- based repair strategies
Dataset
Model
Min @ 64
Min@64 64 x
R Red@64 x
Linter
302
9.2%
ProofOptimizer
144
75.5%
+ Repair
136
77.3%
miniF2F
Repair Linter
132
77.9%
ProofOptimizer @ 128)
130
78.9%
ProofOptimizer (It 2)
125
80.2%
Linter
1359
7.4%
ProofOptimizer
1123
32.9%
Putnam
+ Repair
1113
35.3%
Bench
Repair Linter
1107.2
35.7%
ProofOptimizer (@ 128)
1099
36.5%
ProofOptimizer (44x2)
1095
37.0%
Length
1945
1944
1245
1944
Tapar
Fager
Tapar
Poet
Poofess
Pooffet
Figure 13: Results of Execution -ased Repair with Goedel-Prover
26

---

Published as a conference paper at ICLR 2026
Goedel Repair (miniF2F)
Goedel Repair (Putnam)
Simplified (Wreng)
Simplified (Wrong)
Simplified (Correct)
Simplifled (Correct)
Repaired (Correct)
Repaired (Correct) y=x
Wrong and Repaired Lengths (log scale)
y=x
Wrong and Ropaired Lengths (log scate)
10*
10a
101
10
10c
102
102
10a
Original Length (log scale)
Original Length (log scale)
Figure 14: Comparison of Proof Lengths with Execution- -Bssed Repair
Finally, in Listings 6 and 7, show example of proof that successfully repaired. Note that the repaired proof has many components in common with the original proof.
theozem mathh__umber
theozem mathd seid__numberrr theorry_ Wrong (... statement emitted) :- by
(z N0 tho
1342 & 131 th1
EM [ho]
(hg 1342/n) (hg
13 r) by
have 8 13 < 3 == by omego
6710 $ nn:" :-:::bp have
obtain (k, rfl) : h2
omega
have h_main 6910 S n by
have :
by
theozem mathd www.nnneeeebbbueeeee_ (... statement emitted) :- by
Correct
[h_=] at hg
h_=
by
obtain (k, +f1) :4
[ho]
have as : k := by by_contra
<3> norm_aum
<j> rfl
puaa_neg at h
have h_main 6910 $ :- by
he simp [ha] at h1
:- by omega
hg zw [h_=] at ha
by
cyncears!! hg
exact ha
have
:- by
obtain (k, rf1)
by_contra hg
by_contra!
he have hio 1342 k 2 1342 by nlinarich emega
by omega
hg
emega
interval <p> norm_num [Nat.
+ mel m=l_mod, add_add_nod, modd at ha <i> (try omega)
interval
l_aases _cases <3> norm_num (Nat. mul_mod, Nat.add_modd, Nat moo___oomodd 4 at h4
contradiction!
exact hamain
h_nain
Listing 7: Wrong Simplification and Correct Repair (Length 93)
Listing 6: Original Lean Proof (Length 126)
27

---

Published as a conference paper at ICLR 2026
G EVALUATION DATASET DETAILS
For our evaluation datasets, we use miniF2F and PutnamBench proofs sampled from Goedel-IMM SMMM/Godee-Pronee
-2-V222-2 32B. For miniF2F, we sample with temperature and top-p 0.95. For PutnamBench, we use proofs provided by the team. In both cases, we take the shortest passing proof for each problem in Mathlib 4. 19.0, resulting in 194 proofs for miniF2F and 75 proofs for PutnamBench. Table 10 and Figure 15 show summary statistics of our dataset. One sample from each dataset is shown in Listings and
As sidenote, we observe discrepency in Goedel-Prover- V2-32B's 2 results with Lean versions. Upon testing their model, we measured 90% (pass @G)) and 86 (pass@ 184) on miniF2F and PutnamBench with Mathlib 4.9, but only 80% (pass @ 64) and 75 (pass @ 184) with Mathlib 4.19. In this paper, we use Mathlib rather than 4.9, as more recent and likely more useful to the Lean community.
Table 10: Summary statistics of proof lengths in evaluation dataset
Dataset
Min
Q1
Median
Q3
Max
Mean
MiniF2F
194
13
64
167
499
2980
334
PutnamBench
75
2
608
1179
2110
5420
1468
MiniF2F Evaluation Set Lengths (n=194)
PutnamBench Eval Set Lengths (n=75)
15
Frequency
Frequency
30
20
200
400
800
1000
1200
1400
1000
2000
3000
4000
5000
Proof Length
Proof Length
Figure 15: Histograms of proof lengths for our miniF2F and PutnamBench evaluation sets.
theorom mathd_ mathd_numbe mut.ammteeorty_ygeg88
(n
(bo $
(2 ml
by
have (2
nave : (2 n) 5 12 In 51) 5 by
simp [Nat.mul_nod mat_mod_nodd]
<;> ring_nf at
<2> omega
[bz]
FM [ho]
norm_num
47 rCl
exact hn
Listing 8: Example of miniF2F Eval Task (Length 65)
28

---

Published as a conference paper at ICLR 2026
Lheozem putnam 1993_az N
B]
Ixnonzero V N, x x 01
thx V 1,
ii R, V 1,
x (n 1)
(n 11 by
momain V (n M),
1)1
intro n ha
have àt in N),
21) /xn
2)
4 in 1) := by
have h2 ix in 1)1
2 x-xx0 (n
by
ha :- (n
(hy Miarith)
simpa add assoc]
using
have hs 1x n)
1 1-
1x hn
have h4
21
111
1)
in
4 im by
linarith
have hs ix in 2)
+ m
11)
by
ring_nt at ha
linarith
have be x n # 0 :- xnonzero n
have hy have hg 18 (n 2) + x n / in 1)
11 o
+
101
x
simp [her hy] at ba nlinarith
linarith
have 3 V. in N),
21)
1x
intro n. hn induction ion' norm_num
III
have ha := h1 n
h4
Hnarihh)
simp [ddsoc] at by h4 <y>
(try norm_num at <p>
try linarith) K5>
(try simp_all [NasoeedLassoo]]
(try ring_nf at <;>
try Linarith! <;>
(tzy field_simp [xmonzero] at 52>
try slinarith)
<7>
linarith
hexiistsa
4 0201111
+ by
intro hn
have hi : (x in 1) +x (n 1)1 / x
x himain Jan (x
have : (x (n + +1
+ (n 1)1 / x 2 01 1 x 1- by rw [h1]
have :
by
simpd_simp [bz] at hg
<)>
have in
1xx
(n
: by Fnarith
exact ha
exact h_existe_a
Listing 9; Example of PutnamBench Eval Task (Length 715)
29

---

Published as a conference paper at ICLR 2026
H EXAMPLES OF PROOFS SIMPLIFIED BY PROOFOPTIMIZER
In Listings 10 to 17, we show proofs successfully optimized with ProofOptimizer and iterative shortening. Some proofs were syntactically modified to on the page (new lines removed, multiple lines compressed into one).
mathd aiggeraa_geaBB_ 338 Original
mathd mathd_ aigebra_333
+ Proof
(a b c R) (ho (h1
(a R)
b -31 (b2 a b
(bo
f -31
(h: : 1
191
(b2
19)
b
-56
a x =- 56 :- by
have a 1 :- by linarith subst_vars mlinarith
by
lave 331
= 1= by
have ha2 : la
b 9 (3
Listing 11: Simplified Proof (Length 11)
linarith
linarith
linarith
have ha a 11 by
aave 241 : -a
have h42
4 + linarith
1-3) 1m by
linarith
linarith
have ha : a :- by have 25s
ho
EM [har hal at hel
ring_nf h91
linarith
have
EM [hy]
[hs]
<3> norm_num
have by 1 by
[ha]
[ha]]
<3> norm_num
have hs b
by [har har hrl
-56 :=
<,> nomm
exact ha
Listing 10: Original Proof (Length 214)
30

---

Published as a conference paper at ICLR 2026
Lheozem jutnan_2015__a
labase 4 0 1 mallm
larac VVn 2, v
odd ((1811 N) ((181) B) .rime A (1((1a1) N: 21 2015) :m by
constructor decide
constructor
[Nat.Prime]
have b1 : V : N, (a in 10). 2) = (a [2MDO 181] := by
intro
induction' n using Nat. Nat. inducttionnnnn with n ih
reases
(
n) </>
simp_all (Int, ModBa, abase, arec] <;> omega
have h2 : (a : 2: = [2M0D 1811 = by norm_aum. "Int.ModRE abase, arec)
2015 2)
[aNou 181] by
aove hg : V : N, ta (10 k + 51 2) 0 (IMOE 181] := by
induction' k with k ih norm_num [Int. ModEq] at h2
simpa [abase, arec] using
have hy :- h1 (10
have
[10
?) have hy :- h1 [10
ha :- h1
have hg := h1 [10
k 9)
have h10 :- h1 (10
13)
[MnE.
by hro in F
<;> ring_nf at <1> omega
have
2015
(zMOD 181] by
have he la (10 201 + 53 Z1 = 0 12MOD 1811 :- h4 201
nomm_num
<;> simpa [add_asaoe] using he
exact lis exact Lat.drr__e_eenddeeeesee
Listing 12: Original Proof (Length 324)
theorem pulnan_2015__2
2) labase a 0 a
larec : V 2 2, ararrar a
(n 213
Odd (1181) N) ((18) Fr.irime (1((181) N: B1 2019)
constructer
decide
constructer
norm_num [Nat.Prime]
ru (show 2015 10 202 5 by norm_ num]
have h1 : A
(10 5) = (ZMOD 181] :- by
intro
inductien' n with ih norr_num [abage, Iw aatt.mclssccee simp_all XodEg, zrec]
ModRM)
have h2 ;- h1 lat.dvd__e_eened_ee
Listing 13: Simplified Proof (Length 82)
31

---

Published as a conference paper at ICLR 2026
Lheorem imo_1960_pp
(x R]
(ho $
x)
Real .sqrt
x11"
(b2 (4 x²2) / 11 seat.squt 1- 2-x)) 2+x 3)
(ha # 01
-11 / 2) X
45 /8
constructor nlinsrith lsg_nenneg
2)1
set 5 := Real.agrt (1 2 x1 with ha
161
hg
lave 3s2 1 2 1= 8eal "aoll_srt_ooonee by
have 1ss
[ha]
IE [Reel, s0 sgrgt <5> linarith
aave ass
5) 2
simpo [hs] using
have h5s : 5 * := by
have hasi
5)
2 by
[h]
norm_num
contradiction
have 556
1)
11
1) 2 by
ring
have Asz [hsa]
31
by
ring
have ass R)
2
18
18
by
have has1 : (5 10)
2 0 :m by
intro
have h582 12 8 Bi
0 :- by
R)
R)
2 =-
by ring
by SM [h]
contrediction
field_simp [hss]] at ha7
nlimarith
have asg (4 R) 2 12 6) hsse
16 1) =-
by
ring
alinarith [sg_nonneg (e 211
Listing 14: Original Proof (Length 330)
theorem imo_1960_pz
(x R]
(ho g
(h) (1 Real..qqs -1-3 2 x)122 * 0) x*2) / Real.sqrt 12 2-x11 2*x 9)
(h2
(hs 0)
-(1 / 2) S A x 45 / :- by
constructor
nlinsrith [sq_nennes (x 1 2) hø7 14
seal.sgrt (1 x)) Real.agrt
< 2 x1) =m by have has 11 sgr=
x))
by assumption
field_simp [bsa]
mlinorich [sq_ (show
2 by assumpticn)) by assumption),
inarithh [ag_agrt (show S
Keal. sognonggtnn (1 x)1
Listing 15: Simplified Proof (Length 125)
32

---

Published as a conference paper at ICLR 2026
Uieoren pucran 1950_*
(2
21
(hTa
31
In
letun N (0)
run
2
21
(N
20
(teun
N
(n)
run
1N0
have a_main
: No.
21
intro
heww
h2
Int
I Enduct Fan usinng Net. wong............................ ind Lon_on with
nomm_nom hTO12
simp_all cottoiact
<1>
80TH rum
no:m_nnm
<1>
simp_a11 tactoraco
nomm__an
no:m_ num hTO12]
simp_all tactoiico
<1>
nomm_nun
>>
hg
have h4 1- 1n n iby emege)
have h5 ia (a 1) lyy onegs)
onags)
5130 (h4. has ber pow_ads, paw_one, Nat.faactarsil_ucs Nat.mul_asd, Nat.aad_mol) hy
<1>
sing_nt ba H <1>
<3>
sime_all (atc. pos_add, pos_one, mul_assoc] <1>
ring_nt <p> niimarith
exect hg r. exact 21
(N 2) Iceen
(6)
by
Zunext
azve a in 2) +2 K_aain slap Pi.esdapplyl
corr_cast <1> sinp (Nat.cast_add) ring_nt apply h_nin
theoren putran 1990
( : - 21
(hT012 7
18+44.90 11fon (.)
(ffon
201.1
- +en:
IN
X
Z1112 by
rong.
natch r. with
[.3 => sinp all
simp_ail
simp_all Aac.taactorial_cccy
ring_nt
Listing 16: Original Proof (Length 320) and Simplified Proof (Length 34)
33

---

Published as a conference paper at ICLR 2026
Eleoren putran, 1968_..
22/7 Deal.pi
x14 xi14
x Real-pi
new hy if (01..l,
xi1a x021) if (01.-ly (X76 4xx 5.x14
- x22 + d RD 6.7 x
have
Ri,
x
x 18'6 4 54x74 4.x02
intro x
have h12 x R: R mlinarsth
have h1g x
x114 1876 - 4xx15 5ax14 4xx
x
ring_nt <2> miinorith leg_nonneg 21, egnnnneg 31, egnnonneg
11, egnnonneg
Lave h14 K14
42 x'21 x x (0678 4xx5 SAXTA 4x8
x72)
[h1s]
zw [h14)
tield_rimp (hi2) <p> ringunt <p> sini l512) <2 ring_nt
rM 1511 X
ru [h1]
1f (0)..l, 00'6 4-x'5 5-x"d 4-x
X Of .0)..,, x
apply
apply continuous intervallntegraaiie
continuity
apply incrrvanootoooe.eeeeeeeee
have by continuous (cen x : >> (1
213 1-
epply Continusus div
exect Continuous. ccntinecus_ conett jsontinsous_pon 2)
iatro x
have h4 : (1
by alimarith
exact
exact.
zo [t2]
aave If x in (01..l, 0x'6 1ax'5 + 54x78 4xx 6 R11 (22 linarith [Real.pi_ros]
[integral
(01..), (1 rinennt <1>
aave If
x221) Rsa1.pi
have han (f x in 101..,, 10 Ry 11 231 4 of ln (0)..,, (1 R) + 21)
- by
(f 10)..,, 18
(0)..), 11:
by
congz
ext x </> sing_nt
hag (f (0)..),
(0)..1.
2): 1- by
simp [Lntorvalantegral Integral wowe_moooottteeeeeee (Fun x 12 R) 11+xx 2011 </>
rise_nt
linarith [Rcai.pi_Dos]
in [h43
zu [an1]
hava ( in 101..., 11 x Real.pi
has
Real
IN tincagra wnw___i__on__add______e 522 norm_nun Iw [h4s:
Lave han heal.arctar, Beal-pi pi aretannnct
ha7 aral.arctan
by
aoca asctaa
[h46. h47] 91> rine_nf <1> nomm_nnn
cinganE
zu [la hg] 822 sinq_at 822 sarnane
have S_final 22/7 Reai.pi " J in (0). x 30"4 (1 x"2) by
[[_nii]] Linarith [Real.pi_pos I_nial
Resl.pi x in (31..l,
simp lshow x R, a1
221
- 4 7 221) by
ringl
ring_at
<7> lirarith [Rsa1.pt. pccs]
Listing 17: Original Proof (Length 1097) and Simplified Proof (Length 76)
34

---

Published as a conference paper at ICLR 2026
1 PROOF SPEEDUP AND SLOWDOWN ANALYSIS AND EXAMPLES
1.1 ITERATIVE PROOF SHORTENING RESULTS WITH HEARTBEAT METRIC
Table 12 and Fig. 17 show the results of iterative proof shortening using proof length heartbeats as optimization metrics. Observe that while optimizing for heartbeats isn't nearly as effective for proof length, still leads to considerable simplification.
Comparison of Min@64 (rounded to nearest integer), reduction (%), Heartbeats @ 64 (in thousands), and reduction (%) across inference-tine iterations for miniF2F and PutnamBench proofs. Iterations 1-6 use 64 samples, and 7-8 use 1024 samples. The first group shows the standard (length-optimized) setting: the second group shows the new seeartheat-optimizzer experiment.
Table 11:
Dataset
Metric
Orig
Lint
It
It
3t
4
It
It
It 7*
It 8
Optimizing for Length
Min@64
334
302
144
126
121
117
106
104
88
75
@ed@64 (%)
0.0
9.2
76.6
80.0
81.0
81.5
82.9
83.1
85.7
87.9
Optimizing for Heartbeats
miniF2F
Min 64
334
302
163
145
139
135
129
125
112
96
Red @ @4 (%)
0.0
9.2
71.3
74.8
75.8
76.3
76.9
77.4
79.0
81.3
HB @ 64 (K)
36.3
36.2
14.5
13.6
13.3
13.2
13.0
12.8
11.9
10.4
HB Red 64
0.0
0.2
43.3
46.7
48.2
48.5
48.8
49.6
51.5
57.0
Optimizing for Length
Min 64 Red@64 (%)
1468
1359
1123
1061
1024
1007
975
969
890
811
0.0
7.4
34.8
40.0
42.5
43.6
46.4
47.1
52.2
57.2
Optimizing for Heartbeats
Putnam
Min @ 64
1468
1359
1142
1092
1060
1043
1034
1031
974
904
Red @ 64 (%)
0.0
7.4
32.2
36.2
38.7
39.7
40.5
40.8
44.0
49.2
HB @ 64 (K)
221
219
199
157
155
140
136
136
122
111
HB Red 64
0.0
0.7
18.5
23.9
26.9
28.4
29.5
29.6
34.0
39.5
MIn@64 (miniF2F)
Redg66 (minIF2F)
Ming (Putnam)
Red (Putnam)
Lergt Verie
Leaan Ivet: ioattbeda Moris
60
Poaiizeddo Matric
% Reduction (
Length
60
Proof Lergot
1203
Reductton
85
40
1250
30
Proof
1.20
Longth Yeti
Lenoth Pebk: Hearthooc Marie
Heartboad Notr
Reration
Iteratioon
Iteratton
Figure 16: Optimizing for length vs. heartbeats
1.2 EXAMPLES OF PROOF SPEEDUP AND SLOWDOWN AFTER SIMPLIFICATION
Table 12 and Fig. 17 show the results iterative proof shortening using proof length vs. heartbeats as optimization metrics. Observe that while optimizing for heartbeats isn't 't nearly as effective for proof length, still leads to considerable simplification.
35

---

Published as a conference paper at ICLR 2026
Comparison of Min@64 (rounded to nearest integer), reduction (%), Heartbeats @ (in thousands), and reduction (%) across inference-time iterations miniF2F and PutnamBench proofs. Iterations 1-6 use 64 samples, and 7-8 use 1024 samples. The first group shows the standard (length-optimized) setting: the second group shows the new mecartbat-oppimiiee experiment.
Table 12:
Dataset
Metric
Orig
Lint
It 1
It
It
3
It 4
It
It 6
It 7
It 8
Optimizing for Length
Min@64 64 @4 (%)
334
302
144
126
121
117
106
104
88
75
0.0
9.2
76.6
80.0
81.0
81.5
82.9
83.1
85.7
87.9
Optimizing for Heartheats
miniF2F
Min @ 64
334
302
163
145
139
135
129
125
112
96
Red 64 (%)
0.0
9.2
71.3
74.8
75.8
76.3
76.9
77.4
79.0
81.3
HB @4 (K)
36.3
36.2
14.5
13.6
13.3
13.2
13.0
12.8
11.9
10.4
HB Red @
0.0
0.2
43.3
46.7
48.2
48.5
48.8
49.6
51.5
57.0
Optimizing, for Length
@in@66
1468
1359
1123
1061
1024
1007
975
969
890
811
Red@64 (%)
0.0
7.4
34.8
40.0
42.5
43.6
46.4
47.1
52.2
57.2
Optimizing for Heartbeats
Putnam
Min @ 64
1468
1359
1142
1092
1060
1043
1034
1031
974
904
Red @ 64 (%)
0.0
7.4
32.2
36.2
38.7
39.7
40.5
40.8
44.0
49.2
HBB @64 (K)
221
219
199
157
155
140
136
136
122
111
HB Red@64 @ 64
0.0
0.7
18.5
23.9
26.9
28.4
29.5
29.6
34.0
39.5
Ming964 (miniF2F)
Redg (miniP2F)
Ming864 (Putnam)
Red g:64 (Putnam)
Length Parks
Lungsh Mutric Ineerttenee Hente
Reduction (+)
80
Proof Longth
60
Proof Length
1200
Reduction
2.00
40
30
1.20
902
15
Hearthoots Matic
heartinuss Marn
Figure 17: Optimizing for length vs. heartheats
We analyze two examples of proof speedup and slowdown. In Listing 18, we observe that the original proof uses an extraneous amount of tacties within illinnritt th in order prove the main conjecture. By removing majority of these, the simplified proof achieves 4.7x speedup. In Listing 19, we observe a more extreme case, where original proof is significantly overcomplicated and can be reduced omega invocation. Goedel - 1ell--rrvveee Prover-ve - never found this single-tacts tagleetactic proof (with 64 samples) and instead produces proofs with many unnecessary subgoals, leading to a proof with slow execution time.
In several occurrences, we observe that simplified proofs can be significantly slower than the original proof. This is usually because the simplified proof is notationally shorter, but slower approach to complete the proof. For example, in Listing 20, ProofOptimizer finds shorter proof, but the proof reliant simp_all Finset. www.aaag.........mm....... succ,, and 1ina dinarith, which expand the goal into large proof terms that are time-consuming, causing the new proof to be over 10x slower. Another example shown in Listing 21. Here, the original proof first iterates over all m < 71 with interval cases tries to simplify using omega, and then iterates over all n S 71 with interval 1. cases n. ProofOptimizer, however, removes the try omega, directly doing an exhaustive search over (m, n). The try omega statement in the original proof made it much faster, removing 69 of the 71 goals, whereas the simplified proof had iterate through n for these goals.
36

---

Published as a conference paper at ICLR 2026
Uheozem imo 19
Original Proof, Time: 5,578
(a R)
(bo : < A
< A.B.A. 0
(bg : c
(ha a
S and
(a bj b" 10 0) 002
have hLmain 0 2 (a bl 222 Ce tb of 6 x l6 a) :- by alinarith [sg_nonneg m=l mei__nenngg 1o.1.le 2g.2.1.1e, nonnag ho.2.1.1a 2o.2.2.1s, mai_nenneg hg 2.121e
b), sg_nenneg (b cl, agnnonneg (c
1g.1.le,
mel_nenneg lag_nonnag (a E)1 2o.2.2.1s, mul nonneg (og nonneg (b e) 1. a) 28.2.1.18, pos ho.1 ho.2.1, mul_poo ho. hg
mil mni_nonneg toe_nonnag
4 .2.2,
pei_pes 2..2.2 ho.l, pul (sub mpp hil pcs. b2), m=l_pes (aub_pos.mp) ha) poub_pos.mpr hgh, pol_ pos._po hy) (sub pos.mpp
+ 11,
ae_nonneg
ele ag_nonneg
al, ag_nonneg
exact h_main
theorem imo 1983__69_ppp Simplified Proof, Times 1.20s
(a c : R) (ho
(h1 0 a (<bba<e)))
(bg
(ha <.b
2"2 b by b"2 (o o) o72 (c -) by
mlinarith [mul_pos (sub_pos.mpo hil lsub_pos. hz), mul_pos (sub_pos.ag mpp hz)
4 aub_pos. ha), pol_ (sub_pos.mpt hy) (sub_pos.mpr br sg_nonneg (a b), sq_nonnog
aq_nonneg s)]
Listing 18: Example of Speedup after Simplification (orig: 5.6s, new: 1.2s)
theorem mathd aathhd_nmberrthoryy.Te original Proof, Vime: 2. 50s
(x 2))
(ho
(h: (24 + x) 1195 - 15)
:= by
have h_main x S -449 1= by
by_contre! h
aave -448
by linarith
have x < 0 :- he
have (24
1159
have äs : x -448 :- by linarith have
by
omaga
we will check all possible values of x from -448 to -1 and show that none satiafy have ar False :- by
1199 15
between and check each possible value have hs x 2 -448 :- by linarich
fact
hg : Use Intervai_cae
by omaga
check each possible value of
atterval_cases x <3> norm_nnm [Int.mm _ma__mmdd, Int int_add_emod) at he <1> omega exact h_nain
theorem mathd hatiha_nnnneethoy__e... simplified Proof, rime: 0.50a
(x
(ho <
(hs : (24 + x) 1199 15) onega
by
Listing 19: Example of Speedup after Simplification (orig: 2.5s, new: 0.5s)
37

---

Published as a conference paper at ICLR 2026
Lheorem aine [ene__184__p Original ProoI, Timez 0, 91s
(u N Q1
(h1 1 Dr u ia 11 u
tho
1)
rinset.range 98, E k rinset. 49, (2 k.suec) = 93 im by by
1371
bg 6.. 14 lines oritzed)
have
4851 137
aave hg Σ in range 98, (k. 137 1= b1
5. in Finset, range 98, (k. 57 Finset. range 98, + suce Q1) == by
apply Pinset -um__ongT
intro
Iw [h2 (x.
simp cast_cast_ddd, castcosstoone
<;> ring_nf
<2> norm_num
nw [hs] at 24
have
in Pinset. 98, 1u (k.succ (11 98 4851 by
have by
in Pinset.cange 98, (u (k.suce Q11 - E x in Finset.cange 98,
4 (u 0 Q)
in range 38, (k.succ Q) by [Finset. sum_add__distrts rw [hr] his simp (pinset.summ_omm Finset.ca cartttrarrd_rggage <p> ring_nt [ba]
rinset.cange 98,
have ha in "inset.range 98, suee : Q) 4651 1 by
[Finset. auw__ange___aaeee auoe, rinset. wwrneetsuu_rangeeeeoo ran_r_nng__scc, Pinget. sum_rango__uup
<,>
[hg]
<2> ring_nf
[be] ha
norm num at h4
linrrihh
E é Finset.range
k.suce)
by
f... 25 lines emitced)
have ho : A
2237 :- by
f... lines omitted)
have bg : Σ k rinsat.range 49, u (2 k.suce) = 93 := by
iines onftted!
linarith exact b6
theorem sine eime__9800 1984__191pp1--- -- Simplified Proof, Tine: 16.84s
N - Q1
+ 1) Finset.zang 98, E k E Finset. 49, (2 k.suec) 93 : by
(ho : V. n, u
137] :
simp_all [rinset. wtw.ettte_eaaaeeeceee limorich
Listing 20: Example of Slowdown after Simplification (orig: 0.9s, new: 10.8s)
38

---

Published as a conference paper at ICLR 2026
Lheorem netine_iummbe/ Original Prout, 4,878
N0
(ho m A
Not.god
(b2 Nat.lcm n 112)
by
have h_product
896 by
f... lines omitted)
have humain 72 m 1= ho.1
anve hg
have äs
896 p_roouuct 8 h1
have "g Nat.ged
have Nat.lcm
112
have as :
2 72 by
by_contra!
6... lines omicted)
h11
nlinarith
have hi2
71 by nlinarith
interval cases m. <p> norm_num at hs </>
(Lzy omega) (try
interval_coses
(... 7ines caftted)
1) 4p>
f... lines ond otitted)
exact he exact h_nain
thearem mathd_numben authd__umborthoor__111 711 Simplified Proof, 74. 635
(n Ni
(ho
(h: Nat.god
(h2 Nat.lem n. 112) :
12
have m -mn 696 := by Mat.goo_mmilloe simp_all
by_eentra!
have m S 71 :- by alinarith
have a I :- by alinarith
interval_centt
interval_cases simp_al1
Listing 21: Example of Slowdown after Simplification (orig: 4.9s, new: 74.6s)
39

---

Published as a conference paper at ICLR 2026
J DERIVATION OF CLOSED FORM FOR MIN @ K AND M
In this section, we derive the closed form expression we use for estimating max @K from n samples based off the classic pass @K metrie:
max @ l:
Fi-
Let X real random variable, .,..., X5 independent realizations of and ((k) maxigı X; their maximum. We would like give an estimator for [=)) given n 2 independent samples I1 I S Fn of X sorted by size.
Consider the estimator M
( Eisn (
d4, with the idea being that there exist (x) ways to
choose & out the n samples overall, out of which ((-1) select the i-th and then k: 1 with a smaller index.
We compute
i
Exi
F2
=
Ex.
mmax
(K)
k
(k)
isn
IC(L.... ///////
Bay; (Fmax
Ex; max Tj jEl
IC(1....)..11
[(m)]
IC( IC01,.,,),11E=
E [X())
by the counting argument explained above, linearity of expectation, ordering of the x; and indepen- dence.
Note that this is a generalization of the @ @k metric, which covers the case of Bernoulli distributed X (Chen et al., 2021).
We recommend using a numerically stable implementation that computes the ratio by canceling
(A: 1)! factor and pairing up numerator and denominator factors. Moreover, the min@k estimator can be obtained as min min@k(zi....,. = max @ @k(--I..... -.,).
40

---

Published as a conference paper at ICLR 2026
K HYPERPARAMETERS
In this section, we detail the hyperparameters we use throughout our various training and inference experiments. Prompts can be found in the next section, Appendix L.
Iterative Training (Sec. 3.1.1): For each round of SFT, we use an effective batch size of 64 (2 nodes, 8 H100/node, gradient accumulation steps) and learning rate le-5. We cosine scheduler with minimum learning rate 1e-8 and 100 steps of warm-up up starting from le-30. For inference, we use 1.0 and top-p 0.95.
Reinforcement learning (Sec 3.1.2): Our setup is asynchronous online reinforcement learning with 16 trainer and 16 worker GPUs, and 16 environment copies per worker GPU. We use global training batch size of 32 (local batch size 2 per trainer), a constant learning rate of 6e-8 following linear warmup over 200 steps, a GRPO group size 8, mean normalization but no variance normalziation, no KL penalty and model updates sent to workers every 100 steps. Workers use For inference, we use r 1.0 and top-p 1.0, and evaluations use T 1.0 and top-p 0.95.
For test-time reinforcement learning we use the same settings but halve the number of trainers and workers.
Execution Feedback and Goedel-Prover for Repair (Sec. 4.2): We use temperature 0.2 and top-p 0.95 with a maximum prompt length 8192 and a maximum generation length of 32768.
Iterative Shortening (Sec. 4.3): For iterations 1 through 6, we use temperature = 1.0 and top-p 0.95. We increase the temperature to 1.2 for iteration 7, and to T 1.5 for iteration 8. We find that the higher temperatures in later iterations are helpful for increasing diversity with 1024 samples.
Lean Base Model (Sec. B.1): We use an effective batch size of 512 (2 nodes, 8 H100/node, 32 gradient accumulation steps) and learning rate le-5 with 100 steps of warm-up starting from 1e-30. We train with a maximum sequence length of 8192 for 2000 steps.
effective batch size of 64 (2 nodes, 8 H1000/ode, 4 gradient accumulation steps) and learning rate le-5 with 100 steps of warm-up starting from 1e-30. We train with maximum sequence length of 8192 for 50 steps. Evaluation is done with temperature 0.8 and top-p 0.95.
Proof Sketching (Sec. B.2): We
Comparison with Leading Models (Sec. E): For our model and Qwen2.5-32B, we use 1.0 and top-p 0.95. For GPT-4o and Gemini-2.5-Pii we use the default settings with r = 1.0.
41

---

Published as a conference paper at ICLR 2026
L PROMPTS
L.1 PROOF SIMPLIFICATION PROMPT
You are given correct Lean proof of mathematical theorem. Your goal is to simplify and clean up the proof, making it shorter and more readable while ensuring it atf
original procf:
"lleand [statement]
Now, provide your simplified proot. NOT nodify the theorem header, surround your + procf in ">leand and tags.
Listing 22: Zero-shot Proof Sketching Prompt
L.2 PROOF SKETCHING PROMPTS
Your task
trans natural language math solution Into Tean proof sketch that 4 follows the structure of the natural language solution. Pollow these guidelines:
1. Analyze the natural language solution and identify the key steps.
2. Translate each key step into
syntax, structuring your preof using 'have' statements + for clarity. Include all core steps from the natural language solution.
'serry' to seplace individual proefs lower-level steps, ensuring your proof
+ skeleton would compile auecassfully in Lean 4.
Surround your Tean proot sketch in "*aeean and tags.
Prcblem:
(problem)
soluttoon
(sclution)
Lean 4 Statement:
(statement]
...
Now, provide your Lean proof sketch, Do NoT modify the Uheoren oz header, and surround your 4 procf sketch >eeenn and ** zegs.
Listing 23: Zero-shot Proof Sketching Prompt
Your task la to translate a natural language math solution into a bean 4 proof sketch that follows structure
natural language solution. Pollow these guideliness 1. Anslyze the natural language solution and identify the key steps. Translate each key step into
syntax, structuring your preof using 'have' + for clarity. Include all core staps from the natural language solution,
3. "sorry" to replace individual proofs lower-level stepa, enauring that your proof + skeleton would compile succeaslully in Lean
4. Surround your Tean 4 proof sketch in ean4 and tags.
Here is exemple:
Problem:
Prove that 1f Pr a are iniess such that q divisible by P. then p must equal to q.
Solution:
Siace q prime, only divisore: and Stself, Thecefore, p divides q, either 4 Sp=18 oz Spea8. Because $pp is prime, 8p Ane 18, so Sp-q8.
Tean 4 Statement:
*>leand
import Mathlib
prime wwwpddieeiiiieeeeeeeeeeeeeeeeeee (p q N) (bp the Prine q) + == by sorey
Lean 1 Proof Sketch: v'leand
import Mathlib
thcoren sisto_ddvidde__prineee (p (hp Prime (hg Prime q) (b @
by
42

---

Published as a conference paper at ICLR 2026
q prime, it only have lermal V by sorry
isself.
Lenma Since P is prime, o 1. have lemma2 sorry
by
Vow, do case ana lysis on lemmal to luddlude cases lemnal with inl k_left m> controdiction inr huright exact r_right
Now, is your burn to provide your Lean 1 proof sketch for new problem, Do NOT modify the thecrem header, and surround your procf sketch in MMleand and 1 tegs.
Problem:
(problem)
Solut lons
(sclution)
Lean 4 stattment:: ">leand (statement)
*..
Lean Proof Sketch
Listing 24: One-shot Proof Sketching Prompt
L.3 GOEDEL-PROVE REPAIR PROMPT
In Listing 25, use modified version of Goedel-Proved repair prompt found in their codehase. The main difference is that because do not have proofs annotated with CoT's, lean.proof only contains proof.
Completo the following Lean 4 code:
"lennd
Before producing the Leen code formally
given theorem, provide detailed proof + plan outlining the main proof steps and strategies.
The plan should highlight ideas, intermadiate lemmas, and proaf struccures that will guide 4 the construction of the rinal formal proof.
sere is the proof:
v1alean4
[lean_proot)
proof (Round 1a correct. lowing is compl lntioon measage, where 4 ercor></erro:> to signal the posilion of the ecroz.
(arror htw.:/esssgg_ffr_ooeeeeeeo
Before producing the Lean code formally the given theoren, provide detailed b ana analysis of the error massage.
Listing 25: Goedel-Prover Repair Prompt
43

---

Published as a conference paper at ICLR 2026
M PYTHON CODE FOR PROOF LENGTH
import re
from collections import Counter
def proof_lengte Lectattment__nd_prcae
lean_operators [':-', !!-' '66', (-.', (-st (t ".. '..., + 4':0', '2>',
'<p', 'ii', '=', '1, (axi, 'se,, (>= 1-1,
4 4
lean operators spaceed |' jein for conn in 1ean _ operators lean_operators_diatt dict (zip [eapppoespppprttossssseeeedd
lean_operators))
def lexer (lean_snippett;
tckenized_line lines = []
for line in innn_smipeet.sllt..insss
splitlines ():
tckens =
token
for ch in line:
if ch == == ';
if token:
cokens.append (token))
token
elif str.isalnum (ch) or (ch in ")
token += ch
else:
if token:
tokens. (toked token
tokens appped (ch)
if token:
append (tcken)
tokenized_line
(tokens)
for conn in bean_operaters.. spppcce
if conn in pieenizee__ieer tokenized 4 aaan_opprattrss_dcccccmmm Lokenized_lines.cee return Ann join (tokeni (tokenized_lines,
tokenized Line. replace (conn,
(tokenized_ling
def remove remove_statenee statementtetttttttm (statement_and proof) prooo)
if ":= by" in lectement__ndd_rreeee return statement__nd__rooff split (":= by",
maxsplit=1) (1].strip()
return statement__nd_prroc ottp:aaeaaanrroo.sslll..t.tt split (":"", maxsplit=1) [1] ()
def (le__coommeetteeeennenenneen
$ multi-ling comments
lean Jeap_snippet su.sub (r" */- */-.x-/", Lean snippet,
Elags:re.DOTALL)
# single-line comments
lean_snippet - re. re.sub (r" *--,*", "", lean_snippet)
return lean_snippet
try:
precf = remove_statenes (statement_and__age prooff
proef @emove__ommente (prcef)
proof_tokenized = lexer (prcef)
return sum [len (1. split ()) for
4 proof_tokenizest stt.iiiinneeeeeeeeeeeeeeee ().)
except:
return 10x*9
44


Reviews:
[{"review_id": "GzTamsSbE7", "reviewer": "Reviewer_524q", "summary": "The goal of this work is to shorten LLM generated proofs, which can be long and difficult to understand. This work trains a new LM to shorten a given proof, using reinforcement learning. The reward signal is a mixture of the Lean correctness reward and the length of the new proof output by the model.\n\nFirst, this work introduces a Lean linter, which removes some obviously inefficient portions of proofs. Afterwards, to train an LM to shorten proofs, they use expert iteration, or RL. The initial model is Qwen-2.5-7B-Instruct, which is then further trained on mathematical/formal theorem proving-related tasks before expert iteration/RL. The training dataset is constructed using some problems from Goedel-Pset. The problems’ natural language solution is turned into a proof sketch. Then, each step in the proof sketch is used as a theorem (and the solution is given by Goedel-Prover-V2-32B), resulting in 145K theorem-proof pairs.\n\nLet M be the proof-shortening model. Within each round of expert iteration, for each theorem-proof pair, several shorter versions of the proof are sampled from M, and the shortest correct proof is included in the SFT dataset within this round of expert iteration. The length of this proof should be less than 80% the length of the original proof, so that the model will learn some non-trivial simplifications. In reinforcement learning, the reward is the relative shortening (e.g. 0.1 if the proof is 10% shorter) if the proof is correct and 0 otherwise. The algorithm is GRPO, with no advantage normalization.\n\nAfter performing 3 rounds of expert iteration (obtaining ProofOptimizer-ExpIt), the proof length with 1 generation, and minimum proof length among 32 generations, both improve significantly. However, when performing RL starting from 2 rounds of expert iteration, min@1 improves compared to ProofOptimizer-ExpIt, but the min@32 is worse. Their proof shortening models (both with expert iteration and RL) significantly outperform Gemini-2.5-Pro.\n\nAdditionally, this work finds that iteratively shortening the proof using repeated applications of their model - in each round, they generate several proofs and take the shortest one. There is a 57.2% proof length reduction on Putnam Bench, though some of the longer proofs are more difficult to simplify. There is a significant improvement from using more samples per iteration. Using a large sampling budget, there is around 40-50% length reduction on Seed Prover’s IMO proofs, using iterative applications of the proof-shortening model trained with expert iteration.\n\nThis work also finds that training on simplified proofs can help obtain better theorem proving models - when training their base model on proofs generated by Goedel-Prover-V2, they find that applying the proof-shortening model to these proofs before SFT can improve pass@32 on miniF2F. An additional benefit is that these proofs can execute/be verified more quickly.", "questions": "1. Line 158 - is there a typo in the definition of relative shortening, i.e. should be (|x| - |y|)/|x| instead?\n2. Why do you believe that min@32 is not significantly different from min@1 with RL? Is this due to an entropy collapse?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. Results with expert iteration are strong, as well as with iterative shortening of proofs using the expert iteration model.", "weaknesses": "1. The @1 metrics with RL are strong, but the @32 metrics with RL are not much better than the @1. So this may be a disadvantage since the @32 metrics also tend to be important (since it is possible to use parallel sampling together with the Lean verifier).", "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": "PXuZBhAC7u", "reviewer": "Reviewer_vYF8", "summary": "This work introduces ProofOptimizer, a 7B LLM for Lean proof shortening trained from Qwen2.5-7B-Instruct through the following stages:\n(1) Fine-tuning on five Lean-related tasks \n(2) Expert Iteration (with a 0.8len(x) threshold as the filter) on the Proof Simplification dataset built by collecting and extracting theorems from Goedel-Pset and generating proofs with Goedel-Prover-V2-32B \n(3) RL using a variant of GRPO with a reward $R(x, y) = max (|y|/|x| - 1, 0)$ for shorter proof $y$ given the prompt proof $x$.  \n\nWhen further Integrated with several inference-time techniques, ProofOptimizer manages to significantly reduce the length of the proofs generated by Goedel-Prover-V2-32B by 72.5% and 23.8% on miniF2F and PutnamBench, respectively. Besides, the ProofOptimizer can be used to optimize the training data for fine-tuning a theorem prover to achieve 2% performance gain.", "questions": "1. What do you think is the \"best\" proof for a theorem in the formal system? In my opinion, since a single tactic can comprise complex constructions of proofs (such as brute force tactics mentioned in section 5.2) and can thus be time-costing, it seems to me that shorter execution time is a better metric for evaluating a proof than the proof length. Can you share your understanding on this topic?\n\n2. For non-thinking models, we can directly shorten the proofs in the training data and fine-tune the model on the shortened data, as section 5.1 does. What shall we do when it comes to thinking models that only output the proof at the end of the response?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 4, "presentation": 4, "contribution": 2, "strengths": "- The proof shortening performance of ProofOptimizer is impressive. Seed-Prover’s IMO 2025 proofs are shortened by 50%, which makes the proof much easier for human to go through.\n\n- The task and all the techniques used in the pipeline are clearly stated, and the results are presented in the easiest way for the readers to acquire and understand.\n\n- The performance evaluation and ablation studies are comprehensive. Almost all the questions I came up during reading are answered in the paper.", "weaknesses": "1. The overall conceptual novelty of this work is limited. The task of shortening Lean proof can be seen as a code simplification task on the functional programming language Lean. The main contribution is on engineering implementation. \n\n2. The significance of pursuing the \"shortest proof\" is not entirely clear. In the introduction, the authors claim that \"RL-trained provers often generate proofs that are correct but excessively long and inscrutable\", where I do not agreee with the last \"inscrutable\" description. Both Kimina-Prover and DeepSeek-Prover-V2 follow a declarative proof style, so do the subsequent Goedel-Prover-V2 and Seed-Prover. Compared to the inscrutable imperative(or procedural) style proofs such as the IMO-2024 solutions made by AlphaProver, declarative style proofs explicitly claim every intermediate goal in the proof, which are understandable for people who are familiar with the basic grammars of the formal language. According to Figure 11, a large part of the red@k improvement of ProofOptimizer comes from using a single tactic to substitute the whole proof, which could adversely reduce the readability of the proof.\nIn my opinion, the ideal proof rewriter should do more than shortening the proof. It should not only remove all reduntant tactics, but also make sure the proof granularity is not more coarse-grained than typical natural langauge proofs by human. In other words, advanced tactics that omit necessary details should not be used in the rewrite.", "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": "39puQcY7EW", "reviewer": "Reviewer_gPDN", "summary": "This paper introduces ProofOptimizer, the first LLM designed to simplify formal proofs in the Lean theorem-proving system without relying on human-annotated simplification data. Addressing a critical bottleneck in neural theorem proving, where state-of-the-art (SoTA) reinforcement learning (RL)-trained provers (e.g., Seed-Prover, Goedel-Prover-V2) generate correct but excessively long, inscrutable proofs. ProofOptimizer integrates three core components: a symbolic Lean linter to remove redundant steps, a 7B-parameter LM fine-tuned for simplification, and an iterative inference-time workflow for progressive shortening. Trained via expert iteration (STaR-like iterative refinement using verified simplifications as training data) and online RL (rewarded for proof length reduction while preserving correctness), ProofOptimizer achieves promising results on miniF2F and PutnamBench with shortened proofs.", "questions": "See weaknesses.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- **Address an important issue**: The paper targets proof simplification, which is an under-addressed problem in neural theorem proving. Unlike prior work (e.g., ImProver) that relies on agentic scaffolding around off-the-shelf LLMs and fails on long RL-generated proofs, ProofOptimizer is the first LLM trained specifically for simplification.\n- **No Human Demonstrations**: By leveraging Lean’s mechanical verification to generate training signals (via expert iteration) and RL rewards (based on length and correctness), the model avoids the scarcity of human-annotated proof-simplification pairs, making its approach scalable and practical.\n- **Strong Empirical Performance**: The results are compelling and well-validated across benchmarks.\n- **Multiple Practical Benefits**: The paper goes beyond length reduction to demonstrate downstream value: simplified proofs speed up Lean execution and improve supervised fine-tuning of base provers.", "weaknesses": "- **Diversity Collapse in RL**: The paper acknowledges that RL training (ProofOptimizer-RL) improves single-sample performance (@1) but reduces multi-sample diversity (@32), limiting the model’s ability to explore alternative simplifications. This tradeoff is not fully resolved, and no mitigation strategies are proposed.\n- **Computational Cost**: The iterative shortening workflow and RL training are computationally expensive: the authors note ~3000 H100 GPU hours per IMO problem. This high cost may limit adoption, especially for smaller research teams, and the paper does not discuss efficiency optimizations.\n- **Dependence on Lean**: ProofOptimizer is designed exclusively for Lean, with no discussion of adaptability to other formal systems (e.g., Isabelle, Coq).", "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": "CZcpftakNn", "reviewer": "Reviewer_As7x", "summary": "ProofOptimizer is a system that optimizes the length of long Lean proofs, such as those produced by SOTA prover models. ProofOptimizer is the first work to use reinforcement learning to tackle this problem setting, and they show by comprehensive experiments that they improve upon existing baseline, reaching substantial proof reduction.", "questions": "While proofs produced by Seed-Prover are very redundant and, to a human, look easy to simplify, I am very curious whether the ProofOptimizer pipeline can also be applied to human-written proofs like those in Mathlib, or helping verbose, model-written proofs (like those written by Aristotle) be merged into Mathlib, which is a key factor limiting such models. Relatedly, I am curious whether the model could do better by training on data outside Goedel-Pset or proofs written by Goedel-Prover-V2, such as human-written proofs or diffs in Mathlib commits. I recognize this may be a big ask and I don’t expect a complete answer in the author rebuttal stage.\n\nReduction @64x2 seems much better than @128 in Figure 3. Is there any further analysis on the tradeoff between iteration count and k? Relatedly, why the specific schedule of 6 iterations of k = 64 and 2 iterations with k = 1024?\n\nI am interested in how the Lean-specific tokenizer works specifically, because it seems central to interpreting the numbers like min@k and for reproducibility. Or if the code is not long, is there code for the tokenizer? (You can probably put this as a small explanation in the Appendix).", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "ProofOptimizer is the first work to use RL to shorten formal proofs. The experiments in Section 4 conclusively show the advantage of this method over existing baselines such as Gemini-2.5-Pro on a pipeline like that of ImProver.\n\nI am convinced by the analysis in Section 5 that optimized proofs are easier to learn for a model, and faster to compile. The former is important in improving the data quality in existing SFT datasets for Lean, and the latter is important considering the multi-day runs that AlphaProof, Seed-Prover, and Aristotle required for IMO problems. These establish the importance of the problem setting, which has not been analyzed in prior work.", "weaknesses": "The training distribution seems limited to high-school competition problems, which seems to limit the usability of ProofOptimizer for integrating long proofs of other types of results into libraries like Mathlib, as authors mention on L43–44.", "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)