STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Authors: Kefan Dong
Tengyu Ma
Venue: ICML 2025 poster (2025)
Keywords: formal theorem proving
AI for math
self-play
large language model
reasoning
reinforcement learning
Primary area: deep_learning->large_language_models
TL;DR: We design a self-play algorithm for theorem proving that iteratively conjectures new statements and proves them, achieving state-of-the-art performance on miniF2F and ProofNet among whole-proof generation methods.

Abstract: A fundamental challenge in formal theorem proving by LLMs is the lack of high-quality training data. Although reinforcement learning or expert iteration partially mitigates this issue by alternating between LLM generating  proofs and finetuning them on correctly generated ones, performance quickly plateaus due to the scarcity of correct proofs (sparse rewards). To keep improving the models with limited data, we draw inspiration from mathematicians, who continuously develop new results, partly by proposing novel conjectures or exercises (which are often variants of known results) and attempting to solve them. We design the Self-play Theorem Prover (STP) that simultaneously takes on two roles, conjecturer and prover, each providing training signals to the other. The conjecturer is trained iteratively on previously generated conjectures that are barely provable by the current prover, which incentivizes it to generate increasingly challenging conjectures over time. The prover attempts to prove the conjectures with standard expert iteration. 
We evaluate STP with both Lean and Isabelle formal versifiers. With 51.3 billion tokens generated during the training in Lean, STP proves 28.5% of the statements in the LeanWorkbook dataset,  doubling the previous best result of 13.1% achieved through expert iteration.
The final model achieves state-of-the-art performance among whole-proof generation methods on miniF2F-test (65.0\%), ProofNet-test (23.9\%) and PutnamBench (8/644) with pass@3200.

STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Kefan Dong' Tengyu Ma
Abstract
et al., 2023; Nijkamp et al., 2022). It also key criterion for achieving artificial general intelligence (AGI). Auto- mated theorem proving with formal languages by LLMs stands at the forefront of reasoning research (Yang et al., 2024a), partly because it allows objective and reliable eval- uation through classical verifiers such as Lean (Moura Ullrich, 2021) and Isabelle (Nipkow et al., 2002). Moreover, it arguably encapsulates the essence of advanced reasoning tasks while abstracting away the ambiguity of natural lan- guage, enabling meaningful studies on relatively smaller scale.
A fundamental challenge in formal theorem prov- ing by LLMs is the lack of high-quality training data. Although reinforcement learning or expert it- eration partially mitigates this issue by alternating between LLM generating proofs and finetuning them on correctly generated ones, performance quickly plateaus due to the scarcity of correct proofs (sparse rewards). To keep improving the models with limited data, we draw inspiration from mathematicians, who continuously develop new results, partly by proposing novel conjectures or exercises (which are often variants of known results) and attempting to solve them. We de- sign the Self-play Theorem Prover (STP) that si- multaneously takes on two roles, conjecturer and prover, each providing training signals to the other. The conjecturer is trained iteratively on previously generated conjectures that are barely provable by the current prover, which incentivizes it to gener- ate increasingly challenging conjectures over time. The prover attempts to prove the conjectures with standard expert iteration. We evaluate STP with both Lean and Isabelle formal versifiers. With 51.3 billion tokens generated during the training in Lean, STP proves 28.5% of the statements in the Lean Workbook dataset, doubling the previous best result of 13.1% 3.1% achieved through expert itera- tion. The final model achieves state-of ohe-the-art per- formance among whole- prool- generation methods miniF2F-test (65.0%), ProofNet-test (23.9%) and PutnamBench (8/644) with pass @ 3200.
However, a fundamental challenge in improving reasoning ciformanceewhettie in natural or formal languages in the lack of high-quality training data. Collecting reason- ing data requires domain experts, making it expensive to scale. There are only limited number of advanced math pa- pers and theorems in existence, orders of magnitude smaller than other data sources.
Reinforcement learning (RL) on datasets without solutions (e.g., datasets with theorem statements or reasoning ques- tions and answers) is a prominent approach for improving the reasoning capability, as seen in the recent development of OpenAI ol (Jaech et al., 2024), DeepSeek- Prover (Xin et al., 2024a) and DeepSeek R1 (Guo et al., 2025). Often referred to as expert iteration (Anthony et al., 2017), it par- tially mitigates the data scarcity issue by alternating between LLMs generating proofs and finetuning them on correctly generated ones (Kaliszyk et al., 2018; Wu al., 2021; Al- phaProof, 2024; Xin et al., 2024b; Ying et al., 2024).
However, as Wu et al. (2024) pointed out, RL or expert itera- tion often saturates at low pass rate because the number of samples required to generate a correct proof for an unproven theorem grows exponentially. As a result, a massive amount of computation is wasted on generating incorrect proofs that provide no training signal the model. For instance, the proof sampling process of Wu et al. (2024), 98.5% of the compute yields no successful proof's, despite the pass rate being only 13. 13.1% % on the training dataset, Lean Workbook (Ying et al., 2024). In other words, after few rounds of expert iteration, re-training the model becomes less effective due to the limited number of new successful proofs.
1. Introduction
The reasoning capability of large language models (LLMs) is critical for various applications, including coding assis- tants, question-answering and agents (Plaat et al., 2024;
Shinn et al., 2023; Yao et al., 2022; Shao et al., 2024; Li
Stanford University: Correspondence to: Kefan Dong <kefan- dong@cs es eduz, Tengyu Ma <tengyuma@ stanford.edux.
Proceedings of the 42nd International Conference Machine Learning. Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).
In addition, RL's capability is fundamentally bounded by the difficulty level of the theorems in the training dataset it

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Step Conjecturing
Step 2: Proving (sampling) Given statement or conjecture, generate its proof
Given seed statement and proof,
generate a related conjecture.
statement
proof
conjecture
stmt stmt//ooj.
proof
Step 5: LLM training
Existing dataset w/o proofs:
statement
babett
LEWN RACKER
Step 4: Preparing training data (assigning reward)
Step 3: Verifying proof'
Conjecturer dataset
Prover dataset
proof
conjecture
/conj.
proof
Conjectures from Step that (4) are proved with low but non-zero probability, and (b) pass the elegancy filters.
Proofs from Step that are verified, nontrivial, and de-duplicated.
Figure I: Self-play Theorem Prover (STP). Our model simultancously takes on two roles the conjecturer that generates new, related conjecture given seed theorem with proof (Step 1), and the prover that attempts to prove the statements in an existing dataset and the generated conjectures (Step 2). Step 4 selects the correct, approachable, elegant, yet challenging conjectures to train the conjecturer, and the verifier selects correct proofs in Step 3 to train the prover. The main difference between STP and expert iteration is the conjecturer role highlighted with yellow background.
is unlikely, in principle, for a model to learn college-level proof techniques solely by working on high school-level problems or to solve open math problems using RL on graduate-level problems. Moreover, there are likely not enough open problem statements available for RL train- ing to generalize to other open problems, particularly more advanced ones. In other words, RL or expert iteration al- gorithms cannot train indefinitely without continuously col- lecting more theorem statements or math problems.
1), while the prover attempts to prove conjectures and state- ments from an existing dataset (Step 2). Then, the verifier selects correct proofs (Step 3) to train the prover using stan- dard RL and identifies correct, approachable, elegant, yet challenging conjectures to supervise the training of the con- jecturer (Step 4). More concretely, in each iteration, the conjecturer is trained on previously generated conjectures that: (a) are barely provable by the current prover (i.e., the prover's success probability with respect to its random seed is positive but low), and (b) pass certain elegancy filters. This iterative process gradually increases the difficulty of conjectures and proofs without requiring additional data. Our method can be viewed either as a self-play algorithm between conjectures and provers or as automated curricu- lum learning (Portelas et al., 2020) with a self-generated adaptive curriculum (via conjecturers).
We need an algorithm that can run and self-improve indefi- nitely without more data. To this end, we draw inspiration from how mathematicians learn and develop advanced math- ematics; they refine their understanding and sharpen their proof skills by working on synthesized exercises-variants extensions, or combinations of existing theorems. Addi- tionally, they frequently propose and publish conjectures, process widely regarded as just as important, if not more so, than solving them. In other words, unlike the current training of LLMs, mathematicians engage with far more exercises and conjectures (referred to collectively as con- jectures in this paper) than the polished, published results found in academic papers and books. Moreover, the con- tinuous generation of new conjectures keeps mathematical fields dynamic and moving forward.
We empirically evaluate our method with both Lean (Moura & Ullrich, 2021) and Isabelle (Nipkow et al., 2002). For the Lean experiments, aim for the best performance and therefore choose DeepSeek-Prover Prate--ovvvv-------- V1.5-SFT (Xin et al., 2024b) as the base model for STP. As shown in Fig. 2, after a self- self-play training of roughly 241M generated proofs and 6.M generated conjectures, we successfully prove 28.5 28.5% of the statements in the training dataset Lean Workbook (Ying et al., 2024), doubling the previous best result of 13. % (Wu et al., 2024) achieved by expert iteration.' In Fig. 3, we compare the inference-time performance of existing
In this paper, design Self-play Theorem Prover (STP), which mimics how mathematicians learn and develop math- ematics. It simultaneously assumes two roles ooles-conjectured and prover-providing training signals to each other.
"Based on our reproduction. Deepseek Prover- has a better performance on Lean Workbook,,, proving 13.2% statements with 32 samples per statement, although the original paper does not report this number.
As illustrated in Fig. 1, the conjecturer, given a seed theo- rem with proof, proposes a new, related conjecture (Step
2

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Training performance LeanWarkbook
miniF2F-test
Cumalottve p0xs rate
26
65
Pass Rate
60
22
55-
18
STP (Ours)
Expert iteration
STP (Ours)
Parallel sampling
50
DeepSeck-Prover-VL..55
50m
100m
150m
200m
250m
Training compute
102
10
10a
10
(#generated proofs)
Inference-ting compute (#generated proofs)
Figure 2: The cumulative pass rates of STP, expert iteration, and parallel sampling on Lean Workbook shows that STP achieves a much better scaling terms of the performance vs number of generated proof'. The compute for generating conjectures and training the conjecturer in STP is negligible because the number of generated proof' during training is 64 times the number of conjectures.
Figure 3: Comparison of pass rates on miniF2F-test (y-axis) with different numbers of inference-time samples (x-axis). The model trained with STP consistently outperforms the Deepseek-Proves Prover-vvvr series.
2. Additional Related Works
We refer the readers to Bibel (2013); Loveland (2016) and the reference therein for classical automated theorem prov- ing. Below, we discuss recent works on modern L.-M-based theorem provers in addition to what has been discussed in the intro.
models and the final model trained with STP by taking multiple independent samples on a common benchmark, miniF2F-test (Zheng et al., 2021). Our model significantly outperforms the DeepSeek-Prover-VL. models across var- ious sampling budgets. We also achieve state-of-the-art performance among whole-proof generation methods miniF2F-test (65.0%, pass 3200), ProofNet-test (23.9%, @ 3200) (Azerbayev et al., 2023a) and PutnamBench (8/644, pass @ 3200) (Tsoukalas et al., 2024), where pass @K represents the percentage of statements proved with inde- pendently sampled proofs per statement.
Autoformalization. relatively efficient way to create formal proof data is autoformalization, that is, translating natural language math statements and/or proofs formal language (Jiang et al., 2023; Lu et al., 2024). A line of research focuses on generating proofs or reasoning steps in natural language and then formalizing the proofs (Jiang et al., 2022b; Zheng et al., 2023; Wang et al., 2023). Most recently, AlphaProof (2024); Xin et al. (2024a;b) autofor- malize statements and then train with expert iteration RL write proofs, achieving significant improvement over prior works thanks to the large-scale natural language datasets.
In the Isabelle experiments, by starting from a generic math-focused model Llemma- 7b (Azerbayev et al., 2023b) and run STP for more iterations (300M generated proofs in total). We compare the scaling of STP with expert iteration and parallel sampling, by taking several model checkpoints during the STP training run and then switching to the baseline methods. The results clearly demonstrate that STP achieves better scaling behavior starting from various checkpoints with different capability (see Fig. 4 in Section 4.3). Ablation study also demonstrates that the main performance gain stems from the dense train- ing signals given by the conjectures. Expert iteration wasted its compute on generating unsuccessful proofs to challeng- ing theorems in the training dataset-at a checkpoint where the pass rate is around I 1.44% on LeanWorkbook, only 131 out of 2.5M generated proofs of the unproved statements are correct, resulting in very limited training signals. In contrast, at least 47% of the generated conjectures in STP training are successfully proved because the conjecturer is trained to generate more approachable statements thanks to the design of its reward (see Fig. 6).
study the scalability of STP
Formal conjecturing. Prior works also study how to gener- ate new formal statements/ccojeecuuess by neural networks (Urban & Jakubův, 2020; Einarsdóttir et al., 2024; Johans- son & Smallbone, 2023) or human-written generators (Polu et al., 2022; Trinh & Luong, 2024), and find that the syn- thetic statements are generally useful for training the provers (Wang & Deng, 2020; Wu et al., 2020). Synthetic state- ments and proof' can also be extracted from an incorrect proof trajectory during RL with hindsight experience replay (HER) (Andrychowicz et al., 2017) to speed up the training process (Aygün et al., 2022; Dong et al., 2024). However, even though the training efficiency is improved, we argue that the final performance is still bounded by difficulty level of the existing dataset because synthetic statements are most likely easier than the given ones in the dataset.
Self-play and automatic goal generation. The closest re-
3

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
lated work this paper is Poesia et al. (2024) which also designs a self-play training that iterates between conjectur- ing and theorem proving. The key difference between this paper and Poesia et al. (2024) is that we start with pre- trained model and work on practical formal languages like Lean and Isabelle with an infinite space of possible proof steps (Which are actions in the RL algorithm), whereas Poe- sia et al. (2024) operates in a simplified and constrained setting with finite action space and trains from scratch. As a result, Poesia et al. (2024) rely on constrained decoding to force the validity of generated conjectures, while we solely rely on the LLM itself to generate valid conjectures. Techni- cally, since our training process is much longer (more than 50 iterations) than Poesia et al. (2024) (5 iterations), we must carefully design the conjecturing reward maintain the diversity and relevance of the generated conjectures (see Section 3.2).
and its corresponding proof. We only compute the next to- ken prediction loss on the proof (which is the expected output of the model), while the rest is treated as input. To build this dataset, we simply extract all the statement-pre pairs from the proof library files and add a system prompt.
Conjecturer SFT dataset. Generally, the conjecturer is to generate a new, related conjecture, given a seed statement with proof that provide the initial ideas. Technically, to fur- ther guide the generation of conjecturer, we also provide it lemma used in the proof of the seed statement, which can be extracted from the verifier, so that the generated conjec- tures are more likely to be related to the theorem through the lemma. Therefore, the input is a concatenation of the system prompt, a lemma, and seed statement and its proof, separated by special formatting tokens, and the expected output is a conjecture on which we compute training loss, We also allow the model to generate conjectures with a fixed trivial lemma. To construct this dataset, we extract (lemma, theorem X, theorem Y) tuples from every proof library file such that (a) the lemma and two theorems appears in the file in this particular order, and (b) the lemma is used in the proof of both theorems. The lemma and theorem X will be part of the inputs, and theorem will be the output.
The idea of generating new tasks by the model is also ex- plored in other domains such as alignment (Ye et al., 2024), programming puzzles (Haluptzok et al., 2022; Teodorescu et al., 2023; Pourcel et al., 2024b), video games (Zhang et al., 2023; Pourcel al., 2024a), and classic RL environ- ments Parker-Holdeds et al., 2022; Colas al., 2022). More generally, self-play training has demonstrated its potential to achieve super-human performance on two- wwo-player games in fixed environment like Go (Silver et al., 2016).
3.2. Self-play training
Our self-play training stage of STP is shown in Fig. 1. The main difference compared to expert iteration is the conjec- turer in Steps and 4, highlighted in yellow background.
3. Method
On the high level, Self-play Theorem Prover (STP) involves three training stages: (1) model initialization by supervised finetuning, (2) self-play training (visualized in Fig. 1), and (3) final re-training. Unless otherwise stated, we use the term 'statement' to refer to the statements in given datasets, and 'conjecture' the generated conjectures.
Generating conjectures and proofs (Steps 1 & 2). The self-play training starts with collecting a list of the conjec- turer's inputs in the same format as in the conjecture SFT dataset (system prompt, lemma, and theorem), but from theorem-proof pairs where the theorems are from the given dataset without proof's and proof's are previously generated. We extract a seed lemma from the proof, using the verifier. 3 To prevent the model from only focusing on a few particu- lar proof techniques, we de-duplicate the list based on the seed statement and lemma, and randomly drop some inputs whose lemma appears excessively. Then, the LLM gener- ates conjectures from the inputs, and we randomly select a subset of the generated conjectures with size no larger than the number of remaining unproved statements in the given datasct, so that the prover's compute budget is split equally between the conjectures and statements. (See the pseudo- code and details in Appendix A.2.) For the prover's inputs, we combine the generated conjectures and the unproved statements in the existing dataset. Then, we independently sample K proofs per statemenn/coojjectuee in Step 2.
3.1. Model initialization by supervised finetuning
In this stage, we initialize the model with two roles, con- jecturer and prover, by finetuning a generic LLM (such as the Llama (Touvron et al., 2023)) on a SFT dataset con- structed from existing proof libraries such as Mathlib (math- lib Community, 2020). The proof libraries are organized into files containing human-writted formal proofs of known mathematical theorems, and each file formalizes a relatively self-contained result, such as a chapter of a textbook. Our SFT data consists of the following two parts, for finetuning the prover and conjecturer, respectively. Also see concrete examples in Appendix A.I.
Prover SFT dataset. We construct a SFT dataset to teach the model to write formal proofs in the given format, where each example is the concatenation of a system prompt (to in- struct the model to generate in formal language), statement,
'There is fundamental difference between lemmas and theo- rems in formal proofs the naming purely for better exposition. 'In our implementation, lemmas are extracted together with proof verification in Step 3 by configuring the verifiers accordingly.
4

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Reward assignments (Step 4). The major technical chal- lenge of STP is to design the reward function for the con- jecturer (in other words, construct the conjecturer dataset in Step 4). The ultimate goal is to incentivize conjecturer to generate diverse, relevant, approachable yet challenging conjectures to provide enough training signals to the prover.
the distribution P as the training for the conjecturer. Pseudo-code of this step is in Appendix A.3, and an effi- cient implementation is in Appendix A.5.
For the prover dataset, we only select correct generated proofs where the empirical pass rate of the corresponding statemen//conjccuree is below 1/2. (We consider other cor- rect proofs trivial). We de-duplicate the prover dataset by exact match. Then, the prover is trained on a replay buffer containing the selected proofs from the last three iterations.
In Step 4, we first organize all generated conjectures and proofs into a list of examples D {(t, pi: li G, pf) where f2 and Df represents seed statement and its proof, I is a lemma used in the proof p\: and c,,P Pf are the generated conjectures and the generated proof. We will filter D as described below and then use (t,, pf. 4,) as the input to the conjecturer and o as the output, and pf as the output of the prover w.r.t. the input G--
LLM training (Step 5). We use weighted eross entropy loss computed on the conjectures proofs (but not the inputs of the model). For the proof dataset, we weight the examples reciprocally to the number of verified proofs to the corresponding statement/conjecture We also use a length penalization of the form 7f to reward simpler proofs, where Y < 1 is the discount factor and the length of the proof. For the experiments with Lean, we additionally reward proofs that has faster verification time by a penaliza- tion of the form 3 where T is the execution time of the Lean verifier.*
To decide whether a conjecture is challenging, we use the (empirical) pass rate of the prover estimated by the K independently generated proofs:
P(c) è (# q = c, is c q = =c)).
Then, we select the examples in DD where (a) lemma 1, is used in the proof of conjecture pf. and (b) the pass rate of the conjecture, P(G)), is between (0, 1/4]:
3.3. Final re-training
To avoid training instability caused by the changing data distribution during self-play, we re-train the final model checkpoint from the base model (before the SFT stage) on a combination of the SFT dataset and all the correct proofs generated during the self-play training whose corresponding statement/conjetture has an empirical pass rate no larger than 1/4. For every statement/conjeeture, we randomly keep at most 16 distinct proofs to speedup the training.
D+ [(t,, 4, es) (ta, Pt, 4, 4. p() E D,
P(c.) E (/,1/4), p is correct, 4 is used in pf).
Here we discard the proofs (of the conjecture) pf since they are not needed to train the conjecturer, and we remove the duplicated conjectures (that have multiple proofs).
Then, we apply a heuristic elegancy filter to discourage the model from generating artificially hard conjectures with complicated goals we remove conjectures whose mini- mum proof length divided by the length of the conjecture is in the lowest 20% of remaining examples.
4. Experiments
This section presents our implementation details of STP, the results of Isabelle and Lean experiments, and the ablation studies, followed by examples of generated conjectures.
Finally, we re-weight the selected conjectures to preserve the diversity of the conjecturer - the reward for conjecturer cannot only depend on the generated conjectures individ- ually because otherwise the conjecturer's 's optimal policy may degenerate a singular distribution, whereas in reality, the given dataset typically has multiple modes because the statements focus on different topics like algebra, number theory, and calculus. Therefore, our idea is to push the dis- tribution of the selected conjectures toward the unproved statements the existing dataset to maintain the balance between multiple modes. To this end, we compute distribu- tion P supported on the selected conjectures that minimizes the Wasserstein distance to the uniform distribution over unproved theorems, denoted by Q. The matching cost or similarity metric between a conjecture and a statement, used for computing the Wasserstein distance between P and Q, is defined as the negative cosine similarity between their embeddings (given by the current model). Finally, we use
4.1. Implementation details
Training datasets. Our primary source of statements with- out proofs is the de-duplicated Lean Workbook (Ying et al., 2024), which contains around 89K Lean4 statements (see Appendix A.4 for details). For the Isabelle experiments, we translate the Lean4 statements to Isabelle using the DeepSeck V2.5 with few-shot prompting. For the Lean experiments, we combine Lean Workbook, miniF2F-valid, and ProofNet-valid as the training dataset for STP.
The SFT dataset for the Isabelle experiments is extracted
"In our preliminary experiments. we found that without the penalization on verification time, the Lean verifier takes 2x more wall-clock time on CPU than sampling proofs on TPU for our cluster setup, which becomes a bottleneck for STP training.
5

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
from AFP3 and Isabelle built-in files such HOL. For the Lean experiments, we first sample 32 proofs per statement in Lean beanWorbbook since our base model, DeepSeek-Provet V1.5-SFT, is already trained on it, and combine the correct proofs with examples extracted from the proof library Math- lib4 (mathlib Community, 2020) as the SFT dataset.
metrie for training progress. Fig. plots the cumulative pass rate of STP and two major baselines, expert iteration, and parallel sampling, on the training dataset LeanWork- book (Ying et al., 2024). Expert iteration alternates between generating proofs to the statements in the given dataset and finetuning the model on correct proofs. (See discussions and comparison about variants of expert iteration in Ap- pendix A.6.) Parallel sampling simply generates proofs with the given model. Fig. shows that STP achieves signif- icantly better scaling than expert iteration, which simulates the performance of DeepSeek's 's model as if it were trained for more iterations.
Periodic refreshing. With a limited replay buffer, the model may forget some proof skills learned in the SFT stage af- ter many iterations. Therefore, during our STP training, we periodically re-train the model from the base model on all previously generated correct proofs, following a pro- cedure similar to the final re-training in Section 3.3. After refreshing, we reset the replay buffer and restart the self- play training using the re-trained model checkpoint.
Since the formal statements in our training dataset, Lean- Workbook, are translated from natural language statements, they are not always provable. In Appendix B.3, we ran- domly select 20 unproved statements from Lean Workbook and manually assess whether (a) the formal statement is an accurate translation of the natural language statement, and (b) the formal statement itself is correct and provable. We find that 16 out of the 20 statements are translated correctly, but only 7 statements are provable and the remaining 13 statements are unprovable (e.g., due to missing assumptions in the corresponding natural language statement), suggest- ing that the best possible pass rate on LeanWorkbood is far below 100%.
Verifiers' setup. To study the scalability of STP with lim- ited compute, in the Isabelle experiments, we disable the advanced proof tactics s sledgehanmer, mason, smt, metis, sos, which require huge CPU compute, to allow more training iterations, sacrificing verification strength and overall performance. We use PISA (Jiang et al., 2021) to interact with Isabelle, and enforce a 10s timeout for any proof step and 360s timeout for entire proofs. For Lean, we follow Xin et al. (2024b), which allows all proof tactics, and set 200s timeout and a 15GB memory limit for each proof.
hyperpaarmeters. For inference, we cap the number of generated tokens to 1024, and set the sampling temperature to 0.7 for Llemma-7b and 1.0 for DeepSeek- Prover, fol- lowing Dong et al. (2024); Xin et al. (2024b), respectively. For training, we use batch size 2048 and Adam (Kingma & Ba, 2014) with a constant learning rate of 5c-5 in STP, and le-4 in SFT and final re- re-trnini The discount factors are = 1==xpp-00001 and / = exp(-0.01)
In Table 1, we compare the final re-trained model of STP with prior works on two common benchmarks, miniF2F-test and ProofNet-test, which contain formal statements of high- school level and college level math questions, respectively." Among the whole-proof generation methods, STP signif- icantly outperforms DeepSeek- SeepSeee-Prove--Ve V1.5-RL (which is continuously trained with RL on top of their SFT model) and achieves SoTA performance across various inference- time sample budgets. We also report the performance of the model trained only on JorkWorb for 24 iterations, excluding miniF2F-valid and proofnet-valid, demonstrating that the model trained with STP also generalizes to out-of- domain theorems.?
In each iteration of STP, we sample K = 32 proofs per conjecture/statement. For the expert iteration and parallel sampling, we use K- = 64. Since we maintain the number of generated conjectures per iteration to be at most the number of unproved statements in the given dataset, STP has the same sample budget as the baseline methods per iteration.
Table I also compares STP with tree search methods such as M.temLL.2..5-StepPPP
(Wu et al., 2024), which use LLMs to generate single proof steps conditioned on the current ver- ifier's proof state and then find a complete proof by best first search or MCTS. The sample budget of these methods are not directly comparable with whole-proot generation meth-
4.2. Results with Lean
For the Lean experiments, we choose DeepSeek-Prover: V1.5-SFT as our base model, which is trained on proofs collected by expert iteration on a combination of public, such as Lean Workbook, miniF2F-valid (Zheng et al., 2021), and ProofNet-valid (Azerbayev et al., 2023a), and propri- etary datasets. We run 48 iterations of STP and generated 3.6M conjectures, 241M proofs, and 51.3B tokens in total. We use the cumulative pass rate, defined by the fraction of statements proved during the entire training, as the main
'In our experiments, we use the miniF2F statements in ht tets: / ggt..b..ccoooooooooooo haabb.cc//yaagg htt///yangyy//aa 1atpyy11mmmmn121mmm1 commi t/8c833c4 and the ProofNet statements in https: //t.ittbbcco//cccccmm
"Our base model, httttttsettt/rrooott.eeeeeee
is trained on
m and ProofNet-valid, though we only run STP on Lean Workbook in this experiment. The penalization verification time is also not included in this experiment.
'https: htttps::/www.isee isa- afp.org/
6

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Table I: Pass rate on miniF2F (Zheng et al., 2021) and ProofNet (Azerbayev et al., 2023a) with different inference-time sample budgets. Our method, STP, achieves state-of state-of-the-an the-art performance among whole-proof generation methods across various sample budgets. For reference, we also include tree search methods, even though they are orthogonal to our main contribution. The sample budgets of tree search methods are not fully comparable that of the whole proof generation because they also use the LLM process the verifier's internal proof state.
Sample budget (#Proofs)
Sample budget (#Steps)
Method
MiniF2F-test
ProofNet-test
Whole-Proof Generation Methods
Taao (Wang et al., 2024)
128
33.6%
DSP (Jiang et al., 2022h)
100
39.3%
DeepSeck-Prover- V1,5-SFF
128
50.4% + 0.4%
15.9% + 0.6%
(Xin et al., 2024b)
3200
53.3% + 0.5%
21.0% + 0.9%
DeepSeek-Prover Parblekk-Provr-VI.5--- V1.5-RL
128
51.6% + 0.5%
18.2% - 0.5%
(Xin et al., 2024b)
3200
54.9% 0.7%
22.0% 1 0.5%
25,600
58.4% 1 0.6%
23.7%
102,400
60.2%
STP
128
1.1K
57.2% 1 0.6% 61.1%
18.0% + 0.7%
(w/o minil F-valid, ProofNet-validd)
3200
28K
23.1%
STP
128
1.3K
61.2 % + 0.6%
19.5%
+ 0.7%
3200
32K
65.0 % + 0.5%
23.9%
+ 0.6%
25,600
254K
67.6% %
26.9%
Tree Search Methods
ReProver (Yang al., 2024b)
26.5%
PACT (Zheng et al., 2021)
8 16 512 66K
29.2%
GPT-f (Polu et al., 2022)
64 x 8 x 512 = 262K
36.6%
HTPS (Lamplc et al., 2022)
64 x 5000 = 320K
41.0%
Lean-STaR (Lin et al., 2024)
64 X 1 x 50- 3.2K
46.3%
DeepSeck-Proved V1,5-RL + RMaXTS (Xin et al., 2024b)
3200
55.0% + 0.7%
21.5% + 0.8%
25,600
59.6% 1 0.6%
25.3%
204,800
63.5%
MitemLLM...-SSepPPPrrn
x 32 600 77K
58.5% + 0.9%
(Wu et al., 2024)
16 x 32 600 307K
62.5% + 0.5%
256 x 32 x 600 4.9M
65.9%
ods because (a) the number of steps in generated proof varies significantly, (b) LLMs in tree search methods need to process additional tokens related to the verifier's 's proof (Wu et al., 2024) require an additional LLM as the value fune- tion. Moreover, it's conceivable that tree search methods can also be used with STP, essentially these are orthog- compute the total number
As shown in Table 4, on PutnamBench (Tsoukalas et al., 2024) which consists of undergraduate-level mathematics competition questions, STP solves 7 out of 644 problems with 128 samples per problem, and problems with 3200 samples per problem, outperforming the best result of problems in prior works achieved by Wu al. (2024).
state, and (c) methods like SetrmLLM...-SStPPrrrc
onal methods. Nonetheless, of proof steps per statement generated by STP as an proxy for the total number of LLM output tokens for STP and tree search methods, ignoring the additional compute required by tree search methods to process the verifier's proof state and query the value function. Results in Table 1 indicate that STP also outperforms prior tree search methods with similar (estimated) inference-time budgets.
4.3. Results with Isabelle
For Isabelle experiments, we start with the Llemma- 7b (Azerbayev et al., 2023b), math-focused model, and run 58 iterations of STP study its scalability. We take several checkpoints during STP training and then switch to the expert iteration and parallel sampling baselines to study the scalability of the algorithm from checkpoints with various capability. Fig. 4 compares their cumulative pass rates on Lean Workbook (Isabelle translation), showing that STP consistently achieves a better scaling across the training
*The #Steps for search methods is typically calculated by #Independent runs x #Tactics generated per search step x #Scarch steps. or #independent runs x #Search steps.
DDeepSeek-Prover V1.5-RL+ RMaxTS is tree search method that uses the LLMs generate complete proofs during the search
instead of single proof steps. Therefore, treat their sample budget as the number of generated proofs instead of steps.

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Table 2: Comparison of STP with and without final re-
Per Performance on LeaniWorbbuck (Isabelle translation)
training on miniF2F-test and ProofNet-test.
12.0
11.5
Method
Budget
miniF22 2F
ProofNet
Currulative
11.0
STP
42.3%
7.7%
10.5
w/ re-training
3200
65.0%
23.9%
10.0
SIP
25600
67.6%
26.9%
Expert iteration
Parallet sampling
STP
43.2%
8.8%
9.0
w/o re-training
3200
65.1 %
22.0%
50m
100m
150m
200m
250m
300m
Tr Training compute
25600
66.0%
23.7%
(#generated proafs)
Figure 4: Cumulative pass rate on LeanWorkbook (trans- lated into Isabelle) of STP, expert iteration, and parallel sampling, started from two checkpoints in STP training. STP achieves better scaling starting from both checkpoints. For better visualization, the x-axis starts with 50m here and we defer the full plot to Fig. in the appendix.
process. The model also gradually improves on miniF2F over the training process, as shown Fig. 5.
4.4. Ablation study
Generated conjectures provide denser training signals. Fig. shows the histogram of empirical pass rates of the generated conjectures and the unproved statements in Lean- Workbook using a checkpoint the Isabelle experiment. Only 131 out of 2.5M generated proofs for the 79K un- proved statements model on correct proofs has almost no effect, and thus ex- pert iteration plateaus. In contrast, generated conjectures by STP offers higher pass rates and thus more training signals, leading to better scaling.
Pass@64 miniF2F
miniF2F valid
miniF2F test
46
correct. As a result, finetuning the
Pass
42
3
4
Re-training with generated conjectures still helps down- stream performance. One may hypothesis that the self- play algorithm and generated conjectures only help improve the pass rate on LeanWorkbook. It turns out that the final re-training stage, it is still beneficial to re-train with the generated conjectures in addition the successfully proved statements in GanWorkbook even for performance on miniF2F-test and ProofNet-test-it leads to about 2-3% performance gain (for pass @ 128) than re-training only on the latter (See Appendx B)
Checkpoint ID
Figure 5: The performance of our model on miniF2F grad- ually improves during the training process. Note that our model is not trained on miniF2F valid and we disallow advanced tactics such as sos. The checkpoints are taken roughly per 68M generated proofs.
lemmas in the proofs of Lean Joakbook statements. At late checkpoint of our experiments, 51.1% % of the correct proofs of generated conjectures share at least one lemma with the proof of the seed statement, which indicates that substantial portion of generated conjectures are mean- ingfully related their seed statement. In Appendix B.4, we list 30 most frequently shared lemmas. While lem- mas in the field of inequalities and algebra remain dom- inant (e.g.. sq_nenneg, Real. sii__s__adddeeeeeeeeeee_sses_sie _dd__co__s)) we also see lemmas related to sequence of products (i.e., Finset httpeerrooodddde__eeeeeee range__uucc.. and number theory (e.g.. Nat hitt.powmmo, nat_sub_dvee
Final re-training improves the pass@ @k performance. In Table 2, we compare the performance of STP with the fi- nal model checkpoint from self-play training (i.e., without final re-training) on miniF2F-test and ProofNet-test. Ta- ble 2 shows that STP with final re- te-training achieves better scaling (and therefore a better pass@k k for large k),, while sacrificing the pass@1 performance.
4.5. Analysis of generated conjectures
We observe that the generated conjectures generally require similar proof techniques as the original statements we compute the 20 most frequently used lemmas in the proofs of generated conjectures, and find that among these 20 lemmas, 17 also appear among the top 20 most frequent
4.6. Examples of generated conjectures
In this section, we list three manually selected examples of the generated conjectures the last iteration of the Lean
8

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
10a
Corjectures
theorem _ean_ workbook 2lus__42000 (ha N A /
(a : R)
Unproved Statements
10
S
1)
2' (1 N), 1
4)
Count
10a
The seed statement is special case where a v5/3:
102
theorem 1ean_ saan_workook plus -4203
10
5' : N, (1 * (Real.aqrt .qrt.. 5 (Real sqrt
3)
10
0.0
0.2
0.4
0.6
0.8
1.0
In this case, the conjecture generalizes the given statement by replacing Real. sqrt 5 / 4 with a variable a.
Pass Rate
Figure 6: Histogram of empirical pass rates of generated conjectures and unproved statements the training dataset checkpoint where the cumulative pass rate on Lean- Workbook (Isabelle translation) is 11.4%. The generated conjectures are significantly more likely to be proved (i.e., has a positive pass rate) than the unproved statements in the dataset, and therefore provide denser training signal. Note that the y-axis in log scale.
5. Conclusion
This paper designs Self-play Theorem Prover (STP) that si- multaneously has two roles, conjecturer and prover. By pro- viding training signals to each other, STP goes beyond the statements in the given dataset and its performance continu- ously improves. Our final model significantly outperforms Deepseck-Prove Prover- V1.5 series and achieves statc-of-the ofetth--rt performance among whole-proot generation methods on common formal proof benchmarks. To facilitate future re- search, release code, model, and dataset in this url: https:/ /ST../////./ddd///ST.......
experiment to demonstrate their quality.
Example 1. The generated conjecture says (1 + 2²²n 1+ x" when n 2 1 is an integer and æ E [0, 1]:
theorem l workbook workbook3360811 36081' (x : RR) (hx : 0 < x A < 1) V n :N, n 2
Impact Statement
(1
x) (2+a) 1
x
This paper presents work whose goal is to advance the field of Machine Learning. There are many potential societal consequences of work, none which feel must be specifically highlighted here.
The seed statement says + x² S (1 + ) when x E [0, 1]:
theorem lean workbook 36081 (x I)) (hx
0 < x A < 1) 1 x I (1 + x) ~2
Acknowledgment
In this case, the conjecture is harder than the original state- ment but is proved with similar techniques expanding the powers of a binomial and then using the fact that æ 2 O.
The authors would like thank Yinuo Ren, Zhizhou Ren, Woosuk Kwon, David Hall, Huajian Xin, Kaiyue Wen, and ICML anonymous reviewers for their helpful discussions. The authors would also like to thank the support from NSF RI 221 1780, and NSF CIF 2212263, and the Google TPU Research Cloud for the computing resources that enabled these experiments.
Example 2. The generated conjecture says (x=
1) mod (r 1) < if v. n are integers:
theorem lean httn__woroooo_ooaee 55038" (x : N) (n N (hn 1 n) (x"n - 1) 8 (x 1)
The seed statement says n divides t 1:
References
theorem lean workbook 54038 (n (k N (hn 2 < n) n 1 n
AlphaProof. Ai achieves silver-medal standard solving in- temationna mathematical olympiad problems. 2024. URL https://deet http:///d/deeem.oooggogg//////ee ai-solves- -mm wwwplprsobllaeeeoo at- silve-- medal-level/:
In this case, our model generates variant of the original statement by realizing that b mod equals zero if divides b. This conjecture may help the model connect its proof technique in algebra and number theory. However, the con- jecture itself somewhat unusual and the inequality is not tight. Therefore is unlikely be included in any datasets.
Andrychowicz, M., Wolski, F., Ray, A., Schneider, J., Fong, R., Welinder, P., McGrew, B., Tobin, Pieter Abbeel, O., and Zaremba, W. Hindsight experience replay. Advances in neural information processing systems, 30, 2017.
Example 3. The generated conjecture says Ex2((114))
a) 1-1 i < a <.
Anthony, T., Tian, Z.,, and Barber, D. Thinking fast and slow

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
with deep learning and tree search. Advances in neural information processing systems, 30, 2017.
Jiang, A. Q., Welleck, S., Zhou, J. P., Li, W., Liu, J., Jamnik, M., Lacroix, T.,, Wu, Y., and Lample, G. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.1222 2022b.
Aygün, E., Anand, A., Orseau, L.. Glorot, X., Mcaleer, S. M., Firoiu, V., Zhang, I.. M., Precup, D., and Mourad, S. Proving theorems using incremental learning and hind- sight experience replay. In International Conference on Machine Learning, pp. 198-1210. PMLR, 2022.
Jiang. A. Q., Li, W., and Jamnik, M. Multilingual mathemat- ical autoformalization. arXiv preprint arX1v:2311.03755, 2023.
Azerbayev, Z.,, Piotrowski, B., Schoelkopf, H., Ayers, E. W.,
Johansson, M. and Smallbone, N. Exploring mathematical conjecturing with large language models. 2023.
Radev, D., and Avigad, J. Proofnet: Autoformalizing and formally proving undergraduate-levvl mathematics. arXiv preprint arXiv:2302. 12433, 2023a.
Kaliszyk, C., Urban, J., Michalewski, H., and Olšák, M. Reinforcement learning of theorem proving. Advances in Neural Information Processing Systems, 31, 2018.
Azerbayev, Z., Schoelkopf, H., Paster, K., Dos Santos, M., McAleer, S., Jiang, A., Deng, J., Biderman, S., and Welleck, S. Llemma: An open language model for mathe- maties. In The 3rd Workshop on Mathematical Reasoning and Al NeurlPS 23, 2023b.
Kingma, D. P. and Ba, J. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6900 2014.
Bibel, W. Automated theorem proving. Springer Science & Business Media, 2013.
Kwon, W., Li, Z., Zhuang. S., Sheng, Y., Zheng, L., Yu, C. H., Gonzalez, J., Zhang, H., and Stoica, I. Efficient memory management for large language model serving with pagedattention. In Proceedings of the 29th Sym- posium on Operating Systems Principles, pp. 611-626. 2023.
Colas, C., Karch, T., Sigaud, O., and Oudeyer, P.- Y. Autotelic agents with intrinsically motivated goal- conditioned reinforcement learning: a short survey. Jour- nal of Artificial Intelligence Research, 74:1159-1119, 2022.
Lample, G., Lacroix, T., Lachaux, M.-A., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., and Martinet, X. Hyper- tree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337-26349, 2022.
Dong, K., Mahankali, A., and Ma, T. Formal theorem prov- ing by rewarding Ilms to decompose proofs hierarchically. arXiv preprint arXiv:2411.01809 2024.
Einarsdóttir, S. H., Alhessi, Y., First, E., and Johansson, M. On lemma conjecturing using neural, symbolic and neuro-symbolic approaches. 2024.
Li, R., Allal, L. B., Zi, Y., Muennighoff, N., Kocetkov, D., Mou, C., Marone, M., Akiki, C., Li, J., Chim, J., et al. Starcoder: may the source be with you! arXiv preprint arXiv:2305.06661, 2023.
Guo, D., Yang. D., Zhang, H., Song, J., Zhang, R., Xu, R., Zhu, Q., Ma. S., Wang, P., Bi, X., et al. Deepseek-rl: In- centivizing reasoning capability in llms via reinforcement learning. arXiv preprint urXiv:2501.12948 2025.
Lin, H., Sun, Z., Yang, Y., and Welleck, S. Lean-star: Learn- ing to interleave thinking and proving. arXiv preprint arXiv:2407.1 10040, 2024.
Haluptzok, P., Bowers, M., and Kalai, A. T. Language models can teach themselves to program better. arXiv preprint arXiv:2207. 245002 2022.
Loveland, D. W. Automated theorem proving: A logical basis. Elsevier, 2016.
Jaech, A., Kalai, A., Lerer, A., Richardson, A., El-Kishky, A., Low, A., Helyar, A., Madry, A., Beutel, A., Car- ney, A., et al. Openai ol system card. arXiv preprint arXiv:24 16720, 2024.
Lu, J., Wan, Y., Liu, Z.,, Huang, Y., Xiong, J., Liu, C., Shen, J., Jin, H., Zhang, J., Wang, H., et al. Process-driven auto- formalization in lean 4, arXiv preprint arXiv:2406.0199 2024.
Jiang, A. Li, W., Han, M., and Wu, Y. Lisa: Language models of isabelle proofs. In 6th Conference Artificial Intelligence and Theorem Proving, pp. 378-392, 2021.
mathlib Community, T. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Con- ference Certified Programs and Proofs, CPP 2020, pp. 367-381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781450370974, doi:
Jiang, A. Q. Li, W., Tworkowski, S., Czechowski, K., Odrzygóćdž, T., Mitos, P., Wu, Y., and Jamnik, M. Thor: Wielding hammers to integrate language models and auto- mated theorem provers. Advances in Neural Information Processing Systems, 35:8360- 83833333333,, 2022a.
10. I 11114/337285533333888888 URL ht https: /oi.orgg/ 10.1145/337285.3377
10

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Moura, L. d. and Ullrich, S. The lean 4 theorem prover and programming language. In Automated Deduction- CADE 28: 28th International Conference Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings 28, pp. 625-635,
Panneershelvam, V., Lanctot, M., Dieleman, S., Grewe, D., Nham, J., Kalchbrenner, N., Sutskever, I., Lillicrap. T., Leach, M., Kavukcuoglu, K., Graepel, T., and Hassabis, D. Mastering the game of Go with deep neural networks and tree search. Nature, 529(7676)4444-500 2016.
Springer, 2021.
Nijkamp, E., Pang, B., Hayashi, H., Tu, L., Wang, H.. Zhou, Y., Savarese, S., and Xiong. C. Codegen: An open large language model for code with multi-turn program synthe- sis. arXiv preprint arXiv:2203.13474 2022.
Teodorescu, L., Colas, C., Bowers, M., Carta, T., and Oudeyer, P.-Y. Codeplay: Autotelic learning through collaborative self-play in programming environments. In IMOL In2i-nnlriys Motivated Open- ended Learn- ing workshop NeurIPS 2023, 2023.
Nipkow, T., Wenzel, M., and Paulson, C. Ixabelle/HOL:: proof assistant for higher-order logic. Springer, 2002.
Touvron, H.. Martin, L., Stone, K., Albert, P., Almahairi, A., Babaei, Y., Bashlykov, N., Batra, S., Bhargava, P., Bhosale, S., et al. Llama 2: Open foundation and fine- tuned chat models. arXiv preprint urXiv:2307009288 2023.
Parker-Holder, J., Jiang, M., Dennis, M., Samvelyan, M.,Fo erster, J., Grefenstette, E., and Rocktäschel, T. Evolving curricula with regret- based environment design. In Inter- national Conference on Machine Learning, pp. 17473- 17498. PMLR, 2022.
Trinh, T. and Luong, T. Alphageometry: An olympiad-level ai system for geometry. Google DeepMind, 17, 2024.
Plaat, A., Wong, A., Verberne, S., Broekens, J., van Stein, N., and Back, T. Reasoning with large language models, a survey, arXiv preprint arXiv:2407.1151/ 2024
Tsoukalas, G., Lee, J., Jennings, J., Xin, J., Ding, M., Jen- nings, M., Thakur, A., and Chaudhuri, S. Putnambench: Evaluating neural rrcorem-prover on the putnam mathe- matical competition. arXiv preprint urXiv:2407.1122 2024.
Poesia, G., Broman, D., Haber, N., and Goodman, N. D. Learning formal mathematics from intrinsic motivation. arXiv preprint arXiv:2407.00699 2024.
Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., and Sutskever, I. Formal mathematies statement curricu- lum learning. arXiv preprint arXiv:2202.01334, 2022.
Urban, and Jakubův, J. First neural conjecturing datasets and experiments. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020. Bertinoro, Italy, July 26-31, 2020. Proceedings 13, pp. 315-323, Springer, 2020.
Portelas, R., Colas, C., Weng, L., Hofmann, K., and Oudeyer, P.-Y. Automatic curriculum learning for deep rl:
short survey, arXiv preprint arXiv:2003.cm 04664, 2020.
Wang, H., Xin, H., Zheng, C., Li, L., Liu, Z., Cao, Q. Huang, Y., Xiong. J., Shi, H., Xie, E., et al. Lego-prover: Neural theorem proving with growing libraries. arXiv 2023.
Pourcel, G., Carta, T., Kovač, G., and Oudeyer, P.-Y. Au- totelic llm-based exploration for goal-conditioned rl. In Intrinsically Motivated Open-ended Learning Workshop at NeurIPS 2024, 2024a.
preprint arXiv:2310.00
Wang. M. and Deng, J. Learning to prove theorems by learning to generate theorems. In Proceedings of the 34th International Conference on Neural Information Processing Systems, pp. 18146-18157, 2020.
Pourcel, J., Colas, C., Molinaro, G., Oudeyer, P.-Y,, and Teodorescu, L. Aces: generating diverse programming puzzles with autotelic language models and semantic descriptors. Neurips, 2024b.
Wang. R., Zhang, J., Jia, Y., Pan, R., Diao, S., Pi, R., and Zhang, T. Theoremllama: Transforming general-purpess Ilms into lean4 experts. arXiv preprint arXiv:2407.03203. 2024.
Shao, Z., Wang, P., Zhu, Q. Xu, R., Song, J., Zhang, M., Li, Y., Wu, Y., and Guo, D. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024.
Wu, M., Norrish, M. Walder, C., and Dezfouli, A. Tac- ticzero: Learning to prove theorems from scratch with deep reinforcement learning. Advances in Neural Infor- mation Processing Systems, 0199330-9342, 2021.
Shinn, N., Cassano, F., Labash, B., Gopinath, A., Narasimhan, K., and Yao, S. Reflexion: Language agents with verbal reinforcement learning arXiv preprint cs.A1/2303.1 1366, 2023.
Wu, Y., Jiang, A. Q., Ba, J., and Grosse, R. Int: An inequal- ity benchmark for evaluating generalization in theorem proving. arXiv preprint Siti:200000022244 2020.
Silver, D., Huang, A., Maddison, C. J., Guez, A., Sifre, L., van den Driessche, G., Schrittwieser, J., Antonoglou, I.,

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Wu, Z.,, Huang, S., Zhou, Z., Ying, H., Wang, J., Lin, D., and Chen, K. Internim2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems, arXiv preprint 0tti::2440.1170000 2024.
Xin, H., Guo, D., Shao, Z., Ren, Z., Zhu, Q., Liu, B., Ruan, C., Li, W., and Liang, X. Deepseck-prover: Advancing theorem proving in Ilms through large-scale synthetic data. arXiv preprint 2rXiv:2405.14333 2024a.
Xin, H., Ren, Z., Song, J., Shao, Z., Zhao, W., Wang. H., Liu, B., Zhang, L.,, Lu, X., Du, Q. et al. Deepseck-prover-vll. Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.009 081 52, 2024b.
Yang, K., Poesia, G., He, J., Li, W., Lauter, K., Chaudhuri, S., and Song, D. Formal mathematical reasoning: A frontier in ai. arXiv preprint arXiv:2412. 16075, 2024a.
Yang. K., Swope. A., Gu, A., Chalamala, R., Song. P., Yu, S., Godil, S., Prenger, R. J., and Anandkumar, A. Leandojo: Theorem proving with retrieval-augmentt language models. Advances in Neural Information Pro- cessing Systems, 36, 2024b.
Yao, S., Zhao, J., Yu, D., Du, N., Shafran, Narasimhan, K., and Cao, Y. React: Synergizing reasoning and acting in language models. arXiv preprint arXiv:22 2022.
Ye, Z., Agarwal, R., Liu, T., Joshi, R., Velury, Le. Q. V., Tan, Q., and Liu, Y. Evolving alignment via asymmetric self-play, arXiv preprint arXhv:2411.0008 2024.
Ying, H., Wu, Z., Geng, Y., Wang, J., Lin, D., and Chen, K. Lean workbook: A large-scale lean problem set for- malized from natural language math problems. arXiv preprint arXiv:2406.085 038447, 2024.
Zhang, J., Lehman, J., Stanley, K., and Clune, J. Omni: Open-endedness via models of human notions of interest- ingness. arXiv preprint 200.012306.01711. 2023.
Zheng, C., Wang, H., Xie, E., Liu, Z., Sun, J., Xin, H., Shen, J., Li, Z., and Li, Y. Lyra: Orchestrating dual correction in automated theorem proving. arXiv preprint WwXiv:2309.15800 2023.
Zheng, K., Han, M., and Polu, S. minif2f: a cross-system benchmark for formal olympiad-level mathematics. International Conference on Learning Representations, 2021.
12

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
A. Additional Implementation Details
In this section, we list the missing implementation details,
A.1. Examples of imputs and outputs our model
Here we present some concrete examples to demonstrate the input and output formats of our model.
Examples of the conjecturer. In the following, we show examples of the conjecturer's inputs and outputs. Note that
<1 emma>, <easy theorem>, <hard theorem>, </hará theorem> are the formatting tokens, and the system prompt the first three lines in the input examples.
Input:
Complete the follewing Tean 4 code:
''eann
<lemma>
lemma nonneg (a a1 0
<easy theorem>
theorem lean_workbook 9742 c
0) b 0) (he 2 (hab
b + 1) : a b - cº2 $ a^3 + b93 c^3 : by
nlinarith _e__noneeg (a / 2), sq_nonneg (b 1 2), sq nonneg (c - / 2), _ul_nonneg ha hb, mul_nonneg hb he, mul_nonneg ha he, hab] <hard theorem>
theorem
Output:
lean workbook 9229 (a a R) (a b) ba3 (b c) c²3 (c
(ha
0
1) a^3 1 a*2 b c/24/hard theorem>
b < c) (hab :
a)
In the following example, the lemma is replaced by a trivial statement, and the model can generate conjectures without focusing on any particular direction (see Section 4.1).
Input:
Complete the following Lean 4 code:
""leand
<lemma>
theorem true: True
<easy theorem>
theorem Lean workbook 980 (a b R)) (ha 0 < a) (hb
0 < b) (hab 1/a 1/b = 1)
(/(a 1) + (2 b + 1) < 3/4 by fiepd_simp [ha.ne', hb.ne', ha.ne', hb. hab field_simp [ha.ne', hb.ne', ha.ne', hb.
rw hiv_lle_dv__is (by positivity) (by positivity]]
nlinarith [sq_ nag_nenneg (a b), sq_nenneg (a - x b), sq_nenneg (2 b), hab]
<hard theorem> theorem
Output:
lean workbock 982 (a
R) (ha
a)
(hb b) (ha : 0 < c) (hab tbbb b
1) : / 2 + b 2 1 c n 2 3 4 / (a + b c) 2 (b c ^ ~
/ (c
b) 2 4</hard theorem>
...
Examples of the prover. In the following, we show example of the prover's inputs and outputs.
Input:
Complete the fol following Lean 4 code:
13

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
leean theorem Yean_wcrkbook_5te 52370 (p
N) (hp (hq5 q >= 5) 24 (p^2 2) := by
p) (hg Prime q) (hpq: p >=
Output:
have : p^2 $ 24 = (p $ 22 8 24 : by rw [Nat.pon med]
have : 9-2 24 (q & 24 22 24 by rw [Nat.pow_mott
rw [t Nat add div p 24, + Nat not..mo__addddee q 24] ring_nf
norm_num
have : p & $ 24
p & 24 - V 24 7 V 24
V P
13 V 24
17
p 1po_e__nne____sef__0
19 V 24 23 :- by 2
have :-
have == hp.eq one_or one_or_self_ot
self_ dvd
ser_self_oo of dvd have == hp.eq one_or self of of dvd omega
have hp.eq_one
have $ 24 - 1 24 = 5 V $ 24 7 V q $ 24 = 11 V 24 - 13 V $ 24
17
q $/2 24 19 V =4=22 23 by
have := gg__e__ce__or_sef__fffooo
have : wwt.e__ne__r_sseff...
have : hg._e__one_o__sel_.of..o 5
have = hq..e__ome_or_self_pot
omega
reases this with (h h a
<;> reases this with (h" h | la h
h' h' h') <;>
simp [h, h', pow_two, Nat.mul_mod, Nat.add_mod Nat mod_mod Nat Nat.mod_sseff, zero_add,
Nat. zero_mul, Nat.mod_one,, Nat.one_mul, aat.mod_add_mode
<;> omega ...
A.2. Pseudo-code for selecting the conjecturer's inputs
In the following, present the pseudo-code for selecting the conjecturing imports. Recall that the input for the conjecturer consists of a statement, its proof, and a lemma used in the proof (c.f., Section 3.1). In Step 1, we construct the prompts by taking the correct proofs to statements in the given dataset, and extract the lemmas used in the proof by the formal verifiers. We also allow the model to propose conjectures without focusing on any particular lemma, which is implemented by replacing the lemma statement with a fixed trivial statement in the prompt (see Appendix A. for concrete examples). Finally, we de-duplicate the inputs by the (statement, lemma) pair. After generating the conjectures, we randomly select subset whose size does not exceed the number of remaining unproved statements the given dataset, so that the prover's sample budget is distributed equally between the conjectures and the statements.
We run two heuristic methods to ensure the diversity of the inputs. First, make sure that each lemma / appears at most 0. on times in the inputs because we observe that some lemmas (e.g., sq_nonneg, likely to be included. Second, we make sure that every statement-lemma pair only appear at most once in the prompt, even there are multiple correct proofs.
___onnee) are much more
Alg. shows the complete pseudo-code for selecting the conjecturer's inputs.
A.3. Pseudo-code for preparing the conjecturer dataset.
The pseudo-code for preparing the conjecturer dataset is shown in Alg. 2. The motivations and explanations of each step in Alg. can be found in Section 3.2.
A.4. Pre-processing Lean Workbook
Lean Workbook is a dataset that contains statements translated from natural language math statements (a.k.a,, auto- formalization). The original dataset contains 140K (natural language statement, formal statement) pairs.
14

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Algorithm 1 Prepare inputs for the conjecturer.
Input: list of statements and proofs L
2: Initialize prompt list P= [-
3: for (t, L do
4: Parse the proof and get the set of used lemmas S.
5: With probability 0.5, add the trivial lemma to S.
6: For every lemma E S, add (t,p, 1) to the prompt list
7: end for
8: for I E S
11] > 0.1n then 10: Randomly keep most 0. on prompts with lemma in P.
9: if') p'
11: end if
12: end for
13: De-duplicate P randomly so that every (statement, lemma) pair (t, appears at most once.
14: Return: de-duplicated list of prompts P.
Algorithm 2 Prepare the conjecturer dataset.
1: Input: a list of (seed statement, proof of the seed statement, lemma, generated conjecture, generated proof of the
conjecture) tuples 'D = {(1,, pl. li, 6i (i) and unproved statements Q {44}
2: For each conjecture c, compute its empirical pass rate
P(c) - (# p. is correct))/(#((4 cc).
3: Select conjecturing examples that (a) have low but positive pass rates, and (b) the lemma is used in the proof pf:
D [tt,p'. 1. (tt, 11,,''p)p)) D, e (0, 1/4].
p is correct, is used in p²}.
4: De-duplicate 'D based the conjecture c.
5: Compute the elegancy score
E(c) A min(len(p{) : 1isii n, is correct, Q: = c}
len(c)
Let x be the 20%-quantile of ECc) for conjectures in D.
7: Apply elegancy filter: D = (tt.p', c) D E(c) 2 w}.
8: Find a distribution P supported on the conjectures in D that minimizes the Wasserstein distance W (PP,Q) (Alg. 4).
9: Return: D re-weighted by the density of P.
We de-duplicate the Lean LeanWorbbook dataset by keeping only one formal statements per natural language statement. After de-duplication, get 89,221 formal Lean4 statements our existing dataset w/o proofs for Lean experiments.
For the Isabelle experiments, we translate the Lean4 statements to Isabelle using DeepSeek-V22 V2.5 API with few-shot examples. The prompt to the model is listed below.
Please translate the following lean statement into Isabelle. Please make sure that
1. All the variables are well-typed.
2. All the functions are correctly translated into the corresponding Isabelle functions.
3. All the symbols are correctly translated into corresponding Isabelle symbols.
4. Please directly output the translation without explanation.
Hore are some hints for the translation:
1. In Isabelle, the second operand of the operator should be integer. For real numbers, please use powr instead.
2. Please define the types of numerals.
15

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
3. 'Real.loge y should translated to 'log x y
4. "Real.sque x should be translated to 'sqrt x'.
5. Variables with subscripts should be disallowed. For any variable nanes of form a_b, translate it to ab.
6. Please translate superscripts
the corresponding expenential form. For example, x should be translated to (x powr -1).
7. 'a I b' should be translated to 'a dvd b..
8. "x = y [ZMOD pl should be transiated to 'x mod mod p'.
9. 'x E zmod p should represent that is nat and x p.
## Input:
theorem lean workbook 50 (a 1 A 2 C A 0)
(ha
(hab : a a
3)
=a"3 + b-3 + cº 216
a) / (24 + + a) $ 27 :
by sorry
...
## Output:
"IIsbblle
theorem lean_ Sran_workbook_0
fixes с 1: real
assumes "a 2 A b 2 0 A c 2 0"
assumes "a b c 3"
shows =**3 b-3 + 603
216 (a b
a) / (24 b
S
27
sorry
## Input:
**eaa
()
Output:
A.5. Re-weighting the conjecturing dataset
In this section, we describe the motivations and implementation details of the re-weighting method for the conjecturing dataset.
Motivation. In our early experiments, we observe that the generated conjectures tend to have mode collapse issue after several iterations of self-play training. For example, the generated conjectures are mostly about algebraic manipulations even when the seed statements contain questions about, for example, number theory. This is partly because the Lean Workbook dataset contains significant portion of inequality questions.
Therefore, in addition the particular conjecturing format where we require that the proof of the conjecture must the lemma given in the input, also re-weight the conjecturing examples every iteration. Intuitively, if there is distance function that can separate statements of different topics, the Wasserstein projection of the conjectures will have similar distribution of topics, and therefore alleviates the mode collapsing issue.
We compute the cost d(x, y) of matching conjecture similarity between their embeddings, and the embedding is computed by the last hidden layer of the current model averaged over the sequence dimension. Since our model is trained to generate proofs of conjectures and statements, we expect that statements with similar proof techniques tend to have similar embeddings, and therefore smaller cost for the matching.
Cost function.
statement y by the negative of the cosine
Algorithm. On the high level, our method computes re-weighting of the generated conjectures that minimizes its Wasserstein distance to the unproved statements in the given dataset. Abstractly speaking, let be the set generated conjectures, and Q the set of unproved statements. Let d(r, y) be the distance between conjecture and statement y.
16

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Then, the optimization problem can be written as
argmin
W(P, Q),
P.P valid distribution, (upp(P))X
where Q) is the Wasserstein distance between P and Q (with little abuse of notation, we use Q to represent the uniform distribution over the unproved statements). The Wasserstein distance (PP, Q) is defined by the following optimal transportation problem where μ is a matching between the distribution P and Q:
Q(P.Q) min 1
E résupp(P).
(1 (x,
(2)
s.t.
Σ
p(z, v) = P(x).
(3)
vÉsupp(Q)
Σ
pl v) Q(v),
(4)
rEsupp(P)
u(z, 2 0, Vx,
(5)
Combining the equations above, the re-weighting distribution P can be computed by
argmin min Paupp(P)CX
Σ
u(x,y)d(z,)) v)
(6)
#Esupp (E)ppp))))))))))
s.t.
Σ
u(z,v) = P(xx)
vEsupp(Q)
Σ
u( 3) = Q(y),
(8)
xEsupp(P)
m(x, 2 0, Yr,y:
P(x) 2 0, Va,
(10)
Σ P(x)= ZEX
(11)
where the last two constraint ensures that P is valid distribution. Equivalently, we get the following program,
argmin min Psupp(P)CX
Σ
u(x,)))(x,,
(12)
s.t.
Σ
u(x,y) = Q(y),
(13)
zESupp(P)
Σ
u(x.v) = 1,
(14)
u(x,y) 2 0, Va,
(15)
P(x)= =
Σ
p(z,y). v).
(16)
vEsupp(Q)
Since Qyy) is given, can optimize uut,, v) for every fixed y separately, and then compute the final P(x) using Eq. (16). As a result, the program above has closed-form solution (xx2x) y) = Q(y) [x = argmin d(z', v)] and P(z) Eyesupp(() (z, y). In other words, the optimal matching μ(xxv) y) for any given y is only supported at the x that minimizes the distance d(ar, v). Therefore, the (theoretical) algorithm that computes the optimal re-weighting is given in Alg. 3. Note that the last line in Alg. 3 is to make sure that the sum of the weights equals the number of generated conjectures (i.e., the sum of weights before re-weighting).
Our practical implementation is shown in Alg. 4. In this implementation, we additionally requires that the weighting P for every conjecture x cannot be too big because otherwise might cause instability of the LLM training with weighted cross
17

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Algorithm 3 Computing the optimal re-weighting (theory).
Input: generated conjectures X' { Fnn. of size n, unproved statements Q with size m, and distance function
d(x; y)-
2: Initialize the optimal re-weighting P [0, 0....... ,0.
3: for Q do
4: Compute x² = argmin d(a, y).
5: P(x*) < P(x") 1/m.
6: end for
7: Return: the optimal re-weighting (P(x1) * n, P(rz) * n. P(an) * nl.
entropy loss. We also allow unproved statements Q to have different matching weights - an important statement can be matched more than one conjecture (see Line 5-6 of Alg. 4). In both the Isabelle and Lean experiments, the statements from Lean Workbookk have matching weight 1. The statements from miniF2F-valid and ProofNet-valit have matching weight 1 for the first 24 iterations in the Lean experiment, and 128 afterward.
Algorithm 4 Computing the optimal re-weighting.
1: Input: generated conjectures X' {<11.-. Ind of size n, unproved statements Q with size m, and distance function d(z, v).
2: Initialize the optimal re- re-weighting P = [0, 0.. .0.
3: Initialize the masks Mxx) = 1, Vo E X'
4: for E Q do
5: Let k be the matching weight of y.
6: Let xe L ... ,x be the k conjectures with smallest value of d(- (-).
7:
for === 11,....... do
8:
P(x*) < P(x') + 1/m.
9:
if P(x') n 3 then
10:
M(x') <- 0.
11: end if
end for
end for
14: Return: the optimal re-weighting is [P(x1) *n, P(xz) * n,... P(.n) m).
A.6. Implementation details for expert iteration.
In this section, we describe two different implementations of expert iteration and compare their performance.
Vanilla expert iteration. For vanilla expert iteration, only sample proofs to the unproved statements in the given dataset. The LLM training dataset consists of all the correct proofs generated in this and previous iterations, and in each iteration, the model is trained from the base model.
Optimized expert iteration. The most significant issue of vanilla expert iteration is the limited correct proofs generated in each iteration. As result, even though the model is re-trained at every iteration, the difference between two models in consecutive iterations are limited.
Therefore, in our optimized implementation of expert iteration, we generate proofs to all statements in the given dataset, regardless of whether they are previously proved or not. Then, to construct the LLM training dataset, we randomly choose most 16 proofs per statement (so that the model does not overfit the easy problems with many correct proofs). Note that this implementation requires slightly more sample budget per iteration. However, since the pass rate on the given dataset is low (less than 30% even for our best model), this difference is not significant.
In Fig. (Left), we plot the cumulative pass rate two implementations of expert iteration, STP and parallel sampling. STP outperforms both implementations of expert iteration, and the optimized implementation expert iteration better than the vanilla implementation.
18

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Training performance LeanWorkbook
Performance LeanWorkbook (Isabelle translation)
26
12
Cumulative pass rate
Cumulative pass rate
10-
22
9-
20
(Ours)
7-
STP (Ours)
Optimized expert iteration
Expert iteration
16
Vanilla expert iteration
6-
Paraliel sampling
Parallel sampling
20m
40m
60m
80m 100m 120m
50m
100m
150m 200m
250m
300m
Training compute
Training compute
(# gegeneatedd proots)
(#generated proots)
Figure 7: Left: Comparison of pass rates between STP, two implementations of expert iteration, and parallel sampling methods on LeanWorkbook. Right: Comparison pass rates between STP and baseline methods on Lean Workbookkk (Isabelle translation). The red crosses shows the points where we refresh the self-play training described in Section 4.1.
For the figures of Isabelle experiments, always the optimizes implementation of expert iteration. For Fig. 2, the vanilla implementation.
A.7. Additional details for interacting with the Isabelle verifier
For the Isabelle experiments, have additional filter for the conjectures - if the generated conjecture is equivalent to the statement in the prompt (tested by
in Isabelle), consider it invalid.
We disallow the tactics sledgehammer, mason, smt, metis, sos by invalidating proofs that contain any of these sub-strings. However, following the implementation of Jiang et al. (2022a), we still use the keyword 'sledgehammer" to replace the following simple tactics
[by auto, by simp, by blast, by fastforce, by force, by eval, by presburger, by arith, by linarith, by (auto simp: field_simps]
During proof verification, we try these tactics sequentially to replace the keyword 'sledgehammer". If any of the tactics succeed, we proceed to the remaining proof steps. Otherwise flag the proof incorrect.
A.8. Additional details for interacting with the Lean4 verifier
During the self-play training, we use the same imports as the miniF2F Lean4 project instead importing the entire Mathlib optimize the memory efficiency. This is because we do not have access an additional CPU cluster for proof verification, and the available CPU memory in TPU-v4 VMs is limited.
A.9. Compute resources
Our experiments are primarily done on TPU-v4 VMs with 32 nodes. Each node contains TPU chips (8 TPU cores). 240 CPU cores, and 400G memory. We use vLLM (Kwon al., 2023) to generate LLM outputs, and Levanter'! train the LLM. In both STP and expert iteration, since the generated proofs are heavily filtered (based on the correctness, elegancy, trivialness, etc.) when constructing the training dataset, LLM training only takes less than 25% of the wall-clock time for TPU compute, and generating proofs takes the rest 75%.
"https://g/ 22..://m/aaankky11//mm222-----1 "https:// hhw..coom/ttaaooodeooooo
F2F
19

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
B. Additional Experiment Results
In this section we show the additional experiment results with both Lean and Isabelle formal verifier.
B.1. Additional results with Lean
In Table 4, we compare the performance of our method with prior works on PutnamBench. Note that DSP (Jiang et al., 2022b) uses Isabelle verifier where PutnamBench only has 640 statements. Our model STP achieves state-of-the-art performance by solving
644 problems.
Table 3 compares the model obtained by final re-training with and without the proofs of generated conjectures, discussed in the ablation study section (Section 4.4). The results show that it is still beneficial to re-train with the generated conjectures in addition to the successfully proved statements in Lean WorkBookk even for performance miniF2F-test and ProofNet-test, which leads to about 2-3% performance gain (for pass@ 128).
Table 3: Pass rate miniF2F and ProofNet.
Method
Sample budget
MiniF2F-tess
ProofNet-test
STP (w/o conjectures) STP
128
58.3%
0.7%
17.4%
0.4%
128
61.2%
0.6%
19.5% 0.7%
B.2. Additional results with Isabelle
In Fig. (Right), we plot the pass rates of STP and baseline methods on Lean Workbook starting from iteration 0. The red crosses shows the points where we refresh the training process described Section 4.1. Our models are tested with PutnamBench (Tsoukalas al., 2024), commit d49896f.12
Table Results on PutnamBench.
Method
Sample budget (#Proofs #Steps)
Result
Whole-Proot Generation Methods
DSP (GPT-4o) (Jiang al., 2022b) STP
10
4/640
128 3200
7/644
8/644
Tree Search Methods
IncemL..2.-SStpPrroe-----CCC
x 32 600
6/644
B.3. Examples of unproved statements in Lean Workbook
In this section, we list 20 randomly selected statements from Lean Workbook that are not proved during STP training, The following table shows the formal statement, the corresponding natural language statement Lean Workbook, the correctness of formalization, and the correctness of the formal statement.
# Lean formal statement
Natural language statement
Correct
Correct statement?
formalization?
theorem
lean workbook 7116
If = b²,b= 3² 2,c== z² suffices to show
Yes
No. The case
y
2
(hx
x
y
z
that: x +y+++ =3 2 2
3)
4
+
+
2( + 5
de- fined.
3 <
(1
x
2
1
2
+
21
1= by
"httpss///gtthub.cmm//rrt http:///eggcoooocccooeeeeeeeeeee
6dd894
20

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
2 theoren
Prove that if a = (mod nt), then 6" Yes (mod n²
Yes
_aa___orbooo__ps______ _23990 (a
b.n N) (h b [XMOD
n]) a b [XMOD n*2] by
3
theorem Tean_ wor_wwok _3344
For:
Yes (but maybe missing implicit sumption a.b,c> 0)
No (e.g.
(9
atb+ct a blabbbctca)
a48
bic
the
(a, c)
Real.sqrt (3
b
c+a
as-
(-0,5, 1, 1).)
b* c c * all)) & (1 (a
b) + (b + c) 1 (c
a)) by
4
theorem lean_workbook_Bal _8800
Prove that + + b/ + cv + 3v2,
+
Yes
No
(a c R] ~ 2
Real.se. sqrt
Real.sert (c a Real.sqrt (a 2 b
2)
2) < 3 Real.sqrt 2 i= by
5
theorem
Put Vx =a. The equation equivalent
Yes
No
lean
00118_44018
a² 2a (a -4) v 7 3a + 28
0
(x R) (hx 0 < x) (a R
(ha (1/3)) a
2+a (a*3 Rera
(a"3 7) 3*a*3 28 :=
by
6
theorem
ba,bbc b, > prove disprove
a4-2h-3c 4a4b46
+
Yes
Yes
lean www.wooo__pplite plus 35882
(a b c R) (ha 0 a)
bo a+40+ a+b+de
2043bbe
2 3
(hb 0 < b) (hc 0 < c)
(Real.sqrt ((a + 2 b
c) (4 a a + c))
Real.sgrt (13 +
c) / (a + b g)) +
Real.scrt (12
c) (a by
2)))
7
theorem lean_workbook_12611
Let + +x 1(2, R) Prove
No (there is
No
y : R (x²2+x*xy+y²2)
that +11433)) S x² + 2ry s
xy in Lean. Should x y)
-1-33( -(t)))(Realsssp
(62)2)=(69111Reeal.
169++13333
33)) < x
x^2+2*xay < (1/3) *Real. sqrt (1922 .grt )
:- by
8
theorem
Prove that f([(z)+1) f()) + for all real
Yes
No
lean_workbood pllspppuuppp 20629
R R) (x
+
by
9
theorem lean_workbook_21 337208 (n
Prove that: Vai itive integer
1
for every pos-
Yes
Yes
: N) (hn
/ / (n! : :R) /1 n)
(1 ++11/ a)*n := by
10
theorem 1ean_ Gean_workbook_1u 10259
Given N(a that a+b +b=²² godla, b) Prove that +b d Letd = detd
Yes
Yes
b N) (hab a # b) (h
a b + 2- : a
& (Nat.geo
b4 := by
11
theorem lean workbook 45322 (a b : [R) (ha : < a) (hb
Let > 0 and + (bb 5) 2+ - Prove that S at + ba <
Yes
0 <) (hab (a + 1
a) (b + b) 2
Real.sgrt 1 <
4 4
by
21

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
12
theorem lean_workbook_2
2889
prove: 184F
48x
Yes (but maybe missing x 2 0)
No
(x
R] Real. sqrt (1
- -1/24,
22 212
48
ty
211 Z (184
8(x 47
1
x
1y
2
2
2)
289
x
* 1y
+
21
127
*
2) 1
18
18
2
y
2
2)
47
y)) :- by
13 thcorem loan_workbook_33 33663
Solution without Geometric Formula f + We divide everything by We substitute the
Yes
Yes
(x R) (ho : E' k N, (7
(2*k)) x)
14 by
original equation in: -
Therefore, x 14
14
theorem lean workbook 4086 (g N + N) (h1
Given g(1) = g(1) = g(1) =1
No (natural lan- guage statement is unclear) Yes
2) -1=1
by
15
theorem lean lean_ wtt__ookkoook__90 6922
Let a, 0 and
2. Prove that
Yes
(a bbb [)) (ha : 1 a) (hb
a "V 2+76 + by 2470
b
+ V I48a6 2
c S b) (hab : 2 _ a b)
Real.sqrt (a / (2 + +
b)) +
sqrt (o
+7* a)) sqrt
+1+8-1 + b)) 2 :- by
16
theorem
Find all functions / R - R such that f(++((v)) v ((++))),,,,++ for all 2. R.
Yes
No
lean workbook plus 65183 : R R) (4 x y,
f y) -
(x + 1)) 4 (V
x, -fxxx+1
V (4 8, f x
+ 1) 1= by
17 theorem lean aa+ +
(a b c workwookkkokkkooo 26330 26304
aa+b+es a- 1e
No (natural lan- guage statement is unclear)
No (e.g.. abe
(a*2 + b* b-2 x-2 c^2
and
a*2) (a * bbbb 2) : by
+ b >
18
theorem
Solve the following system of equations: + I xty +==1 r+y+z =1
No
No
lean_workbook.
(x 2 R) (hx x +
= 1) (hy
yh3 +
1) (hz
y 2-3
x = y=yAA = A
== by
19
theorem
Let A E Mn(C) be so that A A = On Prove that A On Here, A' the transpose A.
Yes
No (not true for complex matrix)
lean workbook plus_51637 51637
Matrix (Fin n) (Fin n) C
) (h : : A.transpose = 0)
= by theorem
20
We also have nice inequality
<
Yes
No (when xt, y, 2
Vyz
lean_workbook_pp Nwn__oorkbook_plu____3 Battooo_plu______00
(x y R] (hx
x) (hy 0 < (hz : 2)
y
2
1
V2.
- 0. this
x+1 V ZED 4 VTy +
term goes to 3)
(Real.sqre
2)) (1
With and 2 are the best constant.
(x + 1)) +y (Real.sqrt
(2 * x))
+ 1))
(Real.sgrt (x + {))
/ ( x /Real.RR
z)) * (1
(x+ 1))
(Real sqrt x))
(y + 11) + +2 2// (Real.sgrt
(x ()) * (1 (z 1))
Real.sort 2 := by
22

---

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
B.4. Most frequent shared lemmas in Lean
In this section, we list 30 most frequently shared lemmas in the Lean experiments.
nonneg,
nonneg, div_le div iff, Real. sq sqrt, Resl.sin_add add, Real.sin Real.sin_ss_add add cos_ sq, Real.cos_ add, pow_ two, div _efif Real sub,, Real.sin_suth Real.cos sq, Real.sin two st____tt__lll______________ mul, Real.cos_two _os__tt__mu,, pow www_ull div _____e, Real.squt_pos, pow_add, Roal.tan_er_sin_ddl.. pow_pos, Real.cos cos____________s Nat Nat abs_mul, abs_cases, pcai.pi_pos, hat_sub_dvd_pose
Real.sin_two
one, abs_le, Finset. Finsot.prod_ranme proe_range_suucee www.sunaannnccooosse... Nat pow__no, pow_three,
23


Reviews:
[{"review_id": "P976sqp0KI", "reviewer": "Reviewer_ubJp", "summary": "The paper introduces the Self-play Theorem Prover (STP), a novel method for training large language models (LLMs) in formal theorem proving, addressing the scarcity of high-quality training data. STP employs an LLM in two roles: a conjecturer that generates new mathematical conjectures based on existing theorems and proofs, and a prover that attempts to prove these conjectures alongside statements from an existing dataset. The process is iterative, with the conjecturer trained on previously generated conjectures that are challenging yet provable by the current prover, enabling continuous improvement without additional external data. The method is evaluated on LeanWorkbook, miniF2F, ProofNet, and PutnamBench, achieving SoTA results across the board.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank reviewer ubJp for their positive review, and for noting “The claims are well-supported by clear and convincing evidence”. In the following, we address the reviewer’s questions/comments in detail.\n\n> One claim appears problematic: \"STP proves 26.3% of the statements in the LeanWorkbook dataset, doubling the previous best result of 13.2% achieved through expert iteration.\" I cannot find a reference for this reported 13.2%, and according to Figure 2, expert iteration appears to perform better than this stated number.\n\nThe number 13.2% is reported in [1] — they prove 13.1% statements in LeanWorkbook and disproves 3.9% (we realize that we made a typo in the paper. The correct number should be 13.1%). We will add a reference in the paper upon revision.\n\nFigure 2 shows the performance of expert iteration with the base model DeepSeek-Prover-V1.5-SFT, which is indeed better than 13.1%. However, in the original paper [2], they do not report any number on LeanWorkbook. Therefore, Figure 2 is based on our reproduction of [2].\n\n[1] Wu, Zijian, et al. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems.\n\n[2] Xin, Huajian, et al. Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search.\n\n> What is the intuition behind the construction method of the conjecture dataset? Why can theorem Y be a good conjecture for theorem X?\n\nWe construct the conjecture SFT dataset so that the generated conjecture (Theorem Y) is related to the given theorem (Theorem X) in the sense that they use the same seed lemma in the proof. The conjecture dataset at the SFT stage only serves as an initialization of the model, and the conjecturer will gradually learn to generate diverse, challenging yet approachable, and relevant conjectures by STP’s iterative training via the datasets constructed later (Section 3.2).\n\n> How does the final re-training affect evaluation performance? What if it is removed?\n\nThe following table compares STP and STP w/o retraining. In general, STP w/o retraining has a higher pass@1 but lower pass@k for large k. We will add this result in the paper upon revision.\n\n| Method             | Sample budget | miniF2F-test | ProofNet-test |\n|--------------------|---------------|--------------|---------------|\n| STP w/o retraining | 1             | 45.1%        | 7.8%          |\n|                    | 128           | 57.2%        | 16.9%         |\n|                    | 3200          | 60.7%        | 21.5%         |\n| STP                | 1             | 41.1%        | 5.9%          |\n|                    | 128           | 57.2%        | 18.0%         |\n|                    | 3200          | 61.1%        | 23.1%         |", "claims_and_evidence": "The claims are well-supported by clear and convincing evidence. Table 1 compares STP with prior methods on miniF2F-test and ProofNet-test, showing higher pass rates and sampling efficiency compared to previous baselines and RL training. Figures 2 and 3 illustrate STP’s scaling advantage over expert iteration and Deepseek-Prover-V1.5 models.\n\nOne claim appears problematic: \"STP proves 26.3% of the statements in the LeanWorkbook dataset, doubling the previous best result of 13.2% achieved through expert iteration.\" I cannot find a reference for this reported 13.2%, and according to Figure 2, expert iteration appears to perform better than this stated number.", "methods_and_evaluation_criteria": "The STP method is well-suited for formal theorem proving. Its iterative conjecturing and proving process, inspired by mathematical practice, effectively addresses data scarcity through a self-adaptive curriculum. The evaluation criteria—pass rates on standard benchmarks such as LeanWorkbook, miniF2F-test, ProofNet-test, and PutnamBench—are appropriate and widely accepted in the field. Testing on both Lean and Isabelle verifiers demonstrates generalizability across formal languages.", "theoretical_claims": "I reviewed the derivation in A.5 for the re-weighting method and it looks correct.", "experimental_designs_or_analyses": "The experimental designs are sound and the comparisons are fair. The paper could be further improved through additional ablation studies on key design choices, for example, the filtering and re-weighting process for conjecturer training and the effectiveness of the final re-training phase.", "relation_to_broader_scientific_literature": "The work is well situated within current trends in using LLMs for theorem proving. It also builds on previous studies on RL and self-play training.", "essential_references_not_discussed": "I can't notice any.", "other_strengths_and_weaknesses": "**Strengths:**\n\n- The proposed method is novel and well-motivated;\n- Empirical results are strong and comprehensive;\n- The paper is well-structured, with intuitive explanations and illustrative figures.\n\n**Weaknesses:**\n\n- Ablation studies on the key components of the proposed method are missing.", "other_comments_or_suggestions": "Line 34 in abstract: versifiers → verifiers", "questions_for_authors": "- What is the intuition behind the construction method of the conjecture dataset? Why can theorem Y be a good conjecture for theorem X?\n- How does the final re-training affect evaluation performance? What if it is removed?", "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": "q1MgXIWNRL", "reviewer": "Reviewer_dMfo", "summary": "The paper studies the problem of improving LLM theorem provers through training on self-generated conjectures. The approach, called Self-play Theorem Prover (STP), is a framework to train LLM theorem provers in a dual conjecturer-prover setup, evaluated with Lean and Isabelle as formal verifiers. STP is initialized with supervised fine-tuning on proof libraries like Mathlib, then iterates through a self-play loop: the conjecturer, built on DeepSeek-Prover-V1.5-SFT, generates conjectures from seed theorems and lemmas, guided by a reward function targeting low but positive empirical pass rates and an elegancy score. The prover, trained via expert iteration attempts proofs with a fixed sampling budget per statement / conjecture and the proofs are verified with Lean / Isabelle. With 19.8 billion tokens generated over 24 Lean iterations (120M proofs, 2M conjectures), STP achieves a 26.3% cumulative pass rate on LeanWorkbook and strong performance on miniF2F-test, ProofNet-test. The approach is also evaluated on Isabelle, using Llemma-7b as the base model, and show strong performance on a translated version of the LeanWorkbook and PutnamBench and observe strong performance gains.\n\n### Update after rebuttal: \n\nThe authors clarified several of my concerns during the rebuttal and considering the other reviews, I maintain my positive assessment of the work", "questions": "", "limitations": "", "rating": 5, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank reviewer dMfo for their positive review, and for noting “The experiment design overall is quite sound”. In the following, we address the reviewer’s questions/comments in detail.\n\n> The authors do not include code to reproduce the results. I appreciate the details in the paper but releasing the code would be an important contribution (considering the strong results)\n\nWe have fully released our code, data, and model weights after the submission deadline. We also provide an anonymous version in the links here: https://anonymous.4open.science/r/STP_rebuttal-85F9. \n\n> The DeepSeek-Prover baseline appears to be missing in Table 3.\n\nThe original DeepSeek-Prover paper does not report the number on PutnamBench. In the following, we report the test result of DeepSeek-Prover-V1.5-RL model conducted by ourselves, and we will include the results in the paper upon revision.\n\n| Method                  | Sample budget | Result |\n|-------------------------|---------------|--------|\n| DeepSeek-Prover-V1.5-RL | 64            | 6/644  |\n|                         | 3200          | 7/644  |\n\n> a bit more analysis of the conjectures would be useful. For instance, some details about what the distribution of topics looks like among the generated conjectures or how similar they are to the problems in LeanWorkbook.\n\nThank you for the comments. We can look at the distribution of lemmas used to prove the generated conjectures as a proxy of their topics. Here are the 20 used lemmas with highest frequency, and the majority of the topics are algebra and inequalities:\n\n```\nsq_nonneg, mul_self_nonneg, div_le_div_iff, Real.sq_sqrt, div_le_iff, Real.sin_sq_add_cos_sq, pow_two, Real.sin_add, Real.cos_add, Real.sqrt_pos, div_nonneg, Real.cos_sub, Real.sin_sub, pow_pos, Real.cos_two_mul, Real.cos_sq, div_le_one, Real.sin_two_mul, pow_add, pow_mul\n```\n\nAmong these 20 lemmas, 17 also rank among the top 20 most frequent lemmas in LeanWorkbook. This suggests that the generated conjectures are generally similar to the problems in LeanWorkbook.", "claims_and_evidence": "C1: Propose a self play mechanism for training LLM Theorem provers which enable continuous improvement without requiring additional data and achieves state-of-the-art among whole proof generation methods\n\nThis is the central claim and contribution of the paper. The experiments in Section 4 provide much of the evidence for the claim. In particular Figure 2, 4 and 5, provide evidence for continuous improvement over iterations of conjecture generation and proving. Table 1 provides the results on miniF2F and ProofNet and Table 3 consists of results on PutnamBench, and STP achieves state of the art performance, outperforming DeepSeek-Prover-v1.5 (I’d like to note that DeepSeek-Prover baseline is missing in Table 3). The results also demonstrate strong performance of the method across two different base models (Llemma and DeepSeek-Prover-1.5-SFT) as well as two different proof verification systems (Lean and Isabelle). Overall there is strong evidence for the claim.  \n\nC2: Self play mechanism provides denser training signals making training easier and retraining with generated conjectures improves performance\n\nThe authors conduct two ablations, with results presented in Fig 6 and Table 2, which provide sufficient evidence for these claims.", "methods_and_evaluation_criteria": "The authors use standard benchmark datasets miniF2F, ProofNet, and PutnamBench. The methods used for comparison are also established state-of-the-art to the best of my knowledge.", "theoretical_claims": "N/A", "experimental_designs_or_analyses": "The experiment design overall is quite sound, but there are a couple things which seem lacking:\n- The DeepSeek-Prover baseline appears to be missing in Table 3.\n- There are some examples of generated conjectures in the paper, but I think a bit more analysis of the conjectures would be useful. For instance, some details about what the distribution of topics looks like among the generated conjectures or how similar they are to the problems in LeanWorkbook.", "relation_to_broader_scientific_literature": "A key contribution of the paper is to demonstrate that self-play can be employed at scale for training strong LLM theorem provers. This contribution is important in the context of theorem proving, and also presents potential avenues for the broader topic of reasoning with LLMs.", "essential_references_not_discussed": "N/A", "other_strengths_and_weaknesses": "Strengths:\n* The paper is generally quite well written and easy to follow. There are also many details about the approach which make it easy to understand. \n* The overall approach is also relatively straight-forward, which in my opinion is a strength since it makes the approach easier to use for others to to build upon and scale. \n\nWeaknesses: \n* The authors do not include code to reproduce the results. I appreciate the details in the paper but releasing the code would be an important contribution (considering the strong results)\n* As the authors discuss in the paper, the overall approach is fairly similar to Minimo (Poesia et al. 2024) but scaled up to Lean, with simpler conjecture generation. The novelty of the approach is thus somewhat limited. To be clear this does not detract from the paper (as indicated by my positive score) but I believe it is worth mentioning.", "other_comments_or_suggestions": "N/A", "questions_for_authors": "Please see the sections above.", "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": "CCX0urgeZa", "reviewer": "Reviewer_vtLT", "summary": "The paper proposes a novel method called **Self-play Theorem Prover (STP)**. STP addresses the shortage of high-quality training data in automated formal theorem proving by simultaneously training two roles: a **conjecturer** that produces new theorems (or “conjectures”) and a **prover** that attempts to prove them. This approach is aimed to overcome the plateau seen in reinforcement learning (or “expert iteration”) methods.\n\n  STP continually generates fresh conjectures that match the model’s current skill level—“barely provable” ones (the proof rate (0, 1/4]. The prover’s successful proofs of these conjectures supply training data to improve the model’s proof-writing capabilities. Through experiments using **Lean** and **Isabelle**, STP is shown to outperform standard baselines.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank reviewer vtLT for their review. In the following, we address the reviewer’s questions/comments in detail.\n\n> Fig 2 - I am not sure how strong the baselines are (and how much effort has been given into tuning them)\n\n We spend equal efforts in tuning the baselines and STP (if not more efforts on tuning the baseline). We mostly use off-the-shelf configurations for finetuning LLMs, and only optimize the learning rate and sampling parameters. Our reproduction of DeepSeek-Prover-V1.5-RL on LeanWorkBook is actually better than the best previously reported accuracy. We believe that the amount of tuning is more than sufficient given the enormous gap between our methods and baselines — we don’t expect the hyperparameters in the baseline to make any difference nearly comparable to the gap between ours and the baselines.\n\n> Fig 3 - I find comparisons with Deepseek-Prover not quite informative without careful information on the training budget of the two methods (and any detail to ensure an apple-2-apple comparison)\n\nFirst, we’d like to point out that our model is trained on top of Deepseek-Prover-V1.5-SFT. Hence, we assume that the reviewer’s question is about the comparison between STP and Deepseek-Prover as if it were trained with the same additional compute (please kindly let us know otherwise). \n\nSince Deepseek-Prover-V1.5-SFT is trained with expert iteration, our expert iteration baseline simulates the performance of DeepSeek’s model as if it were trained for more iterations. Note that the training compute is approximately proportional to the number of generated proofs during training (for our method, we count the proofs of both the statements in the given dataset and the generated conjectures; for expert iteration, we count the proofs of the statements in the given dataset). Therefore, Figure 2 is an apple-to-apple comparison between our method and DeepSeek-Prover.\n\n> Table 1 - the same as above. Moreover, I am not sure what the difference is between the Sample budget (#proofs) and sample budgets (#steps).\n\nSample budget (#proofs) and sample budgets (#steps) are two different ways to measure the inference-time compute. For whole-proof generation methods (generating an entire proof auto-regressively by LLM, such as STP), sample budget (#proofs) is the most common metric for inference-time compute, which means the total number of proofs generated independently per problem. Sample budgets (#steps) is mostly used for tree search methods that use LLMs to generate single proof steps (e.g., a single line in the proof) then search for a complete proof by best first search or MCTS. We introduce the two approaches for completeness. \n\n\n> another subtle issue about the comparison of STP and deepseek is how much the presented method 'overfits' to benchmarks. Following that, I'd love to see a deep analysis of the generalization properties (although doing this properly might be another paper)\n\nWe assume that the reviewer’s question is about whether any method overfits to the benchmarks like miniF2F, ProofNet, and PutnamBench. The STP checkpoint (Line 291) is only trained on LeanWorkbook, and we do not use any early-stopping methods that may leak information about the test datasets. In addition, miniF2F, ProofNet, and PutnamBench cover statements from different sources and of different difficulty. Therefore, we believe that it is unlikely for STP to overfit to all three test benchmarks at the same time.\n\n(If the reviewer’s question is about whether STP or DeepSeek-Prover overfits to formal proofs, the answer is yes, but that’s expected because they are only trained on formal proofs. None of the models can generalize to natural language tasks, and we believe that generalizing formal proofs to natural language tasks is still an open question.)\n\n\n> In the RL parlance, the presented work can be framed as an exploration problem and curriculum construction. I find it strange not to include a short discussion about these topics. I do not insist on going deep.\n\nWe thank the reviewer for the comments. Our method can indeed be framed as automatic curriculum learning (e.g., [1]) and we included some of the related work in Line 177-183. Upon revision, we will include a more broad discussion on their connections.\n\n[1] Portelas, Rémy, et al. Automatic curriculum learning for deep rl: A short survey.\n\n> I'd love to see what is the limit of the method. Does it plateau, when, why?\n\nAfter the submission, we run STP for longer, and it continues to improve. With about 50B generated tokens (requiring 86K TPU-v4 hours in total; 2.5x the compute used in the submitted experiment), STP reaches at approximately 28.5% pass rate on LeanWorkbook, significantly higher than the best reported in the paper. We don’t have compute to run even further. We also estimate that only about 50% of LeanWorkBook statements are correct, and thus, 28.5% is already pretty high.", "claims_and_evidence": "The main claim of the papers is that it enables data generation via a self-play mechanism. The key novel element is a generation mechanism of well-calibrated conjectures. The benefits of this are shown by comparisons with two baselines: expert iteration and parallel sampling. The paper claims significant improvement with respect to these baselines. \n\nThe paper also claims to outperform DeepSeek-Prover-V1.5-RL on the Mini-F2F and ProofNet benchmarks. The evidence is pass rates gathered in Table 1.", "methods_and_evaluation_criteria": "The method can be shortly summarised as follows:\n\nA single large language model (LLM) alternates between two tasks:\n\t1.\tConjecturer, that generates new mathematical statements (conjectures).\n\t2.\tProver – Attempts to prove the generated conjectures along with existing theorems.\n\nKey Steps of STP:\n\t1.\tGenerating Conjectures:\n\t•\tGiven a known theorem and proof, the conjecturer synthesizes new conjectures that are barely provable \n\t2.\tProving Conjectures and Theorems:\n\t•\tThe prover attempts to prove both newly generated conjectures and existing unproven theorems from a dataset (successful ones are added to the dataset)\n\t3.\tTraining with Dense Signals:\n\t•\tThe prover is fine-tuned on successful proofs.\n\t•\tThe conjecturer is updated based on which conjectures led to useful proofs.\n\t4.\tGoto 1.\n\nThe method is very intuitive and reasonable. Its main design is unsurprising; the value lies in proposing implementation details. These details feel correct and valid; at the same time, they are somewhat arbitrary and not well justified or motivated. I'd love to see more ablations! (I totally understand that the cost is quite high, though). \n\nI find the evaluation criteria perhaps the weakest point of the paper. My criticism is as follows:\n- Fig 2 - I am not sure how strong the baselines are (and how much effort has been given into tuning them)\n- Fig 3 - I find comparisons with Deepseek-Prover not quite informative without careful information on the training budget of the two methods (and any detail to ensure an apple-2-apple comparison)\n- Table 1 - the same as above. Moreover, I am not sure what the difference is between the Sample budget (#proofs) and sample budgets (#steps).\n- another subtle issue about the comparison of STP and deepseek is how much the presented method 'overfits' to benchmarks. Following that, I'd love to see a deep analysis of the generalization properties (although doing this properly might be another paper)\n\nHaving said that, I stress that I am not an expert in the field. It's hard for me to full understand the results and used benchmarks.", "theoretical_claims": "The paper does not contain any significant theoretical claims.", "experimental_designs_or_analyses": "Correct", "relation_to_broader_scientific_literature": "I am not an expert in the field. The related work covers most of the essential topics.", "essential_references_not_discussed": "In the RL parlance, the presented work can be framed as an exploration problem and curriculum construction. I find it strange not to include a short discussion about these topics. I do not insist on going deep.", "other_strengths_and_weaknesses": "see above", "other_comments_or_suggestions": "see above", "questions_for_authors": "I'd love to see what is the limit of the method. Does it plateau, when, why?", "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": "mcmo6ePmBV", "reviewer": "Reviewer_76YT", "summary": "This paper introduces STP, a self-playing training framework for automated theorem proving. STP employs a conjecturer to generate new conjectures based on existing theorems and lemmas, while a prover attempts to prove previously unproven conjectures or statements in an iterative process. Experiments on the LeanworkBook and miniF2F benchmarks show that STP is more sample-efficient than expert iteration and reinforcement learning, achieving state-of-the-art performance on both datasets across the Lean and Isabelle proof assistants.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank reviewer 76YT for their positive review, and for noting “the paper is well-motivated and well-written, with comprehensive experiments”. \n\n> I think the following work is not currently discussed in the paper: [1],\n\nThank you for the comments. We will include a discussion about [1] upon revision.\n\n[1] MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data\n\n> the training dataset design for SFT-conjecture data does not seem to explicitly encourage the conjecturer to generate harder theorems. [...]\n\nThe conjecture dataset at the SFT stage only serves as an initialization, and we encourage the conjecturer to generate harder conjectures in STP’s iterative training — at every iteration, the conjecturer is continuously trained on previously generated conjectures on which the prover has a *low pass rate*. Therefore, as the prover gets better, the training data of the conjecturer will encourage harder conjectures at the next iteration.\n\n> Minor: In the paper, the authors state that ''RL’s capability is fundamentally bounded by the difficulty level of the theorems in the training dataset [...]''. However, I don't think the proposed STP can truly address such a distribution shift problem, as the conjecturer primarily generates variants of existing theorems and remains heavily reliant on the training dataset.\n\nThanks for the comments! We agree with the reviewer that the STP at its current form is unlikely to discover fundamentally novel proof techniques, and we do not claim that STP truly addresses this particular issue. This paragraph serves as a high-level motivation and STP is only a first step toward this direction (more promising than the standard RL baseline). Moreover, even though STP primarily generated variants of existing theorems, it does discover some new interesting ones, at least *harder* forms of existing theorems. We also only trained with limited compute and data, and the full potential of this line of ideas still requires more future work.\n\n> what is the accuracy of STP after the SFT stage? Additionally, what is the accuracy of STP after self-play training without retraining?\n\nWe thank the reviewer for their comments. The SFT checkpoint is not very different from the base model (DeepSeek-Prover-V1.5-SFT):\n\n| Method         | Sample budget | miniF2F-test | ProofNet-test |\n|----------------|---------------|--------------|---------------|\n| SFT checkpoint | 1             | 35.7%        | 3.8%          |\n|                | 128           | 51.4%        | 15.4%         |\n|                | 3200          | 55.7%        | 19.4%         |\n| STP            | 1             | 41.1%        | 5.9%          |\n|                | 128           | 57.2%        | 18.0%         |\n|                | 3200          | 61.1%        | 23.1%         |\n\n\nAnd STP is better than STP w/o retraining. In general, STP w/o retraining has a higher pass@1 but lower pass@k for large k. \n\n| Method             | Sample budget | miniF2F-test | ProofNet-test |\n|--------------------|---------------|--------------|---------------|\n| STP w/o retraining | 1             | 45.1%        | 7.8%          |\n|                    | 128           | 57.2%        | 16.9%         |\n|                    | 3200          | 60.7%        | 21.5%         |\n| STP                | 1             | 41.1%        | 5.9%          |\n|                    | 128           | 57.2%        | 18.0%         |\n|                    | 3200          | 61.1%        | 23.1%         |\n\nWe will include these results upon revision.\n\n> Furthermore, could you provide more examples of how STP generates variants of existing theorems? Does the conjecturer primarily produce slight variations of input theorems, or can it genuinely generalize to harder problems? It would be valuable to conduct a small analysis comparing the difficulty of the generated conjectures to the original theorems\n\nThe conjecturer generates both variants and more challenging problems. On average, the proof length of the conjectures is 1.98 times that of the seed statements, implying they are generally more difficult to prove. As an example, the following conjecture involves the square root function, where the seed theorem is about polynomials:\n\nSeed theorem\n```\ntheorem lean_workbook_plus_36664 (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : (1 + a^2) * (1 + b^2) = 4) : a + b + a * b ≤ 3\n```\nConjecture\n```\ntheorem lean_workbook_plus_36684 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hab : a * b * c = 1) :   Real.sqrt ((a ^ 2 + 1) / b) + Real.sqrt ((b ^ 2 + 1) / c) + Real.sqrt ((c ^ 2 + 1) / a) ≥ 3 / (a + b + c)\n```\n\nOr the generated conjectures can have very different proofs:\n\nSeed theorem\n```\ntheorem lean_workbook_plus_12215 : sin (π / 2) = 1\n```\nConjecture\n```\ntheorem lean_workbook_plus_60  : ¬(∀ f : ℝ → ℝ , (∀ x :ℝ, f (x + π / 2) = f x - 1) ↔ f = fun x ↦ cos x)\n```", "claims_and_evidence": "Most claims in the submission are well-supported by evidence.", "methods_and_evaluation_criteria": "I think the proposed methods and evaluation criteria are well-motivated and logically sound.", "theoretical_claims": "N/A", "experimental_designs_or_analyses": "I think most of the experiment designs and analyses make sense.", "relation_to_broader_scientific_literature": "I think the key contribution of this paper is the conjecturer, which can generate new, potentially provable training data, helping to mitigate data scarcity and the sparse reward problem in formal theorem proving. This idea is very similar to some approaches in general reasoning tasks (e.g., [1,2]), which also leverage LLM-based rewriting or permutation methods to generate variant training data.\n\n[1] MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Models\n\n[2] WizardMath: Empowering Mathematical Reasoning for Large Language Models via Reinforced Evol-Instruct", "essential_references_not_discussed": "Besides the above references, I think the following work is not currently discussed in the paper: [1], which proposes generating theorems and proofs from seed concepts. Moreover, I believe the discussion of [2] is not entirely fair, as it focuses on a more challenging setting where unpretrained LLMs generate harder conjectures than those in the training set, thereby avoiding data contamination issues. In contrast, STP in this paper fully leverages an LLM to generate variants of existing theorems rather than entirely harder conjectures.\n\n[1] MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data\n\n[2] Learning Formal Mathematics From Intrinsic Motivation", "other_strengths_and_weaknesses": "I think the paper is well-motivated and well-written, with comprehensive experiments. I also appreciate the demonstrated examples, which show that the conjecturer can indeed generate more generalized—and potentially harder—problems given input theorems and lemmas. Additionally, I find the design of reward assignments and filtering strategies well thought out, all of which make sense to me.\n\nOne major concern I have is that the training dataset design for SFT-conjecture data does not seem to explicitly encourage the conjecturer to generate harder theorems. Instead, it appears to primarily promote the generation of variants of existing theorems, given that theorem X and theorem Y originate from the same proof file. There is no guarantee that the conjecturer will propose genuinely harder conjectures, as its design relies entirely on the diverse sampling capabilities of LLMs.", "other_comments_or_suggestions": "Minor: In the paper, the authors state that ''RL’s capability is fundamentally bounded by the difficulty level of the theorems in the training dataset—it is unlikely, in principle, for a model to learn college-level proof techniques solely by working on high school-level problems or to solve open math problems using RL on graduate-level problems''. However, I don't think the proposed STP can truly address such a distribution shift problem, as the conjecturer primarily generates variants of existing theorems and remains heavily reliant on the training dataset.", "questions_for_authors": "Could the paper include more ablation studies? Specifically, what is the accuracy of STP after the SFT stage? Additionally, what is the accuracy of STP after self-play training without retraining?\n\nFurthermore, could you provide more examples of how STP generates variants of existing theorems? Does the conjecturer primarily produce slight variations of input theorems, or can it genuinely generalize to harder problems? It would be valuable to conduct a small analysis comparing the difficulty of the generated conjectures to the original theorems to better understand STP’s ability to propose more challenging problems", "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:

Meta-review: The paper presents a new theorem-proving system called the "Self-Play Theorem-Prover." The system consists of two modules -- the Conjecturer and the Prover -- that repeatedly interact with each other. The Conjecturer is trained on previously generated conjectures that were found hard to prove. The Prover tries to prove these conjectures using standard expert iteration. The system is shown to lead to SOTA performance on several established benchmarks.

The reviewers were all supportive of the paper. While the overall approach is similar to the existing Minimo system, this paper is the first to scale the ideas to Lean, and the problem it studies is one of the central open challenges in AI-for-maths. Given this, I am recommending acceptance. Please incorporate the reviewers' feedback carefully in the final version.
Decision: Accept (poster)