Alchemy: Amplifying Theorem-Proving Capability Through Symbolic Mutation
Under review as a conference paper at ICLR 2025

ALCHEMY: AMPLIFYING THEOREM-PROVING CAPA-
BILITY THROUGH SYMBOLIC MUTATION

Anonymous authors
Paper under double-blind review

ABSTRACT

Formal proofs are challenging to write even for experienced experts. Recent
progress in Neural Theorem Proving (NTP) shows promise in expediting this pro-
cess. However, the formal corpora available on the Internet are limited compared
to the general text, posing a significant data scarcity challenge for NTP. To ad-
dress this issue, this work proposes Alchemy, a general framework for data syn-
thesis that constructs formal theorems through symbolic mutation. Specifically,
for each candidate theorem in Mathlib, we identify all invocable theorems that
can be used to rewrite or apply to it. Subsequently, we mutate the candidate the-
orem by replacing the corresponding term in the statement with its equivalent
form or antecedent. As a result, our method increases the number of theorems
in Mathlib by an order of magnitude, from 110k to 6M. Furthermore, we per-
form continual pretraining and supervised finetuning on this augmented corpus
for large language models. Experimental results demonstrate the effectiveness of
our approach, achieving a 5% absolute performance improvement on Leandojo
benchmark. Additionally, our synthetic data achieve a 2.5% absolute performance
gain on the out-of-distribution miniF2F benchmark. To provide further insights,
we conduct a comprehensive analysis of synthetic data composition and the train-
ing paradigm, offering valuable guidance for developing a strong theorem prover.

1

INTRODUCTION

Nowadays, some pioneer mathematicians are attempting to verify their proofs using the proof as-
sistant Lean (de Moura et al., 2015; Tao, 2023). Writing proofs for formal statements demands
mastery of formal language and domain-specific mathematical knowledge. To mitigate the com-
plexity associated with completing proofs, several research efforts (Polu & Sutskever, 2020; Polu
et al., 2023; Trinh et al., 2024) seek to automatically generate formalized proof through a neural
model, known as Neural Theorem Proving (NTP). NTP represents a long-standing challenge for
machine learning-based methods (Li et al., 2024), highlighting the limitations in the reasoning abil-
ities of neural models. Prevalent Large Language Models (LLMs) (Brown et al., 2020; Dubey et al.,
2024) still struggle with theorem-proving, despite excelling in related reasoning-intensive scenarios
such as math reasoning (Reid et al., 2024) or code generation (Guo et al., 2024).

The key challenge of theorem-proving lies in data scarcity (Li et al., 2024; Trinh et al., 2024). Due
to the difficulties associated with the manual formalization of theorems, formal corpora available on
the Internet are relatively scarce compared to the general text (Azerbayev et al., 2023). Synthetic
data has shown promise in alleviating the data scarcity problem. Some works propose to directly
create theorems in symbolic space. For instance, Wang & Deng (2020) attempts to train a neural
theorem generator on human-written formal theorems for the low-weighted formal system Meta-
math. Other efforts focus on generating theorems based on symbolic rules (Wu et al., 2021; Trinh
et al., 2024), which are restricted to a specific domain of mathematics, such as inequality theorems
and 2D geometry. Additionally, there are endeavors focused on autoformalization (Xin et al., 2024;
Ying et al., 2024), which typically translates natural language mathematical problems into formal-
ized statements, samples correct proofs, and retrains the theorem prover iteratively. Autoformal-
ization has yielded promising results in competition-level theorem-proving tasks through the use of
large autoformalized datasets. However, the process of formalizing problems and retrieving proofs
is labor-intensive and cost-prohibitive. The distribution of formalized theorems is constrained by
the pool of human-collected natural language problems and the intrinsic capabilities of the model.

1

000
001

002
003
004
005
006
007

008
009
010
011
012
013

014
015
016
017
018

019
020
021
022
023
024

025
026
027
028
029
030

031
032
033
034
035
036

037
038
039
040
041

042
043
044
045
046
047

048
049
050
051
052
053

Under review as a conference paper at ICLR 2025

054
055

056
057
058
059
060
061

062
063
064
065
066
067

068
069
070
071
072

073
074
075
076
077
078

079
080
081
082
083
084

085
086
087
088
089
090

091
092
093
094
095

096
097
098
099
100
101

102
103
104
105
106
107

Compared to autoformalization, synthesizing theorems in symbolic space is a more direct process
without intermediate translation, and is also easier to scale up to large, cost-effective CPU units.

Building upon the advanced Lean theorem prover, we introduce a general method that synthesizes
theorems directly in symbolic space. We analogize theorem synthesis to constructing functions in
general programming language and adopt an up-to-down approach. Initially, a new statement (func-
tion declaration) is constructed for each candidate theorem. Specifically, with the mathematical
library of Lean Mathlib41 as seed data, we aim to find a symbolic manipulation Φ between two
existing statements. We posit that Lean’s tactics serve as suitable candidates for manipulation Φ
because of their efficacy in handling symbolic expressions. {rw, apply} are basic tactics frequently
used in theorem proving and capable of handling the equality and implication relationship between
terms. We assign both tactics to the set of manipulations Φ and retrieve the invocable theorems for
each candidate theorem by executing a predefined list of instructions in an interactive Lean environ-
ment. Then we mutate the candidate statement by replacing its components with their corresponding
equivalent forms or logical antecedents. Ultimately, we construct the corresponding proof (function
body) based on the existing proof and verify its correctness using Lean. The worked example shown
in Fig 1 illustrates the entire procedure of our algorithm. This algorithm is executed on a large CPU-
only computing unit for several days. Our method increases the number of theorems in Mathlib
by an order of magnitude from 110,657 to 6,326,679. This significant increase in the number of
theorems demonstrates the potential of creating theorems in symbolic space.

We pre-train the LLMs on the combination of Mathlib theorems and their mutated variants. Then
we fine-tune the models on the extracted state-tactic pairs, composing both the training split of
Mathlib and additional synthesized state-tactic pairs. We demonstrate the effectiveness of our
method by evaluating the theorem-proving capability of these provers on the challenging Lean-
dojo benchmark. Our synthetic data improve the performance by around 5% (over 70 theorems) on
the novel premises split. Furthermore, the synthesized data exhibit promise in enhancing the out-
of-distribution theorem-proving ability of LLMs, as evidenced by a performance increase of about
2.5% on the competition-level miniF2F benchmark.

Our main contributions are as follows. 1) To the best of our knowledge, this work represents the
first general data synthesis framework in the symbolic space for the Lean theorem prover, effectively
complementing mainstream autoformalization-based methods. Notably, our synthesis pipeline in-
creases the number of theorems in Mathlib4 by an order of magnitude. 2) The synthesized data
and associated code will be made open-source to facilitate further research in data synthesis for
formal systems. Also, the synthesized theorems can serve as a valuable supplement to Mathlib. 3)
We conduct a comprehensive evaluation on both in-distribution and out-of-distribution benchmarks,
providing empirical insights to enhance the theorem-proving capabilities of LLMs.

2 RELATED WORK

Neural Theorem Proving Proof assistants such as Lean (de Moura et al., 2015), Isabelle (Paulson,
1994) or Coq (Barras et al., 1997) are gaining traction within the mathematical community. These
tools help mathematicians in interactively formalizing and checking the correctness of proofs (Tao,
2024). Neural networks have shown promise in lowering the barrier of using a specific formal
language for mathematicians, serving as a copilot (Song et al., 2024; Welleck & Saha, 2023). Polu
& Sutskever (2020) propose to prove theorems automatically by training a decoder-only transformer
to predict the next proofstep and construct the entire proof through a predefined search tragedy. Then
a series of works seek to enhance the efficiency of this framework by incorporating auxiliary training
objectives (Han et al., 2022), conducting reinforcement learning (Polu et al., 2023; Xin et al., 2024),
improving proof search tragedy (Lample et al., 2022; Wang et al., 2023; Xin et al., 2024), refining
the premise-selection (Mikula et al., 2023; Yang et al., 2023) and so on. Our work follows the
framework proposed by Polu & Sutskever (2020), using proofstep prediction as the objective and
best-first-search as the search tragedy.

Synthetic Theorem Creation Data scarcity is a main challenge for NTP (Li et al., 2024). Syn-
thetic data can effectively alleviate this problem alongside manual data collection (Wu et al., 2024).

1https://github.com/leanprover-community/mathlib4

2

Under review as a conference paper at ICLR 2025

108
109

110
111
112
113
114
115

116
117
118
119
120
121

122
123
124
125
126

127
128
129
130
131
132

133
134
135
136
137
138

139
140
141
142
143
144

145
146
147
148
149

150
151
152
153
154
155

156
157
158
159
160
161

Figure 1: The overview of our synthesis pipeline. At the theorem level, we find invocable theorems
that can be used to rewrite or apply to the assumptions or assertion of the candidate statement,
such as the iff and implication rules about the Coprime. Then, we construct the new statements by
replacing the specific component with its equivalent form or antecedent. At the proof tree level, our
method merges two existing proof trees.

The current approach for synthesizing theorems diverges into two pathways. For autoformalization-
based methods, the prevalent statement-level autoformalization is to translate a set of natural lan-
guage problems into formal statements, followed by expert iteration to sample a collection of proofs
for these statements (Wu et al., 2022; Xin et al., 2024; Ying et al., 2024). The proof-level autofor-
malization (Jiang et al., 2023; Huang et al., 2024) leverages LLM to generate a proof sketch, which
is completed by symbolic engines such as Sledgehammer (B¨ohme & Nipkow, 2010). In contrast, the
second pathway focuses on synthesizing theorems in formal space. Wang & Deng (2020) propose to
train a neural theorem generator to synthesize theorems on a low-weight formal system, Metamath
(Megill & Wheeler, 2019) which has only one tactic substitute. Wu et al. (2021) sequentially edits
the seed expression according to a predefined set of axioms and an axiom order to create a new
statement, concatenating the implications from all steps to build a complete proof. This method is
used to create theorems on domains grounded in well-established axioms, such as inequality theo-
rems and ring algebra (Polu & Sutskever, 2020). Beyond these works, AlphaGeometry (Trinh et al.,
2024) can solve olympiad geometry without human demonstrations by constructing statements and
proofs in symbolic space from scratch, using a carefully designed deduction engine and large-scale
computing resources. Our method aims to directly synthesize theorems in symbolic space on the
advanced Lean theorem prover, fully utilizing the power of computing.

Benchmarks for Theorem Proving Most neural theorem provers based on Lean are primarily
trained on Lean’s mathematical library, Mathlib. It encompasses a broad spectrum of mathematical
subjects (e.g., algebra and analysis), composed of over 120,000 theorems along with their respective
axioms and definitions. Researchers test the capability of neural models to prove in-distribution
theorems on a held-out set of Mathlib (Polu & Sutskever, 2020; Han et al., 2022; Polu et al., 2023).

3

Find Invocable TheoremsFormal Knowledge BaseMathlib/Algebra/IsPrimePow.leantheorem Nat.disjoint_divisors_filter_isPrimePow  {a b : ℕ} (hab : a.Coprime b) :  Disjoint (a.divisors.filter IsPrimePow) (b.divisors.filter IsPrimePow) := by    simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]    rintro n han _ha hn hbn _hb -    exact hn.ne_one (Nat.eq_one_of_dvd_coprimes hab han hbn)NL description: If two natural numbersaandbare coprime, then the sets of prime power divisors ofaandbare disjoint. Equality:theorem coprime_iff_isRelPrime {m n : ℕ} : m.Coprime n  IsRelPrime m n := by …NL description: For two natural numbers m and n, the property of being coprime is equivalent to the property of being relatively prime.Implication:theorem coprime_of_mul_modEq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) : a.Coprime n := by …NL description: If there exist natural numbers a, b, and n, such that the product a * b is congruent to 1 modulo n, then a and n are coprime.Construct new theoremsEquality-Variant:example {a b : ℕ} (hab : IsRelPrime a b) :  Disjoint (a.divisors.filter IsPrimePow) (b.divisors.filter IsPrimePow) := by     have hab : a.Coprime b := by rw [←Nat.coprime_iff_isRelPrime] at hab ; exact hab      …Implication-Variantexample {a b : ℕ} (c : ℕ) (h : a * c ≡ 1 [MOD b]) :  Disjoint (a.divisors.filter IsPrimePow) (b.divisors.filter IsPrimePow):= by     have hab : a.Coprime b := by apply Nat.coprime_of_mul_modEq_one <;> assumption        ...Simplified Proof Tree⊢a b : ℕa.Coprime ba.Coprime bIsRelPrime a b a.Coprime ba * c ≡ 1 [MOD b])c : ℕ ⊢a b : ℕa.Coprime bIsRelPrime a b ⊢a b : ℕa.Coprime ba * c ≡ 1 [MOD b])c : ℕ EqualityImplicationVariants of Original TheoremUnder review as a conference paper at ICLR 2025

162
163

164
165
166
167
168
169

170
171
172
173
174
175

176
177
178
179
180

181
182
183
184
185
186

187
188
189
190
191
192

193
194
195
196
197
198

199
200
201
202
203

204
205
206
207
208
209

210
211
212
213
214
215

Yang et al. (2023) creates a challenging data split of Mathlib (novel premise split) which requires
testing proofs to use at least one premises not seen in the training stage and mitigates the over-
estimated phenomena in the traditional setting of evaluation (random split). Another widely-used
benchmark, miniF2F, (Zheng et al., 2022) is a cross-system benchmark and includes competition-
level problems as well as IMO-level problems in the domain of algebra and number theory.

3 METHOD

Theorems written in Lean can be viewed as a special form of code, where declarations and func-
tion bodies possess precise mathematical meanings. The initial step in creating a new theorem
involves formulating a theorem statement (function declaration) that defines the essence of the theo-
rem. Then, one must verify its correctness by generating a proof block (function body) and submit-
ting it to the proof assistant for validation. The resulting theorems that pass type checking can serve
as supplementary data for training a neural theorem prover.

3.1 STATEMENT GENERATION

Find invocable theorems Constructing a new statement is the first step in creating a Lean theo-
rem. The candidate theorem t has a statement denoted as s. In the corresponding Lean repository,
there exists a set of potentially invocable theorems Tp = {ti}N
i=0. We assume that the challenge
in creating a new theorem involves effectively leveraging the possibly invocable theorem ti to mu-
tate the candidate statement s. This understanding arises from two perspectives. Each theorem in
Lean can be represented in the form of a proof tree as presented in Fig 1. The leaf nodes rep-
resent the assumptions, and the root node signifies the assertion. At the tree level, the task of
generating a new Lean theorem with existing theorems is equivalent to defining operations Φ that
combine the proof trees of ti and t. To streamline this process, our focus is solely on establishing
the connection between the root node of ti and the leaf node (or root node) of the candidate the-
orem t. From a mathematical standpoint, we can transform a target formula into an equal variant
or break it down into multiple subformulas that suffice to prove the original formula, by employing
the equality or “only if” relationship between formulas. The mathematical interconnections be-
tween formulas provide heuristic insights on how to mutate s to create a new theorem. Similarly,
we can substitute the terms in s with their equivalent forms or logical antecedents. For instance,
consider the statement a + b > c + d, m > 0 → m(a + b) > m(c + d) and the known theorems
a > b ⇐⇒ ea > eb and a > c, b > d =⇒ a+b > c+d. From these, we can derive new theorems:
a + b > c + d, m > 0 → em(a+b) > em(c+d), and a > c, b > d, m > 0 =⇒ m(a + b) > m(c + d).
In summary, identifying operations Φ that use ti to modify the assumptions or assertion of s is the
primary step in constructing new statements.

With their intrinsic mathematical meanings and proficiency in manipulating terms within Lean, tac-
tics are promising candidates for the operations Φ. Following the preceding discussion, we choose
two frequently used basic tactics, rw and apply to formulate Φ.

• rw The “rewriting” tactic rw is mostly used to replace some terms in the target expression
with their equivalent forms according to the given identity or iff (a.k.a., if and only if)
rules2. In the presence of an identity h : a = b or an iff rule h : P ⇐⇒ Q, rw [h]
substitutes all occurrences of term on the left side of equality in the proof goal with term
on the right side. The direction of substitution can be reversed by adding a back arrow in
the bracket (rw [← h]). The target of rewriting can also be changed using at, e.g. rw [h] at
h1, where h1 is an arbitrary assumption of the current proof state.

• apply The apply tactic is a “suffice-to” tactic. Given an implication, it will match the
consequent with the proof goal. If matched, it will transform the goal into the antecedent
of the implication. With an implication rule h : P =⇒ Q and a proof goal Q, then apply
[h] will reduce the goal to proving P , which means that “proving P suffices to prove Q
by implication”. Similarly, apply can be used to modify the assumption by deducing the
implication forward. With assumption h1 : P , then apply [h] at h1 will change h1 into Q,
which means “If P is true, then we can assert Q is true by the implication”.

2Strictly speaking, the rw tactic is used to handling equality in Lean, the identity and iff are just some kinds

of equality.

4

Under review as a conference paper at ICLR 2025

216
217

218
219
220
221
222
223

224
225
226
227
228
229

230
231
232
233
234

235
236
237
238
239
240

241
242
243
244
245
246

247
248
249
250
251
252

253
254
255
256
257

258
259
260
261
262
263

264
265
266
267
268
269

Algorithm 1 Find invocable theorems

Input: candidate statement s, potential invocable theorems Tp, instruction templates I
Output: invocable theorems Ti
(env, init state) ← INIT(s)
Ti ← ∅
for t in Tp do

▷ Ti : {(init state, next state, instruction) · · · }
▷ initialize gym-like environment and retrieve initial state

for i in I do

▷ for each instruction template

instruction inst ← FORMAT(t, i)
next state ← RUN TAC(env, init state, inst)

▷ run a tactic specified by instruction i

and theorem t

if VALID(next state) then

Add (init state, next state, inst) to Ti

▷ if return a valid proof state

end if

end for

end for

Table 1: Templates for instructions designed to be executed in a Lean environment. We determine
if a theorem is invocable by running the specific instruction.

Tactic

Instruction Template

Description

Equality invocable theorem : a = b or a ⇐⇒ b

rw

apply

rw [invocable theorem]
rw [←invocable theorem]
rw [invocable theorem] at assumption
rw [←invocable theorem] at assumption

replace all as in goal with b
replace all bs in goal with a
replace all as in assumption with b
replace all bs in assumption with a

Implication invocable theorem : a =⇒ b

have assumption := by apply invocable theorem

set assumption as current proof
goal, and try to argue backwards

To generate a new statement, we need to find the relationship between the candidate statement s and
the potentially invocable theorems Tp. The pseudocode outlined in Algorithm 1 describes the main
procedure to find invocable theorems. The process involves initializing a gym-like environment
to interact with Lean and extracting the initial proof state for the candidate statement. Then, the
algorithm iteratively tests whether one theorem can be used to rewrite or apply to the candidate
theorem leveraging the instruction templates shown in Table 1. Suppose the feedback from the
interactive environment is deemed valid according to predefined criteria, the algorithm adds the
proof states before and after the tactic running together with the respective instruction to the set of
invocable theorems Ti. More information about this process is described in Appendix C.2.

Mutate statements After obtaining the initial set of invocable theorems, we applied some filtering
rules to Ti to improve the quality of the data and lower the complexity of mutating statements. With
filtered invocable theorems Ti, we construct new statements by replacing the components with their
equivalent forms or antecedents. Since we use tactics in Lean to formulate the operations Φ, most
symbolic manipulations are bypassed to the Lean proof assistant. What remains is just parsing and
replacing. Specifically, for the candidate statement s and instruction i, we utilize its abstract syntax
tree to pinpoint the exact location within the code that requires modification. Then we replace the
corresponding parts with mutants parsing from the subsequent proof state generated by the execution
of a specific tactic. The details of our algorithm and helpful source code are described in C.3.

3.2 PROOF GENERATION AND THEOREM VERIFICATION

Mutated statements can serve as useful lemmas for theorem-proving only if we can construct proofs
that pass the verification of the proof assistant. We construct the entire proof using symbolic rules.
Although neural provers and other automated theorem proving (ATP) tools (e.g., hammer) can gen-
erate more natural and diverse proofs than rule-based methods, they are compute-intensive and do

5

Under review as a conference paper at ICLR 2025

not guarantee the correctness of the generated proofs. The idea of building a proof block is intuitive.
Given that we only make a one-step modification to the statement, transforming the original proof
state to a mutated proof state, a logical approach is to reverse the mutation and utilize the original
proof to complete the remaining proving process. We use have tactic to restore the modified part of
a statement (the original assumption or assertion) by introducing a lemma.

• have The have tactic enables users to introduce new assumption into the current proof state
if they can prove it. Given an assumption h1 : P and an implication rule h2 : P =⇒ Q,
a new assumption h : Q can be added by have h: Q := by apply h2 at h1; exact h1. This
tactic is usually used to introduce helpful lemmas when proving a theorem.

In addition to its ability to introduce new assumptions into the proof state, have can be used in both
tactic-style proof and term-style proof, which enlarges the margin for theorems to which our method
can be applied. Apart from this, the additional have instruction transforms the mutated complex
proof state into a canonical proof state. To some extent, this transformation is analogous to con-
structing an auxiliary point in geometry problems, which we assume will be beneficial for theorem
proving in the general domain. Subsequently, we combine the original proof with this lemma to
build the proof for the new statement. The details of the implementation of proof generation are
depicted in the Appendix C.3. We construct the proof block for each mutated theorem. Then we
submit the synthesized theorems to the Lean theorem prover for verification and remove the wrong
ones. Details of the verification process are provided in Appendix C.4. Finally, we obtain a set of
variants V = {vi}n

i=0 defined by the keyword “example” for each candidate theorem.

3.3 MODEL TRAINING

Regarding the synthetic data, we have two observations. At the theorem level, the synthetic data
comprises numerous theorems, each with statement distinct from existing theorems. At the state-
tactic level, the process of constructing proofs introduces additional state-tactic pairs, primarily
centered on rw and apply. Based on these insights, we assume that the synthetic data can serve as
an augmented corpus for continual pretraining and supervised finetuning. Specifically, we fine-tune
LLMs using the proofstep prediction objective proposed by Polu & Sutskever (2020), utilizing state-
tactic pairs derived from both seed theorems and synthetic theorems. Given the current proof state,
the model is required to predict the next tactic sequence that contributes to the proving of the target
theorem. We utilize the prompt template used by Welleck (2023), as shown in Fig.2.

Figure 2: Prompt template

4 EXPERIMENTS

We implement the data-synthesis pipeline described in Section 3 for rw and apply, constructing a
set of variants for each candidate theorem in Mathlib. We train the LLMs on a mixture of human-
written theorems and synthetic ones. To examine the effectiveness of synthetic data, we evaluate the
theorem prover on two benchmarks that are widely adopted by the research community: 1) Test split
of Mathlib, which shares the same distributional characteristics as the seed theorems; 2) miniF2F, a
challenging benchmark focusing on competition-level problems that exhibits a distinct distribution

6

270
271

272
273
274
275
276
277

278
279
280
281
282
283

284
285
286
287
288

289
290
291
292
293
294

295
296
297
298
299
300

301
302
303
304
305
306

307
308
309
310
311

312
313
314
315
316
317

318
319
320
321
322
323

/- You are proving a theorem in Lean 4.You are given the following information:  - The current proof state, inside [STATE]...[/STATE]Your task is to generate the next tactic in the proof. Put the next tactic inside [TAC]...[/TAC] -/[STATE]{state}[/STATE][TAC]Under review as a conference paper at ICLR 2025

324
325

326
327
328
329
330
331

332
333
334
335
336
337

338
339
340
341
342

343
344
345
346
347
348

349
350
351
352
353
354

355
356
357
358
359
360

361
362
363
364
365

366
367
368
369
370
371

372
373
374
375
376
377

compared to seed data. The experimental results derived from both benchmarks demonstrate the
potential efficacy of our approach.

4.1

IMPLEMENTATION DETAILS

Data-Synthesis We choose Mathlib43 which contains 116,695 theorems as the seed data for data-
synthesis. Our synthesis pipeline is built upon Leandojo4 (Yang et al., 2023), a Python module that
enables tracing a specific Lean repository, extracting the state-tactic pairs and abstract syntax trees
(ASTs), and interacting with the Lean environment5 (run tac API). Finding invocable theorems is
the most time-consuming step of our pipeline. For rw, the time overhead amounts to 14 days using
4,096 CPU cores6. For apply, it takes 7 days at this stage using 2,048 CPU cores with a one-hour
timeout for each theorem. The substantial time cost is attributed to the O(n2) complexity of our
algorithm and the memory-intensive characteristics of Leandojo. We believe this overhead could be
greatly reduced through a more meticulous implementation. After retrieving the invocable theorems,
we construct new statements and proofs for the target theorems in approximately an hour using 24
CPU cores. We then write back the mutated theorems and compile the enlarged repository through
lake build, utilizing 2,048 CPU cores. We retrieve the error messages returned by Lean, which
can be parsed to locate the wrong theorems. Finally, we trace the enlarged repository on a 96-core
machine for 3 days, obtaining the additional state-tactic pairs by parsing the AST of each file.

Model Training We select Llama-3-8B (Dubey et al., 2024) and deepseek-coder-base-v1.5- 7B
(Guo et al., 2024) as our base models. We conduct continual pretraining with the next-token predic-
tion objective for one epoch. Then we fine-tune the models with the proofstep prediction objective
(Polu & Sutskever, 2020) for two epochs. All experiments are conducted on 8 × H100 GPUS. We
employ a linear learning rate scheduler with a 3% warm-up period and a maximum learning rate of
2e-5. We set the global batch size to 256 and the cutoff length to 2,048. All models are trained using
Deepspeed ZeRO Stage3 (Rajbhandari et al., 2021) and Flash-Attention 2 (Dao, 2023). We utilize
the open-sourced codebase Llama-Factory (Zheng et al., 2024) for all training experiments.

Evaluation We follow the evaluation setting used in Azerbayev et al. (2023). We use the fre-
quently used best-first-search as our search tragedy and set a 10-minute timeout. The search budget
can be represented as N × S × T , where N denotes the number of attempts, S denotes the number
of generated tactics per iteration, and T denotes the maximum number of generations. Following
Azerbayev et al. (2023), we set N = 1, S = 32 and T = 100. Our evaluation script is modified from
an open-source implementation (Welleck, 2023) which is based on vLLM (Kwon et al., 2023) and
Leandojo (Yang et al., 2023). We utilize Leandojo Benchmark (Yang et al., 2023) which contains
2,000 theorems as the test split of Mathlib4 and report the results on both the random split and the
novel premises split. We remove the subsets of theorems for both splits that can not be initialized
by Leandojo. There remain 1,929 theorems in random split and 1,659 theorems in novel premises
split. We upgrade the tool-chain version of miniF2F (Zheng et al., 2022) to v4.6.0 rc1.

4.2 ANALYSIS OF SYNTHETIC DATA

Table 2: Number of theorems. Stage one: the number of invocable instructions for all candidate
theorems. Stage two: the number of theorems that pass the verification of the Lean theorem prover.

Tactic Candidate theorems

Stage one

Stage two Expansion Conversion Ratio

rw
apply

110,657
78,871

5,081,544
9,483,504

2,830,817
3,495,832

×25
×44

56%
37%

We separately run the synthesis pipeline for these two tactics. For rw, we choose Mathlib theorems
as candidate theorems. Additionally, candidate theorems for apply should have at least one explicit

3commit: 2iufd 3c307701fa7e9acbdc0680d7f3b9c9fed9081740
4version: 1.7.1
5lean-toolchain: v4.6.0 rc1
6512 CPU nodes, each node has 8 cores and 56GB RAM

7

Under review as a conference paper at ICLR 2025

assumption. In practice, the synthesis process is divided into two stages. In the first stage, we find
the potential invocable theorems for each candidate theorem by running a specific tactic. In the
second stage, we construct the new theorems and verify their correctness using the Lean theorem
prover. Table 2 shows the number of theorems of different stages. For both tactics, we increase the
number of theorems by an order of magnitude (×25 for rw and ×44 for apply). The conversion ratios
from the potential invocable theorems to the outcomes are primarily determined by the method used
to construct the new statements and proofs. We believe that a finer implementation could greatly
improve the conversion ratio. Figure 3 shows the dynamics of the distribution of mathematical
subjects. The rw tactic increases the percentages of Analysis, Ring Algebra, Number Theory, and so
on. The apply tactic mainly contributes to the fields of Analysis and Topology. Further information
about synthetic data can be found in the Appendix D.

Figure 3: Distribution of mathematical subjects. For each employed tactic, we mix the generated
variants with the original theorems. a) The distribution of Mathlib. b) The distribution of Mathlib +
rw. c) The distribution of Mathlib + apply.

Our method synthesizes a large collection of new theorems utilizing each tactic. Then we combine
them with the theorems in Mathlib as the training data for continual pre-training. Our approach also
introduces new state-tactic pairs during the theorem-construction process. We write the variants to
corresponding lean files and extract additional state-tactic pairs using Leandojo. The synthesized
data are categorized primarily based on the employed tactic, specifically rw and apply. Variants
and their corresponding state-tactic pairs that appear in the test split of the Leandojo benchmark are
removed. Furthermore, the extracted state-tactic pairs are deduplicated according to the invocable
theorem (i.e., premise) used in the tactic instruction. Finally, we obtain about 30k data points for
each tactic. We combine them with the training set of Leandojo (Mathlib-train) that composes over
200k data points to form the SFT dataset. A detailed description of the deduplication process and
training data are presented in the Appendix D.3.

4.3 EXPERIMENTAL RESULTS

4.3.1 MAIN RESULTS

We conduct continual pretraining on the augmented lean corpus. Then we fine-tune the LLMs on
the mixture of Mathlib-train and additional state-tactic pairs. The training data are grouped by the
tactic employed in the additional state-tactic pairs. We evaluate the effectiveness of our method on
the challenging Leandojo benchmark and report results on different mixtures of data. As shown in
Table 3, our synthetic data consistently improve the theorem-proving capabilities of LLMs. Com-
pared with solely finetuning on the training split of Mathlib, data augmentation for a single tactic
demonstrates a beneficial effect on the theorem-proving ability of LLMs. Moreover, the positive
impacts of each tactic can be cumulative. Training on the combination of rw variants and apply
variants results in a significant performance improvement in the challenging novel premises split
of Leandojo benchmark, where the model is required to use at least one new premise to prove the
target theorem (+4.7%, 78 theorems for Llama3-8b; +4.22%, 70 theorems for deepseek-coder-7b-
base-v1.5). Our synthetic data still make a certain improvement on the random split, where the
performance of models is over-estimated by allowing it to prove many theorems through memoriza-

8

378
379

380
381
382
383
384
385

386
387
388
389
390
391

392
393
394
395
396

397
398
399
400
401
402

403
404
405
406
407
408

409
410
411
412
413
414

415
416
417
418
419

420
421
422
423
424
425

426
427
428
429
430
431

a)b)c)Under review as a conference paper at ICLR 2025

Table 3: Results on Mathlib. tidy: a tactic in Mathlib that uses heuristics to complete a proof. We
select the performance of each model solely fine-tuned using Mathlib-train as the main baseline.
Mathlib-train + x: the performance of the model pre-trained and fine-tuned on a mixture of Mathlib-
train and additional data about x.

random

novel premises

Search Budget

Methods

tidy
GPT-4
Reprover (Yang et al., 2023)

w/ retrieval

llmstep (Pythia 2.8b) (Welleck & Saha, 2023)

Llama3-8b

Mathlib-train + rw
Mathlib-train + apply
Mathlib-train + rw + apply

23.8
29.0
47.6
51.2
47.6
50.1

58.22

5.3
7.4
23.2
26.3
-
-

38.52

59.62 (+1.40)
58.84 (+0.62)
59.82 (+1.60)

42.13 (+3.62)
41.29 (+2.77)
43.22 (+4.70)

deepseek-coder-7b-base-v1.5

57.7

39.24

Mathlib-train + rw
Mathlib-train + apply
Mathlib-train + rw + apply

59.25 (+1.55)
58.68 (+0.98)
60.39 (+2.69)

42.98 (+3.74)
40.51 (+1.27)
43.46 (+4.22)

-
1 × 35
1 × 64
1 × 64
1 × 32
2 × 32

1 × 32

1 × 32
1 × 32
1 × 32

1 × 32

1 × 32
1 × 32
1 × 32

tion. In conclusion, the results of the experiment show that simply mutating the seed theorems and
introducing state-tactic pairs of a single tactic can relieve the data scarcity problem and enhance the
theorem-proving ability of LLMs.

4.3.2 EFFECTIVENESS OF CONTINUAL PRETRAINING

Table 4: Effectiveness of continual pre-training. We grouped the
dataset for CPT and SFT by the tactic employed in the additional
state-tactic pairs.

Methods

random

novel premises

random

novel premises

Llama3-8b

deepseek-coder-base-7b-v1.5

sft: mathlib-train

w/o cpt
rw
apply
rw + apply

58.22
59.56 (+1.35)
58.42 (+0.21)
59.72 (+1.50)

38.52
42.56 (+4.04)
41.29 (+2.77)
42.19 (+3.68)

57.70
58.74 (+1.04)
58.58 (+0.88)
59.67 (+1.97)

39.24
40.69 (+1.45)
40.02 (+0.78)
41.65 (+2.41)

sft: mathlib-train + rw

w/o cpt
rw

57.85
59.62 (+1.76)

41.59
42.13 (+0.54)

58.63
59.25 (+0.62)

41.05
42.98 (+1.93)

sft: mathlib-train + apply

w/o cpt
apply

56.71
58.84 (+2.13)

40.02
41.29 (+1.27)

57.96
58.68 (+0.73)

41.17
40.51 (-0.66)

sft: mathlib-train + rw + apply

w/o cpt
rw + apply

58.53
59.82 (+1.30)

41.95
43.22 (+1.27)

58.37
60.39 (+2.02)

42.92
43.46 (+0.54)

Figure 4: Influence of the quantity
of synthesized data points.

To examine the necessity of continual pretraining, we assess and contrast the performance of the
LLM on Leandojo benchmark when the pretraining stage is included versus when it is excluded
from the experimental setup. We use models fine-tuned on various combinations of state-tactic pairs
as our baselines and present the results of pretraining on the augmented corpus. As shown in Table 4,
the continual pretraining stage demonstrates a positive influence on the performance of LLMs across
diverse supervised fine-tuning settings. The experimental results indicate that continual pretraining
before the supervised finetuning stage is also beneficial to the theorem-proving ability of the LLM.

9

432
433

434
435
436
437
438
439

440
441
442
443
444
445

446
447
448
449
450

451
452
453
454
455
456

457
458
459
460
461
462

463
464
465
466
467
468

469
470
471
472
473

474
475
476
477
478
479

480
481
482
483
484
485

rwapplyDownsampleDeduplicateUnder review as a conference paper at ICLR 2025

486
487

488
489
490
491
492
493

494
495
496
497
498
499

500
501
502
503
504

505
506
507
508
509
510

511
512
513
514
515
516

517
518
519
520
521
522

523
524
525
526
527

528
529
530
531
532
533

534
535
536
537
538
539

4.3.3

INFLUENCE OF THE QUANTITY OF SFT DATASET

We deduplicate the synthesized state-tactic pairs of each tactic by the invocable theorem (i.e.,
premise). Then we obtain about 30k data points for each tactic. To examine the influence of the
quantity of the SFT dataset, we compare the performance of Llama-3-8B, trained on different quan-
tities of additional data points, on novel premises split of Leandojo benchmark. As shown in Fig
4, the selected quantity (30k) achieves a relatively optimal compromise between the performance
and overhead. The experimental results also reveal that enlarging the quantity of state-tactic pairs
of a single tactic tends to lead to rapid saturation. We assume that the key to continually improving
the theorem-proving ability lies in keeping the diversity of tactics during the process of scaling the
synthetic data. More details are presented in Appendix D.3.4.

4.3.4 ANALYSIS OF OUT-OF-DISTRIBUTION PERFORMANCE

We evaluate Llama-3-8b using the competition-level theorem proving benchmark miniF2F. As
shown in Table 5, our synthesized data still helps to improve the theorem-proving ability of LLMs
on the out-of-distribution benchmark. The magnitude of this improvement is comparatively smaller
than that observed on the in-distribution benchmark. We attribute this discrepancy to the divergence
between synthesized tactics and the preferred tactics to prove competition-level problems. Through
manual inspection of the correct proofs generated by various LLMs trained on Mathlib-train, we
identify a tendency to favor advanced and automated tactics (e.g., simp, omega, linarith, norm num,
etc.). Additionally, we analyze the distribution of tactics used in proved theorems across different
data compositions and make the following observations. 1) Data augmentation on a single tactic
will increase the model’s preference for the specific tactic. 2) Adjusting the distribution of different
tactics within the dataset is promising to improve the theorem-proving ability of LLMs. The entire
analysis process is illustrated in Appendix E.2.

Table 5: Results on miniF2F. We evaluate the performance across different data compositions and
list the ratio of rw, apply, norm num and linarith used by Llama3-8b to prove these theorems.

Methods

miniF2F-test Correct/Total

rw

apply

norm num linarith

Mathlib-train
Mathlib-train + rw
Mathlib-train + apply
Mathlib-train + rw + apply

34.01
35.24
36.07
36.48 (+2.47)

83/244
86/244
88/244
89/244

16.10
18.75
8.87
12.31

0.00
0.78
2.42
0.77

27.12
14.84
20.16
26.92

16.95
21.88
15.63
16.92

5 CONCLUSION

We have presented a general data-synthesis framework for the Lean theorem prover, which amplifies
the theorem-proving capability of the LLM through symbolic mutation. Our algorithm increases
the number of theorems in Mathlib by an order of magnitude and achieves promising results in
improving the theorem-proving ability of the LLM. We discuss the limitations of our method in
Appendix B. Synthesizing formal theorems is an inherently challenging problem. Our approach,
much like ancient alchemy, involves experimenting with a substantial number of theorems in the
hope of uncovering valuable “gold”. We aspire for our algorithm and data to serve as a foundation
for further research, advancing theorem synthesis from alchemy to chemistry.

REFERENCES

Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Al-
bert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language
model for mathematics. CoRR, abs/2310.10631, 2023. doi: 10.48550/ARXIV.2310.10631. URL
https://doi.org/10.48550/arXiv.2310.10631.

Bruno Barras, Samuel Boutin, Cristina Cornes, Judica¨el Courant, Jean-Christophe Filliatre, Eduardo
Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The Coq proof
assistant reference manual: Version 6.1. PhD thesis, Inria, 1997.

10

Under review as a conference paper at ICLR 2025

540
541

542
543
544
545
546
547

548
549
550
551
552
553

554
555
556
557
558

559
560
561
562
563
564

565
566
567
568
569
570

571
572
573
574
575
576

577
578
579
580
581

582
583
584
585
586
587

588
589
590
591
592
593

Sascha B¨ohme and Tobias Nipkow. Sledgehammer: Judgement day. In J¨urgen Giesl and Reiner
H¨ahnle (eds.), Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edin-
burgh, UK, July 16-19, 2010. Proceedings, volume 6173 of Lecture Notes in Computer Sci-
doi: 10.1007/978-3-642-14203-1\ 9. URL https:
ence, pp. 107–121. Springer, 2010.
//doi.org/10.1007/978-3-642-14203-1_9.

Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal,
Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. Language models are
few-shot learners. Advances in neural information processing systems, 33:1877–1901, 2020.

Tri Dao. Flashattention-2: Faster attention with better parallelism and work partitioning. CoRR,
abs/2307.08691, 2023. doi: 10.48550/ARXIV.2307.08691. URL https://doi.org/10.
48550/arXiv.2307.08691.

Leonardo Mendonc¸a de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von
Raumer. The lean theorem prover (system description).
In Amy P. Felty and Aart Middel-
dorp (eds.), Automated Deduction - CADE-25 - 25th International Conference on Automated
Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in
Computer Science, pp. 378–388. Springer, 2015. doi: 10.1007/978-3-319-21401-6\ 26. URL
https://doi.org/10.1007/978-3-319-21401-6_26.

Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha
Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The llama 3 herd of models.
arXiv preprint arXiv:2407.21783, 2024.

Daya Guo, Qihao Zhu, Dejian Yang, Zhenda Xie, Kai Dong, Wentao Zhang, Guanting Chen, Xiao
Bi, Y. Wu, Y. K. Li, Fuli Luo, Yingfei Xiong, and Wenfeng Liang. Deepseek-coder: When the
large language model meets programming - the rise of code intelligence. CoRR, abs/2401.14196,
2024. doi: 10.48550/ARXIV.2401.14196. URL https://doi.org/10.48550/arXiv.
2401.14196.

Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact
co-training for theorem proving with language models. In The Tenth International Conference on
Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022.
URL https://openreview.net/forum?id=rpxJc9j04U.

Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo
Li, Linqi Song, and Xiaodan Liang. MUSTARD: mastering uniform synthesis of theorem and
proof data. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vi-
enna, Austria, May 7-11, 2024. OpenReview.net, 2024. URL https://openreview.net/
forum?id=8xliOUg9EW.

Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timoth´ee Lacroix, Jiacheng Liu, Wenda Li,
Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding for-
mal theorem provers with informal proofs. In The Eleventh International Conference on Learn-
ing Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. URL
https://openreview.net/forum?id=SMa9EAovKMC.

Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph
Gonzalez, Hao Zhang, and Ion Stoica. Efficient memory management for large language model
serving with pagedattention. In Jason Flinn, Margo I. Seltzer, Peter Druschel, Antoine Kaufmann,
and Jonathan Mace (eds.), Proceedings of the 29th Symposium on Operating Systems Principles,
SOSP 2023, Koblenz, Germany, October 23-26, 2023, pp. 611–626. ACM, 2023. doi: 10.1145/
3600006.3613165. URL https://doi.org/10.1145/3600006.3613165.

Guillaume Lample, Timoth´ee Lacroix, Marie-Anne Lachaux, Aur´elien Rodriguez, Amaury Hayat,
Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem
In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh
proving.
(eds.), Advances in Neural Information Processing Systems 35: Annual Conference on Neural
Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - De-
cember 9, 2022, 2022. URL http://papers.nips.cc/paper_files/paper/2022/
hash/a8901c5e85fb8e1823bbf0f755053672-Abstract-Conference.html.

11

Under review as a conference paper at ICLR 2025

594
595

596
597
598
599
600
601

602
603
604
605
606
607

608
609
610
611
612

613
614
615
616
617
618

619
620
621
622
623
624

625
626
627
628
629
630

631
632
633
634
635

636
637
638
639
640
641

642
643
644
645
646
647

Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie
Si. A survey on deep learning for theorem proving. CoRR, abs/2404.09939, 2024. doi: 10.48550/
ARXIV.2404.09939. URL https://doi.org/10.48550/arXiv.2404.09939.

Norman Megill and David A Wheeler. Metamath: a computer language for mathematical proofs.

Lulu. com, 2019.

Maciej Mikula, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou,
Christian Szegedy, Lukasz Kucinski, Piotr Milos, and Yuhuai Wu. Magnushammer: A
transformer-based approach to premise selection. CoRR, abs/2303.04488, 2023. doi: 10.48550/
ARXIV.2303.04488. URL https://doi.org/10.48550/arXiv.2303.04488.

Lawrence C. Paulson. Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow),
volume 828 of Lecture Notes in Computer Science. Springer, 1994. ISBN 3-540-58244-4. doi:
10.1007/BFB0030541. URL https://doi.org/10.1007/BFb0030541.

Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving.

CoRR, abs/2009.03393, 2020. URL https://arxiv.org/abs/2009.03393.

Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya
In The Eleventh International
Sutskever. Formal mathematics statement curriculum learning.
Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenRe-
view.net, 2023. URL https://openreview.net/forum?id=-P7G-8dmSh4.

Samyam Rajbhandari, Olatunji Ruwase, Jeff Rasley, Shaden Smith, and Yuxiong He. Zero-infinity:
Breaking the GPU memory wall for extreme scale deep learning. CoRR, abs/2104.07857, 2021.
URL https://arxiv.org/abs/2104.07857.

Machel Reid, Nikolay Savinov, Denis Teplyashin, Dmitry Lepikhin, Timothy Lillicrap, Jean-
baptiste Alayrac, Radu Soricut, Angeliki Lazaridou, Orhan Firat, Julian Schrittwieser, et al. Gem-
ini 1.5: Unlocking multimodal understanding across millions of tokens of context. arXiv preprint
arXiv:2403.05530, 2024.

Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots
for theorem proving in lean. CoRR, abs/2404.12534, 2024. doi: 10.48550/ARXIV.2404.12534.
URL https://doi.org/10.48550/arXiv.2404.12534.

Terence Tao, 2023. URL https://teorth.github.io/pfr/blueprint.pdf.

Terence Tao. Machine assisted proof. Notices of the American Mathematical Society, to appear,

2024.

Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. Solving olympiad geometry with-
out human demonstrations. Nat., 625(7995):476–482, 2024. doi: 10.1038/S41586-023-06747-5.
URL https://doi.org/10.1038/s41586-023-06747-5.

Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie,
Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, and Xiaodan Liang. Dt-solver: Automated
theorem proving with dynamic-tree sampling guided by proof-level value function.
In Anna
Rogers, Jordan L. Boyd-Graber, and Naoaki Okazaki (eds.), Proceedings of the 61st Annual
Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023,
Toronto, Canada, July 9-14, 2023, pp. 12632–12646. Association for Computational Linguistics,
2023. doi: 10.18653/V1/2023.ACL-LONG.706. URL https://doi.org/10.18653/v1/
2023.acl-long.706.

Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing
Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, and Xiaodan Liang. Lego-prover: Neural
theorem proving with growing libraries. In The Twelfth International Conference on Learning
Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. OpenReview.net, 2024. URL
https://openreview.net/forum?id=3f5PALef5B.

12

Under review as a conference paper at ICLR 2025

Mingzhe Wang and Jia Deng.

Learning to prove theorems by learning to generate theo-
rems.
In Hugo Larochelle, Marc’Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and
Hsuan-Tien Lin (eds.), Advances in Neural Information Processing Systems 33: Annual Con-
ference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12,
2020, virtual, 2020. URL https://proceedings.neurips.cc/paper/2020/hash/
d2a27e83d429f0dcae6b937cf440aeb1-Abstract.html.

Sean Welleck.

Neural

theorem proving tutorial

ii.

https://github.com/cmu-l3/

ntptutorial-II, 2023.

Sean Welleck and Rahul Saha.

CoRR,
abs/2310.18457, 2023. doi: 10.48550/ARXIV.2310.18457. URL https://doi.org/10.
48550/arXiv.2310.18457.

LLMSTEP: LLM proofstep suggestions in lean.

Yuhuai Wu, Albert Q. Jiang, Jimmy Ba, and Roger Baker Grosse. INT: an inequality benchmark
for evaluating generalization in theorem proving. In 9th International Conference on Learning
Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL
https://openreview.net/forum?id=O6LPudowNQm.

Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik,
and Christian Szegedy. Autoformalization with large language models.
In Sanmi Koyejo,
S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Advances in Neu-
ral Information Processing Systems 35: Annual Conference on Neural Information Process-
ing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9,
2022, 2022. URL http://papers.nips.cc/paper_files/paper/2022/hash/
d0c6bc641a56bebee9d985b937307367-Abstract-Conference.html.

Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. Lean-github: Compiling github LEAN reposi-
tories for a versatile LEAN prover. CoRR, abs/2407.17227, 2024. doi: 10.48550/ARXIV.2407.
17227. URL https://doi.org/10.48550/arXiv.2407.17227.

Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu,
Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F.
Wu, Fuli Luo, and Chong Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback
for reinforcement learning and monte-carlo tree search. CoRR, abs/2408.08152, 2024. doi: 10.
48550/ARXIV.2408.08152. URL https://doi.org/10.48550/arXiv.2408.08152.

Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu,
Leandojo: Theorem prov-
Saad Godil, Ryan J. Prenger, and Animashree Anandkumar.
ing with retrieval-augmented language models.
In Alice Oh, Tristan Naumann, Amir
Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Advances in Neu-
ral
Information
Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16,
URL http://papers.nips.cc/paper_files/paper/2023/
2023,
hash/4441469427094f8873d0fecb0c4e1cee-Abstract-Datasets_and_
Benchmarks.html.

Information Processing Systems 36:

Annual Conference on Neural

2023.

Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook:
A large-scale lean problem set formalized from natural language math problems. arXiv preprint
arXiv:2406.03847, 2024.

Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark
In The Tenth International Conference on Learning
for formal olympiad-level mathematics.
Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. URL
https://openreview.net/forum?id=9ZPegFuFTFv.

Yaowei Zheng, Richong Zhang, Junhao Zhang, Yanhan Ye, Zheyan Luo, and Yongqiang Ma. Lla-
mafactory: Unified efficient fine-tuning of 100+ language models. CoRR, abs/2403.13372, 2024.
doi: 10.48550/ARXIV.2403.13372. URL https://doi.org/10.48550/arXiv.2403.
13372.

13

648
649

650
651
652
653
654
655

656
657
658
659
660
661

662
663
664
665
666

667
668
669
670
671
672

673
674
675
676
677
678

679
680
681
682
683
684

685
686
687
688
689

690
691
692
693
694
695

696
697
698
699
700
701

Under review as a conference paper at ICLR 2025

CONTENTS

A Background on Lean

B Limitations

C Detailed Information of Synthesizing Algorithms

C.1 Overview .

.

.

.

.

.

.

.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

C.2 Find Invocable Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

C.3 Construct New Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

C.3.1

rw tactic .

.

.

C.3.2

apply tactic .

C.4 Verify the Theorems

.

.

.

.

.

.

. . . .

. . .

. . . . . . . . . . . . . . . . . . . . . . . .

. . .

. . . . .

. . .

. . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

C.5 Limitations of Synthesis Pipeline . . . . . . . . . . . . . . . . . . . . . . . . . . .

D Deeper Analysis of Synthetic Dataset

D.1 Numerical Analysis .

D.2 Examples .

.

.

.

.

.

.

.

.

.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

D.3 Details of Training Data

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

D.3.1 Examples of Training Data . . . . . . . . . . . . . . . . . . . . . . . . . .

D.3.2 Preprocessing .

.

. .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . .

D.3.3 Classification of Extracted Tactics . . . . . . . . . . . . . . . . . . . . . .

D.3.4 Influence of the Quantity of SFT Dataset

. . . . . . . . . . . . . . . . . .

E Additional Experiments

E.1 Effectiveness of Different Tactics . . . . . . . . . . . . . . . . . . . . . . . . . . .

E.2 Analysis of the Tactics to Prove miniF2F Theorems . . . . . . . . . . . . . . . . .

E.2.1 Preference in Used Tactics . . . . . . . . . . . . . . . . . . . . . . . . . .

E.2.2

Influence of Additional Tactics . . . . . . . . . . . . . . . . . . . . . . . .

15

15

16

16

16

17

17

19

20

21

22

22

22

22

22

23

23

23

26

26

26

26

26

14

702
703

704
705
706
707
708
709

710
711
712
713
714
715

716
717
718
719
720

721
722
723
724
725
726

727
728
729
730
731
732

733
734
735
736
737
738

739
740
741
742
743

744
745
746
747
748
749

750
751
752
753
754
755

Under review as a conference paper at ICLR 2025

756
757

758
759
760
761
762
763

764
765
766
767
768
769

770
771
772
773
774

775
776
777
778
779
780

781
782
783
784
785
786

787
788
789
790
791
792

793
794
795
796
797

798
799
800
801
802
803

804
805
806
807
808
809

A BACKGROUND ON LEAN

Lean is a functional programming language and interactive theorem prover based on dependent
type theory. As one of the most popular formal systems, Lean aids mathematicians in formalizing
statements and proofs in a semi-auto style and enables them to verify the correctness of each proof
step through rigorous type-checking.

Theorem in Lean To some extent, theorems in Lean can be seen as a special variant of functions
in general-purpose programming languages. A theorem consists of a statement and corresponding
proof. In Lean, the keyword “theorem”, “example” or “lemma” is used to define the “function”,
sometimes followed by a specific function name. The assumption of a statement can be formatted
as implicit or explicit arguments, while the assertion of the statement specifies the return type of the
function. The proof of the statement can be viewed as the function body, which constructs a proof
term with the type specified by the assertion. There are two main proof styles in Lean: term-style
and tactic-style. In term-style proofs, theorems are proven using constructive methods. On the other
hand, tactic-style proofs sequentially decompose the proof goal using specific tactics. Although
tactic-style proofs are less readable, they tend to have shorter proof lengths. Most machine learning-
based theorem-proving systems focus on tactic-style proof. The synthesis method proposed by our
paper can be applied to both styles.

Tactic Lean offers various advanced tactics for theorem proving, which set it apart from other
formal systems (e.g., Coq, Isabelle). In handwritten proofs, authors tend to guide the reader on
building the proof through instructions such as “apply the previous lemma”, “invoke the principle
of mathematical induction”, or “simplify the expression”. Similarly, tactics in Lean are used to
describe how to construct a proof term incrementally. They help users decompose the proof goal
step by step, allowing users to focus on only one proof goal at a time.

Mathlib Mathlib7 is a comprehensive mathematical library for Lean, largely maintained by the
community, which encompasses a broad spectrum of mathematical subjects (e.g., algebra and anal-
ysis) and consists of over 120,000 theorems along with their respective axioms and definitions. This
extensive knowledge base serves as the primary corpus for neural theorem provers.

B LIMITATIONS

Our method exhibits some limitations that remain to be addressed in future endeavors.

Data Diversity and Quality We only define two symbolic rules (using two tactics) to synthesize
new theorems. The implementation of the synthesis pipeline is over general and utilizes little domain
knowledge, which affects the diversity and quality of synthetic data.

The Cost of Synthesizing Despite the CPU-only nature of our algorithm, the cost of synthesizing
remains huge. We believe the overhead can be significantly reduced with a finer implementation and
more specialized tools to interact with the Lean theorem prover.

Single-Round v.s. Multi-Round Theoretically speaking, our algorithms can be iteratively exe-
cuted by adding the synthesized theorems into seed theorems. Conversely, the synthesized repository
is very heavy, which makes it hard to interact with Lean using Leandojo and deploy our algorithm
on existing hardware.

Theorem-level or Term-level Our method synthesizes theorems from top to bottom and intro-
duces additional state-tactic pairs of specific tactics. Synthesizing formal data at the theorem level
Ideally, we
is not efficient and not consistent with the step-by-step nature of theorem-proving.
anticipate that we can synthesize formal data directly at the term level, which aligns with the char-
acteristics of interactive theorem proving.

7https://github.com/leanprover-community/mathlib4

15

Under review as a conference paper at ICLR 2025

Up-to-down v.s. Down-to-up We synthesize theorems in an up-to-down fashion. We construct
the new statements first and then retrieve the correct proofs. The up-to-down fashion depends on a
specific set of seed theorems, which restricts the diversity of synthetic data. A more fundamental
idea is that we can sample some terms in the symbolic space directly, merge them using symbolic
manipulations, and then find the corresponding goals for this new theorem. This AlphaGeometry-
style idea is hard to implement in Lean and requires a large amount of domain knowledge and
engineering endeavors.

Symbolic Synthesis in Conjunction with Other Techniques Our proposed method demonstrates
significant potential for integration with other techniques to enhance the theorem-proving capabil-
ities of LLMs. We posit that theorem synthesis in the symbolic space serves as a valuable com-
plement to prevailing auto-formalization methods. For instance, it may contribute to the expansion
of autoformalized datasets. Besides, our approach generates a substantial quantity of new proven
statements which can be utilized as a comprehensive database for Retrieval-Augmented Generation
(RAG) (Yang et al., 2023; Wang et al., 2024). Our objective is to amalgamate these methodologies
to develop a robust theorem prover in the future.

C DETAILED INFORMATION OF SYNTHESIZING ALGORITHMS

C.1 OVERVIEW

As discussed in Section 3, the entire algorithm is composed of four steps. 1) Find invocable theorems
for the candidate theorem by executing a specific tactic and retrieving the resulting proof state. 2)
Construct new statements, where we parse the resulting proof state and mutate the old statement
with the help of AST. 3) Establish the entire proof by inserting a have tactic and integrating it with
the old proof to build the whole proof for this new statement. 4) Verify the correctness of generated
theorems in Lean theorem prover. In practice, we separately run the time-consuming first step on
hundreds of 8-core CPU nodes and unify step 2) and step 3) together to construct the new theorem.
Then we will write back synthetic theorems and run “lake build” to verify the generated theorems.

C.2 FIND INVOCABLE THEOREMS

For each candidate theorem, we check whether other theorems can be used to rewrite or apply to
it by executing tactics. We use the run tac API provided by Leandojo to run a specific tactic and
extract the valid proof state according to predefined criteria. The instruction templates for each tactic
are listed in Table1. Here is the code snippet that illustrates this process.

1 ’’’args:
2

dojo: interactive environment
init_state: initial proof state of target theorem
theorem: a possible invocable theorem
hypos: the assumptions of the target theorem (extracted by parsing
the AST)

6 ’’’
7 def is_invocable_theorem(
8
9 ):
10

name = theorem.full_name
if mode == "rw":

dojo, init_state, theorem, hypos, mode="rw"

# e.g. rw [name] at hypo_name
insts = get_rw_insts(name, hypos)

elif mode == "apply":

# e.g. have hypo_str := by apply name
insts = get_apply_insts(name, hypos)

res = []
for i, inst in enumerate(insts):

try: next_state = dojo.run_tac(init_state, inst)
except Exception as e: ...
else:

state_info = {

"init_state": init_state.pp,

# pp means pretty-printed

16

810
811
812
813
814

815
816
817
818
819
820

821
822
823
824
825
826

827
828
829
830
831
832

833
834
835
836
837

838
839
840
841
842
843

844
845
846
847
848
849

850
851
852
853
854
855

856
857
858
859
860

861
862
863

3

4

5

11

12

13

14

15

16

17

18

19

20

21

22

23

Under review as a conference paper at ICLR 2025

24

25
26 }
27

28

29

30

31

32

33

"next_state": next_state.error if isinstance(next_state,

LeanError) else next_state.pp,

"rule": inst

if isinstance(next_state, LeanError):

if mode == "implication" \
and "unsolved goals" in next_state.error:

res.append(state_info)

elif isinstance(next_state, TacticState):

res.append(state_info)

return res

Listing 1: Find invocable theorems by running tactics.

We set different validation criteria for each tactic. For the rw tactic, if the resulting state is a Tac-
ticState, we annotate this theorem as invocable. In contrast, for the apply tactic, the resulting state
should be “unsolved goals”. Additionally, we filter the resulting invocable theorems to simplify
the problem of constructing new theorems. Specifically, we remove the invocable theorems whose
next state contains meta-variables (e.g.,?a, ?m123) for the rw tactic and unnamed meta-variables
(e.g.,?e12384) for the apply tactic. Ultimately, we retrieve the invocable theorems for each candi-
date theorem. One example of invocable theorems is shown in Fig 5.

The experiments run on a large collection of CPUs (512×8-core for the rw tactic and 256×8-core for
apply). The substantial CPU requirement is largely due to the memory-intensive nature of Leandojo,
which hinders multiprocessing on a single node. We anticipate a significant reduction in the cost of
our experiments by implementing a lighter interface for Lean interaction. The operation of apply is
more complex and time-consuming than rw. We set a one-hour timeout for each dojo environment
to reduce the time cost. When running a specific tactic, we do not add additional imports to the dojo
environment to avoid introducing human preferences in the process of synthesis. This setting may
narrow the scope of theorems that the tactic can access and lower the variety of invocable theorems.

In summary, finding invocable theorems constitutes the most time-consuming and computationally
intensive stage of our algorithm, entailing trade-offs among cost, time, and generated data volume.

C.3 CONSTRUCT NEW THEOREMS

To create a new theorem, we construct the new statement using the invocable theorems returned by
Section C.2 and then establish the entire proof through have tactic. Our symbolic engine is built upon
Leandojo API, utilizing the extracted AST and some string manipulations. To facilitate the detailed
explanation of algorithms, we will delineate the implementation of these two tactics separately in
the following pseudocode or source code.

C.3.1

rw TACTIC

The logic of constructing a new statement for rw tactic is simple. We just identify whether a specific
assumption or assertion has been rewritten by parsing invocable instructions with regular expres-
sions. Then we parse the AST node of the candidate statement to locate the corresponding part that
should be mutated. Finally, we extract the new assumption or assertion from the next proof state and
replace the old one with the new one. The main procedure is shown in Algorithm 2.

Algorithm 2 Construct new statement for rw tactic

Input: candidate statement s, invocable theorem i
Output: mutated statement sm
node ← EXTRACT AST(s)
, next state, inst ← i
flag ← IDENTIFY(i)
location l ← PARSE(node, i, f lag)
should to be mutated
m ← CONSTRUCT(next state)
new statement sm ← REPLACE(s, m, l)

▷ extract the AST of candidate statement
▷ get the next state and instruction
▷ flag specifies whether the assumption or assertion should be mutated
▷ parse AST node and locate the corresponding part that

▷ parse the next proof state and construct the target string

864
865

866
867
868
869
870
871

872
873
874
875
876
877

878
879
880
881
882

883
884
885
886
887
888

889
890
891
892
893
894

895
896
897
898
899
900

901
902
903
904
905

906
907
908
909
910
911

912
913
914
915
916
917

17

Under review as a conference paper at ICLR 2025

Figure 5: Examples of invocable theorems for apply

After creating a new statement, we should insert a have tactic to construct the whole proof. If the
assumption is modified, then we just restore it to the old one by reversing the direction of rw within
a have instruction and then concatenate it with the original proof. If the assertion is mutated, the
have tactic can be used to prove the original assertion with initial proof block. Then we just rewrite
the old proof goal to the new one to construct the whole proof. Here is a simplified code snippet that
illustrates this process.

1 def proof_generation_rw(
2

invocable_inst,
flag,
proof_str,
conc_or_hypo_old=None,
is_tactic_style=False
):

3

4

5

6

7

8

9

10

11

inst = invocable_inst["rule"]
if flag == "hypo":

hypo_name = parse(inst, flag)

# find the delimiter for proof str(e.g. := by or :=)(simplified
version)

18

918
919
920
921
922

923
924
925
926
927
928

929
930
931
932
933
934

935
936
937
938
939
940

941
942
943
944
945

946
947
948
949
950
951

952
953
954
955
956
957

958
959
960
961
962
963

964
965
966
967
968

969
970
971

theorem_name: Char.ofNat_toNatrule:   have h : isValidCharNat c.toNat := by apply List.rel_of_pairwise_consinit_state:c : Charh : isValidCharNat (toNat c)⊢ ofNat (toNat c) = cnext_state: unsolved goalscase hpc : Charh : isValidCharNat (toNat c)⊢ Std.RBNode.All isValidCharNat ?tcase Hc : Charh : isValidCharNat (toNat c)⊢ ∀ {x : ℕ}, x ∈ ?lb → isValidCharNat xcase ac : Charh : isValidCharNat (toNat c)⊢ Std.RBNode.lowerBound? ?cut ?t ?lb = some (toNat c)case lbc : Charh : isValidCharNat (toNat c)⊢ Option ℕcase cutc : Charh : isValidCharNat (toNat c)⊢ ℕ → Orderingcase tc : Charh : isValidCharNat (toNat c)⊢ Std.RBNode ℕUnder review as a conference paper at ICLR 2025

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

972
973

974
975
976
977
978
979

980
981
982
983
984
985

986
987
988
989
990

991
992
993
994
995
996

997
998
999
1000
1001
1002

1003
1004
1005
1006
1007
1008

1009
1010
1011
1012
1013

1014
1015
1016
1017
1018
1019

1020
1021
1022
1023
1024
1025

if is_tactic_style:

delimiter = ":= by"

else:

delimiter = ":="

splits = proof_str.split(delimiter)
proof_seqs = delimiter.join(splits[1:])
if flag == "hypo":

rev_inst = reverse_rw(invocable_inst)
have_template = "have {subgoal} := by {proof_seqs}"
have_inst = have_template.format(
subgoal=conc_or_hypo_old,
proof_seqs=rev_inst)

have_inst += f’;exact {hypo_name}’
end_inst = proof_seqs

elif flag == "conclusion":

have_template = "have : {subgoal} {delimiter} {proof_seqs}"
have_inst = have_template.format(
subgoal=conc_or_hypo_old,
delimiter=delimiter,
proof_seqs=proof_seqs)

head = "by " if not is_tactic_style else ""
_suffix = " at this;exact this"
end_inst = head + inst + _suffix

# do indentation
have_inst = indent_code(delimiter, proof_str, have_inst, indent_level
=...)
end_inst = indent_code(delimiter, proof_str, end_inst, indent_level
=...)
# concat the different parts of proof
prefix = splits[0] + delimiter + ’\n’
suffix = end_inst if end_inst.startswith(’\n’) else ’\n’ + end_inst
new_proof = prefix + have_inst + suffix
return new_proof

Listing 2: Build the whole proof for rw tactic

C.3.2

apply TACTIC

Algorithm 3 Construct new statement for apply tactic

Input: candidate statement s, invocable instruction i
Output: mutated statement sm
H ← ∅
node ← EXTRACT AST(s)
, next state, inst ← i
M, G ← PARSE(next state)
for m ∈ M do

▷ initialize the set of new assumptions
▷ extract the AST of candidate statement
▷ get the next state and instruction
▷ get the set of metavaribales and other subgoals
▷ Assigning metavariables

Add ASSIGN(m, next state) to H

end for
for g ∈ G do

Add ASSIGN(g, next state, M ) to H

▷ Fill the other subgoals depending on meta-varibales

end for
H ← HANDLE NAMING CONFLICTS(H)
new assumption hm ← CONCAT(H)
location l ← PARSE(node, i)
mutated
sm ← REPLACE(s, hm, l)

▷ parse AST node and locate the old assumption that needs to be

Constructing new statements for apply tactic is more complex than rw. Applying a theorem may
introduce some metavariables and new subgoals into the local context for the resulting proof state as
shown in Fig 5. We assign values to the metavariables by parsing the next state and then retrieve all
subgoals containing metavariables as new assumptions. For each new assumption, we can extract

19

Under review as a conference paper at ICLR 2025

1026
1027
1028
1029
1030

1031
1032
1033
1034
1035
1036

1037
1038
1039
1040
1041
1042

1043
1044
1045
1046
1047
1048

1049
1050
1051
1052
1053

1054
1055
1056
1057
1058
1059

1060
1061
1062
1063
1064
1065

1066
1067
1068
1069
1070
1071

1072
1073
1074
1075
1076

1077
1078
1079

its name and type from the proof state. To avoid naming conflicts, we define a set of rules to rename
the variable according to the naming conversion of Mathlib8. Ultimately, we concatenate all new
assumptions and replace the old assumption with them. This procedure is shown in Algorithm 3.

Similarly, we can construct the entire proof for the new statement by inserting a have lemma. The
simplified code snippet illustrates this process.

1 def proof_generation_apply(cases_goals, inst, proof_str, is_tactic_style)

:
if len(cases_goals) == 1:

lemma = inst + "; assumption"

elif len(cases_goals) > 1:

lemma = inst + "<;> assumption"

else:

raise Exception("no available case and corresponding goal")

if is_tactic_style:

delimiter = ":= by"

else:

delimiter = ":="

splits = proof_str.split(delimiter)
proof_seqs = delimiter.join(splits[1:])
lemma = indent_code(delimiter, proof_str, lemma, indent_level=...)
prefix = splits[0] + delimiter + ’\n’
suffix = proof_seqs if proof_seqs.startswith(’\n’) else ’\n’ +
proof_seqs
new_proof = prefix + lemma + suffix
return new_proof

Listing 3: Build the whole proof for apply tatic

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

.

C.4 VERIFY THE THEOREMS

Our method creates a set of variants for each candidate theorem in Mathlib4. We write the variants
back to the original file and execute lake build for verification. We remove the wrong lines for
each file by parsing the error message returned by Lean. Then, we will rebuild the repo to ensure
the effectiveness of verification. We remove the files that cause errors in the rebuilding process.
Specifically, for each 8-core CPU node, we only build one “.lean” file each time to speed up this
process and simplify the logic of parsing. The whole experiment runs on 2,048 CPUs (256×8-core).
The code snippets illustrate the procedure for each CPU node. After verifying the correctness of the
synthesized theorem, we extract the state-tactic pairs from our augmented Mathlib repository using
Leandojo. For rw or apply, it takes three days for a 96-core CPU machine to trace the enlarged
repository. In practice, we split the modified lean files into several portions, separately write them
into multiple lean repositories, and trace the repos on several 96-core CPU machines.

1 # A single 8-core CPU node
2 res = []
3 for idx, file in enumerate(files):
4

’’’file {

# for each modified file

5

6

7

8

9

10

11

12

13

file_name: "name of the lean file",
text:

"the content of this file after writing synthesized

variants into this file"

"loc": {"theorem_name": [(start_line_nb, end_line_nb)...]}
}’’’

tmp = {

’loc’: file[’loc’],
’file_name’: file[’file_name’],
’text’: file[’text’]
}

8https://leanprover-community.github.io/contribute/naming.html

20

Under review as a conference paper at ICLR 2025

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

60

61

62

63

64

1080
1081

1082
1083
1084
1085
1086
1087

1088
1089
1090
1091
1092
1093

1094
1095
1096
1097
1098

1099
1100
1101
1102
1103
1104

1105
1106
1107
1108
1109
1110

1111
1112
1113
1114
1115
1116

1117
1118
1119
1120
1121

1122
1123
1124
1125
1126
1127

1128
1129
1130
1131
1132
1133

file_name = file[’file_name’]
file_path = os.path.join(mathlib_package_path, file_name)
# extract the old content of this file
with open(file_path, "r") as f:

old_str = f.read()

# replace the old content with new content
with open(file_path, "w") as f:

f.write(file[’text’])

# change the build target to current file
with open(LIBRARY_ROOT_FILE, ’w’) as f:
Mathlib.lean

# LIBRARY_ROOT_PATH:

module_name = file_name.replace(’/’, ’.’).replace(’.lean’, ’’)
f.write(f"import {module_name}")

if have_variants(file):

## lake build the new mathlib project
wd = os.getcwd()
result = lake_build(mathlib_package_path) #a helper function
os.chdir(wd)
## parse the output
# subprocess error
if result == None: tmp[’valid_loc’] = ["No variants"]
elif result == 0:

tmp[’valid_loc’] = tmp[’loc’]
print(’successful build’)

# timeout error
elif result == -1: tmp[’valid_loc’] = ["No variants"]
else:

# find the error locations(line numbers)
pattern = fr"({file_name}):(\d+):(\d+): error:"
errors = re.findall(pattern, result)
if len(errors) == 0:

tmp[’valid_loc’] = ["No variants"] #

parse exception

else:

# extract line numbers from errors
error_line_nbs = ...
# get the locations of all variants
intervals = ...
# drop the error ones and write back
valid_locs = diff(intervals, error_line_nbs)
write_back(valid_locs, file[’text’])
## rebuilt the project if causes error then remove this

wd = os.getcwd()
result = lake_build(mathlib_package_path)
os.chdir(wd)
if result != 0:

tmp[’valid_loc’] = ["No variants"] #

file

rebuild error

else:

# pass the rebuilding process

tmp[’valid_loc’] = valid_locs

else:

tmp[’valid_loc’] = [’No variants’]

# write back the original content
with open(file_path, "w") as f:

f.write(old_str)

res.append(tmp)

Listing 4: Verify the correctness of generated theorems

C.5 LIMITATIONS OF SYNTHESIS PIPELINE

Our synthesis pipeline is mainly based on the advanced Leandojo tool. We use it to interact with
Lean, parse abstract syntax trees and trace state-tactic pairs. However, this tool has the following
weaknesses. 1) It will generate a significant number of temporary files that consume substantial disk
space when initializing a “dojo” environment. The memory-intensive nature of this tool hinders our

21

Under review as a conference paper at ICLR 2025

ability to effectively implement multiprocessing. 2) Moreover, it lacks native support for tracing a
local Lean repository, so we must first upload our data to GitHub. 3) We encounter challenges when
tracing a repository of a scale significantly larger than that of Mathlib, which makes it hard to do
multi-round synthesis. We aspire to enhance the functionality of the Leandojo tool to tackle more
demanding scenarios in our forthcoming endeavors.

In addition, the process of constructing statements and proofs plays an important role in data volume
and diversity. Our implementation involves parsing the abstract syntax tree for localization and
conducting various string manipulations, which is straightforward but struggles with sophisticated
situations such as coercion, naming conflicts, and other corner cases. We are looking forward to
refactoring our modification logic with the metaprogramming API of lean 9 in the future, which is
more robust and easier to extend.

D DEEPER ANALYSIS OF SYNTHETIC DATASET

D.1 NUMERICAL ANALYSIS

The histogram of the number of variants synthesized by each tactic is shown in Figure 6.

Figure 6: The distribution of the number of variants (only 99% of the data are visualized).

For each tactic, we also list the top 20 theorems with the highest number of variants in Figure 7.

D.2 EXAMPLES

Due to the large volume of synthetic data, it is challenging to display all the data in the appendix.
We only display a subset of demo theorems for reference. The proof lengths of these theorems range
from 1 to 3 lines. To explore further details, please examine our dataset. The synthesized theorems
of rw tactic are displayed in Fig 8. The synthesized theorems of apply are displayed in Fig 9.

D.3 DETAILS OF TRAINING DATA

D.3.1 EXAMPLES OF TRAINING DATA

As shown in Fig 10, we synthesize a series of variants for each candidate theorem by employing
different tactic instructions to mutate existing theorems. We simply combine these additional theo-
rems with the original theorems in Mathlib and train LLMs on this augmented corpus. In addition
to synthesizing variants for each candidate theorem, symbolic manipulations to construct new theo-
rems also introduce some new state-tactic pairs. What should be noted is that the state-tactic pairs

9https://leanprover-community.github.io/lean4-metaprogramming-book/

22

1134
1135

1136
1137
1138
1139
1140
1141

1142
1143
1144
1145
1146
1147

1148
1149
1150
1151
1152

1153
1154
1155
1156
1157
1158

1159
1160
1161
1162
1163
1164

1165
1166
1167
1168
1169
1170

1171
1172
1173
1174
1175

1176
1177
1178
1179
1180
1181

1182
1183
1184
1185
1186
1187

rwapplyUnder review as a conference paper at ICLR 2025

1188
1189

1190
1191
1192
1193
1194
1195

1196
1197
1198
1199
1200
1201

1202
1203
1204
1205
1206

1207
1208
1209
1210
1211
1212

1213
1214
1215
1216
1217
1218

1219
1220
1221
1222
1223
1224

1225
1226
1227
1228
1229

1230
1231
1232
1233
1234
1235

1236
1237
1238
1239
1240
1241

Figure 7: The top20 theorems for rw and apply.

are extracted by Leandojo rather than manually designed symbolic rules. We have not performed
any post-processing on the extracted state-tactic pairs. We group the extracted theorems by the em-
ployed tactics (rw, apply, have). The examples of rw and apply are shown in Fig 11. The examples
of have are shown in Fig 12.

D.3.2 PREPROCESSING

The synthesized variants of theorems and corresponding state-tactic pairs appearing in the test split
of Leandojo benchmark are removed. During the data synthesis process, an invocable theorem may
be used to rewrite or apply to different candidate theorems. Thus, many data points extracted from
the augmented Mathlib repository share the same tactic and invocable theorem (i.e., premise), such
as premise A in “rw [A]” or “apply A”. These data points have similar changes in the proof state.
We keep one state-tactic pair for each used premise in the synthesized state-tactic pairs and obtain
about 30k data points for each tactic.

D.3.3 CLASSIFICATION OF EXTRACTED TACTICS

The types of extracted state-tactic pairs are mainly determined by the symbolic manipulations to
construct the theorems. We construct the proof by inserting a have instruction and integrating it
with the original proof. As a result, we manually introduce tactics centered on rw, apply or have.
The traced data predominantly features these tactics. The style of the seed theorem (tactic-style or
term-style) and the implementation of the tracing tool are also key factors for the traced data. To see
more details of this process, it is a good choice to trace the synthesized repository in person. Being
familiar with the tracing process will offer some valuable guidance in designing symbolic rules to
modify the proof. The extracted state-tactic pairs can also be post-processed (e.g., split the chained
tactics into single ones), which has not been explored by our work.

D.3.4

INFLUENCE OF THE QUANTITY OF SFT DATASET

We assess the impact of varying quantities of additional state-tactics pairs for each tactic under
several conditions. 1) Mathlib-train with no additional data points; 2) Downsampling with a ratio of
0.25, resulting in 7.5k additional data points; 3) Downsampling with a ratio of 0.5, resulting in 15k
additional data points; 4) Our setting with a deduplication threshold of 1, resulting in 30k additional
data points; 5) Deduplication with a threshold of 50, resulting in 500k additional data points; and

23

rwapplyUnder review as a conference paper at ICLR 2025

1242
1243

1244
1245
1246
1247
1248
1249

1250
1251
1252
1253
1254
1255

1256
1257
1258
1259
1260

1261
1262
1263
1264
1265
1266

1267
1268
1269
1270
1271
1272

1273
1274
1275
1276
1277
1278

1279
1280
1281
1282
1283

1284
1285
1286
1287
1288
1289

1290
1291
1292
1293
1294
1295

Figure 8: Examples of synthesized theorems for rw

6) No deduplication, resulting in 3M additional data points. We fine-tune Llama-3-8b on these
different mixtures of data and evaluate their performance on random split of Leandojo Benchmark.
The experimental results are shown in Fig 4, demonstrating that our setting achieves a relatively
optimal balance between overhead and performance.

24

Finset.multiplicativeEnergy_mono_righttheorem multiplicativeEnergy_mono_right (ht : t₁ ⊆ t₂) :    multiplicativeEnergy s t₁ ≤ multiplicativeEnergy s t₂ :=  multiplicativeEnergy_mono Subset.rfl htexample (ht : t₁ ∩ t₂ = t₁) :    multiplicativeEnergy s t₁ ≤ multiplicativeEnergy s t₂:=  have ht : t₁ ⊆ t₂ := by rw [Finset.inter_eq_left] at ht;exact ht  multiplicativeEnergy_mono Subset.rfl htexample (ht : t₁.val ⊆ t₂.val) :    multiplicativeEnergy s t₁ ≤ multiplicativeEnergy s t₂:=  have ht : t₁ ⊆ t₂ := by rw [←Finset.subset_def] at ht;exact ht  multiplicativeEnergy_mono Subset.rfl htexample (ht : t₁ ⊆ t₂) :     max (multiplicativeEnergy s t₂) (multiplicativeEnergy s t₁) = multiplicativeEnergy s t₂:=  have : multiplicativeEnergy s t₁ ≤ multiplicativeEnergy s t₂ :=     multiplicativeEnergy_mono Subset.rfl ht  by rw [←max_eq_left_iff] at this;exact thisMultiset.card_le_cardtheorem card_le_card {s t : Multiset α} (h : s ≤ t) : card s ≤ card t :=  leInductionOn h Sublist.length_leexample {s t : Multiset α} (h : s ≤ t) :  ∀ ⦃c : ℕ⦄, card t < c → card s < c:=  have : card s ≤ card t :=     leInductionOn h Sublist.length_le  by rw [←forall_lt_iff_le'] at this;exact thisexample {s t : Multiset α} (h : s ≤ t) :  card s ⊓ card t = card s:=  have : card s ≤ card t :=     leInductionOn h Sublist.length_le  by rw [←inf_eq_left] at this;exact thisexample {s t : Multiset α} (h : s ≤ t) :  card s = card t ∨ card s < card t:=  have : card s ≤ card t :=     leInductionOn h Sublist.length_le  by rw [le_iff_eq_or_lt] at this;exact thisNat.one_lt_pow'theorem one_lt_pow' (n m : ℕ) : 1 < (m + 2) ^ (n + 1) := one_lt_pow (n + 1) (m + 2) n.succ_ne_zero (Nat.lt_of_sub_eq_succ rfl)example (n m : ℕ) : (m + 2) ^ (n + 1) ≠ 0 ∧ (m + 2) ^ (n + 1) ≠ 1:= have : 1 < (m + 2) ^ (n + 1) :=   one_lt_pow (n + 1) (m + 2) n.succ_ne_zero (Nat.lt_of_sub_eq_succ rfl) by rw [Nat.one_lt_iff_ne_zero_and_ne_one] at this;exact thisexample (n m : ℕ) : (m + 2) ^ (n + 1) < (m + 2) ^ (n + 1) * (m + 2) ^ (n + 1):= have : 1 < (m + 2) ^ (n + 1) :=   one_lt_pow (n + 1) (m + 2) n.succ_ne_zero (Nat.lt_of_sub_eq_succ rfl) by rw [←Nat.lt_mul_self_iff] at this;exact thisUnder review as a conference paper at ICLR 2025

1296
1297

1298
1299
1300
1301
1302
1303

1304
1305
1306
1307
1308
1309

1310
1311
1312
1313
1314

1315
1316
1317
1318
1319
1320

1321
1322
1323
1324
1325
1326

1327
1328
1329
1330
1331
1332

1333
1334
1335
1336
1337

1338
1339
1340
1341
1342
1343

1344
1345
1346
1347
1348
1349

Figure 9: Examples of synthesized theorems for apply

25

StrictMonoOn.mapsTo_Ioclemma StrictMonoOn.mapsTo_Ioc (h : StrictMonoOn f (Icc a b)) :  MapsTo f (Ioc a b) (Ioc (f a) (f b)) := fun _c hc ↦ ⟨h (left_mem_Icc.2 <| hc.1.le.trans hc.2) (Ioc_subset_Icc_self hc) hc.1,  h.monotoneOn (Ioc_subset_Icc_self hc) (right_mem_Icc.2 <| hc.1.le.trans hc.2) hc.2⟩example (h : StrictMonoOn f (Icc a b)  True) :  MapsTo f (Ioc a b) (Ioc (f a) (f b)):= have h : StrictMonoOn f (Icc a b) := by apply of_iff_true; assumption fun _c hc ↦ ⟨h (left_mem_Icc.2 <| hc.1.le.trans hc.2) (Ioc_subset_Icc_self hc) hc.1,  h.monotoneOn (Ioc_subset_Icc_self hc) (right_mem_Icc.2 <| hc.1.le.trans hc.2) hc.2⟩example (H : ∀ (b_1 : Prop), (StrictMonoOn f (Icc a b) → b_1) → StrictMonoOn f (Icc a b)) :  MapsTo f (Ioc a b) (Ioc (f a) (f b)):= have h : StrictMonoOn f (Icc a b) := by apply peirce'; assumption  …example (h : Icc a b ∈ {x | StrictMonoOn f x}) :  MapsTo f (Ioc a b) (Ioc (f a) (f b)):= have h : StrictMonoOn f (Icc a b) := by apply Membership.mem.out; assumption …PNat.XgcdType.reduce_atheorem reduce_a {u : XgcdType} (h : u.r = 0) : u.reduce = u.finish := by  rw [reduce]  exact if_pos hexample {u : XgcdType} (h : 0 ∣ r u) : u.reduce = u.finish:= by  have h : u.r = 0 := by apply Nat.eq_zero_of_zero_dvd; assumption  rw [reduce]  exact if_pos hexample {u : XgcdType} (H : u.bp + 1 ∣ u.ap + 1) : u.reduce = u.finish:= by  have h : u.r = 0 := by apply Nat.mod_eq_zero_of_dvd; assumption  …example {u : XgcdType} (n : ℕ) (H : Nat.gcd (r u) n = 0) : u.reduce = u.finish:= by  have h : u.r = 0 := by apply Nat.eq_zero_of_gcd_eq_zero_left<;> assumption   …Ordnode.not_le_deltatheorem not_le_delta {s} (H : 1 ≤ s) : ¬s ≤ delta * 0 :=  not_le_of_gt Hexample {s} (h : 0 < s) (a : 1 ∣ s) : ¬s ≤ delta * 0:=  have H : 1 ≤ s := by apply Nat.le_of_dvd<;> assumption  not_le_of_gt Hexample {s} (n : ℕ) (H1 : s ∣ n) (H2 : 0 < n) : ¬s ≤ delta * 0:=  have H : 1 ≤ s := by apply Nat.pos_of_dvd_of_pos<;> assumption  …example {s} (l : List ℕ) (p : List.Pairwise LE.le (1 :: l)) (a : s ∈ l) : ¬s ≤ delta * 0:=  have H : 1 ≤ s := by apply List.rel_of_pairwise_cons<;> assumption  …Under review as a conference paper at ICLR 2025

1350
1351

1352
1353
1354
1355
1356
1357

1358
1359
1360
1361
1362
1363

1364
1365
1366
1367
1368

1369
1370
1371
1372
1373
1374

1375
1376
1377
1378
1379
1380

1381
1382
1383
1384
1385
1386

1387
1388
1389
1390
1391

1392
1393
1394
1395
1396
1397

1398
1399
1400
1401
1402
1403

Figure 10: Examples of data for pretraining

E ADDITIONAL EXPERIMENTS

E.1 EFFECTIVENESS OF DIFFERENT TACTICS

We evaluate the effectiveness of different tactics by combining additional state-tactic pairs of a
specific tactic with Mathlib-train and fine-tuning the LLMs using this mixture. The experimental
results are shown in Table 6. We observe that state-tactic pairs of rw and apply are beneficial for the
theorem-proving ability of the LLM. And the highest improvement is achieved by the combination
of these two tactics. For the state-tactic pairs of have, we assume that these data will teach the
model to introduce lemmas in the process of proving a theorem, helping them to prove the theorems
in multiple steps. However, experimental data show that have has complex effects on the proving
capacity of LLMs. The performance on a mixture of “have” and other tactics shows poorer results
compared to that on a single tactic. We hope to investigate the effectiveness of have tactic soon.

E.2 ANALYSIS OF THE TACTICS TO PROVE MINIF2F THEOREMS

E.2.1 PREFERENCE IN USED TACTICS

To see the preference for the tactics used to prove competition-level problems, we perform a com-
prehensive analysis of the theorems proved by different LLMs. Specifically, we fine-tune different
LLMs with the random train-split of Leandojo benchmark and gather all theorems proved by these
models. The collection of these models proves 100 theorems out of 244 theorems (41%) on the
test split of miniF2F benchmark. The average length of the proofs generated by these models is
1.38. And the distribution of these proved theorems is shown in Fig 14. We have the following
observations. 1) About half of the theorems in the miniF2F test split can be proven with only 1-2
line proofs. 2) Most of the theorems are proved with advanced and automatic tactics in Lean (e.g.,
norm num, linarith, omega, simp, etc.). We assume that these tactics play an important role in the
theorem-proving ability of LLMs to prove competition-level problems. From the above observa-
tions, we assume that synthesizing advanced tactic data points rather than basic data points featuring
rw and apply is promising to improve the performance of proving competition-level problems.

E.2.2

INFLUENCE OF ADDITIONAL TACTICS

We analyze the distribution of used tactics in proven miniF2F problems across different data com-
positions. The dynamics of distribution changes are shown in Fig. 15. We assume that increasing

26

Variant  of  rwtheorem_name: CategoryTheory.Limits.Multicofork.sigma_condition_variant_0file_path: Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.leantext: example :  MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K) ∈ [MultispanIndex.sndSigmaMap I ≫ Sigma.desc (π K)]:= by have : I.fstSigmaMap ≫ Sigma.desc K.π = I.sndSigmaMap ≫ Sigma.desc K.π := by      ext     simp    rw [←List.mem_singleton] at this;exact thismeta: https://github.com/leanprover-community/mathlib4/commit/3c307701fa7e9acbdc0680d7f3b9c9fed9081740’Variant  of  applytheorem_name: UniformInducing.equicontinuous_iff_variant_26file_path: Mathlib/Topology/UniformSpace/Equicontinuity.leantext: example {F : ι → X → α} {u : α → β} (B : Set (Set (α → β))) (s : Set (α → β)) (hB : TopologicalSpace.IsTopologicalBasis B) (hs : IsOpen s) (h : ∀ U ∈ B, U ⊆ s → U ⊆ UniformInducing) (a : u ∈ s) : Equicontinuous F  Equicontinuous ((u ∘ ·) ∘ F):= by have hu : UniformInducing u := by apply TopologicalSpace.IsTopologicalBasis.subset_of_forall_subset<;> assumption congrm ∀ x, ?_ rw [hu.equicontinuousAt_iff]meta: https://github.com/leanprover-community/mathlib4/commit/3c307701fa7e9acbdc0680d7f3b9c9fed9081740Under review as a conference paper at ICLR 2025

Table 6: The effectiveness of different tactics

Methods

Llama3-8b
Mathlib-train

rw tactic
Mathlib-train + rw
Mathlib-train + have
Mathlib-train + rw + have

apply tactic
Mathlib-train + apply
Mathlib-train + have
Mathlib-train + apply + have

both tactic
mathlib-train + rw + apply

deepseek-coder-7b-base-v1.5
Mathlib-train

rw tactic
Mathlib-train + rw
Mathlib-train + have
Mathlib-train + rw + have

apply tactic
Mathlib-train + apply
Mathlib-train + have
Mathlib-train + apply + have

both tactic
Mathlib-train + rw + apply

random

novel premises

Search Budget

58.22

38.52

57.85 (-0.37)
58.27 (+0.05)
57.96 (-0.26)

41.59 (+3.07)
41.29 (+2.77)
41.53 (+3.01)

56.71 (-1.51)
57.44 (-0.78)
57.23 (-0.99)

40.02 (+1.51)
39.24 (+0.72)
38.34 (-0.18)

1 × 32

1 × 32
1 × 32
1 × 32

1 × 32
1 × 32
1 × 32

58.53 (+0.31)

41.95 (+3.44)

1 × 32

57.7

39.24

58.63 (+0.93)
58.11 (+0.41)
58.74 (+1.04)

41.05 (+1.81)
39.06 (-0.18)
40.57 (+1.33)

57.96 (+0.26)
57.02 (-0.68)
58.16 (+0.46)

41.17 (+1.93)
39.66 (+0.42)
39.78 (+0.54)

1 × 32

1 × 32
1 × 32
1 × 32

1 × 32
1 × 32
1 × 32

58.37 (+0.67)

42.92 (+3.68)

1 × 32

Table 7: The results of miniF2F for different LLMs. We fine-tune each model with the random
train-split of Leandojo benchmark and evaluate their performance on miniF2F benchmark.

Methods

miniF2F-test

Llama-3-8b
deepseek-coder-base-7b-v1.5
deepseek-math-7b-base
llemma-7b
mistral-7b
internlm2-math-7b

Combination

34.01
37.70
34.42
32.38
32.38
36.06

40.98

the diversity of synthesized tactics and adjusting the tactic distribution will be beneficial to enhance
the theorem-proving ability of LLMs.

1404
1405

1406
1407
1408
1409
1410
1411

1412
1413
1414
1415
1416
1417

1418
1419
1420
1421
1422

1423
1424
1425
1426
1427
1428

1429
1430
1431
1432
1433
1434

1435
1436
1437
1438
1439
1440

1441
1442
1443
1444
1445

1446
1447
1448
1449
1450
1451

1452
1453
1454
1455
1456
1457

27

Under review as a conference paper at ICLR 2025

1458
1459

1460
1461
1462
1463
1464
1465

1466
1467
1468
1469
1470
1471

1472
1473
1474
1475
1476

1477
1478
1479
1480
1481
1482

1483
1484
1485
1486
1487
1488

1489
1490
1491
1492
1493
1494

1495
1496
1497
1498
1499

1500
1501
1502
1503
1504
1505

1506
1507
1508
1509
1510
1511

Figure 11: Examples of rw and apply data points for finetuning

28

instruction:/- You are proving a theorem in Lean 4.You are given the following information:- The current proof state, inside [STATE]...[/STATE]Your task is to generate the next tactic in the proof.Put the next tactic inside [TAC]...[/TAC]-/rw  tacticinput:[STATE]α : Type u_1β : Type u_2R : Type u_3s t : Finset αf : α → βn : ℕinst : DecidableEq αthis : s.card = 2  ∃ x y, x ≠ y ∧ s = {x, y}⊢ s.card = 2  ∃ a ∈ Set.range fun x y => x ≠ y ∧ s = {x, y}, Exists a[/STATE][TAC]output:rw [←Set.exists_range_iff] at this[/TAC]apply  tacticinput:[STATE]n : ℕinst : NeZero na b : ZMod nw : val b ∈ HAdd.hAdd (val a) ⁻¹' Nat.le n⊢ n ≤ val a + val b[/STATE][TAC]output:apply Set.mapsTo_preimage[/TAC]Under review as a conference paper at ICLR 2025

1512
1513

1514
1515
1516
1517
1518
1519

1520
1521
1522
1523
1524
1525

1526
1527
1528
1529
1530

1531
1532
1533
1534
1535
1536

1537
1538
1539
1540
1541
1542

1543
1544
1545
1546
1547
1548

1549
1550
1551
1552
1553

1554
1555
1556
1557
1558
1559

1560
1561
1562
1563
1564
1565

Figure 12: Examples of have data points for finetuning

29

[/TAC]instruction:/- You are proving a theorem in Lean 4.You are given the following information:- The current proof state, inside [STATE]...[/STATE]Your task is to generate the next tactic in the proof.Put the next tactic inside [TAC]...[/TAC]-/have tactic-rw-relatedCase oneinput:[STATE]m n a b : ℕcop : Coprime m nha : a ≠ 0hb : b ≠ Int.toNat 0⊢ a * m + b * n ≠ m * n[/STATE][TAC]output:have hb : b ≠ 0 := by rw [Int.toNat_zero] at hb;exact hb[/TAC]Case twoinput:[STATE]α : Type u_1inst : DecidableEq α𝒜𝒜: Finset (Finset α)u v a : Finset αr : ℕhuv : Equiv.swap u.card v.card = Equiv.refl ℕa : Finset α⊢(compress u v a).card = a.card[/STATE][TAC]output:have huv : u.card = v.card := by rw [Equiv.swap_eq_refl_iff] at huv;exact huv[/TAC]have tactic-apply-relatedInput:[STATE]α : Type uβ : Type vinst¹ : DecidableEq αinst : Fintype ασ : Perm αn : ℕh : orderOf σ ∈{x | Nat.Coprime n x}⊢ support (σ ^ n) = support σ[/STATE][TAC]output:have h : Nat.Coprime n (orderOf σ) := by apply Membership.mem.out; assumption[/TAC]Under review as a conference paper at ICLR 2025

1566
1567

1568
1569
1570
1571
1572
1573

1574
1575
1576
1577
1578
1579

1580
1581
1582
1583
1584

1585
1586
1587
1588
1589
1590

1591
1592
1593
1594
1595
1596

1597
1598
1599
1600
1601
1602

1603
1604
1605
1606
1607

1608
1609
1610
1611
1612
1613

1614
1615
1616
1617
1618
1619

Figure 13: The performance of models fine-tuned on different SFT datasets on novel premises split.
a) Mathlib-train; b) Mathlib-train + rw; c) Mathlib-train + apply; d) Mathlib-train + rw + apply.

Figure 14: a) The distribution of theorems proved by different LLMs; b) The distribution of tactics
used in the proved theorems.

30

a)b)c)d)a)b)Under review as a conference paper at ICLR 2025

1620
1621

1622
1623
1624
1625
1626
1627

1628
1629
1630
1631
1632
1633

1634
1635
1636
1637
1638

1639
1640
1641
1642
1643
1644

1645
1646
1647
1648
1649
1650

1651
1652
1653
1654
1655
1656

1657
1658
1659
1660
1661

1662
1663
1664
1665
1666
1667

1668
1669
1670
1671
1672
1673

Figure 15: The distribution of used tactics for Llama-3-8b fine-tuned on different SFT datasets to
prove miniF2F. a) Mathlib-train; b) Mathlib-train + rw; c) Mathlib-train + apply; d) Mathlib-train +
rw + apply.

31

a)b)c)d)