Alchemy: Amplifying Theorem-Proving Capability Through Symbolic Mutation
Authors: Shaonan Wu
Shuai Lu
Yeyun Gong
Nan Duan
Ping Wei
Venue: ICLR 2025 Poster (2025)
Keywords: Synthetic Data
Neural Theorem Proving
Formal Reasoning
Lean Theorem Prover
Primary area: applications to computer vision, audio, language, and other modalities
TL;DR: This work proposes Alchemy, a general framework for data synthesis that constructs formal theorems through symbolic mutations.

Abstract: Formal proofs are challenging to write even for experienced experts.  Recent progress in Neural Theorem Proving (NTP) shows promise in expediting this process. However, the formal corpora available on the Internet are limited compared to the general text, posing a significant data scarcity challenge for NTP.   To address this issue, this work proposes Alchemy, a general framework for data synthesis 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 theorem 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 perform continual pretraining and supervised finetuning on this augmented corpus for large language models. Experimental results demonstrate the effectiveness of our approach, achieving a 4.70% absolute performance improvement on Leandojo benchmark. Additionally, our approach achieves a 2.47% absolute performance gain on the out-of-distribution miniF2F benchmark based on the synthetic data. To provide further insights, we conduct a comprehensive analysis of synthetic data composition and the training paradigm, offering valuable guidance for developing a strong theorem prover.

Published as a conference paper at ICLR 2025
ALCHEMY: AMPLIFYING THEOREM-PROVING CAPA- BILITY THROUGH S SYMBLLIC MUTATION
Shaonan Wu Shuai Lu
Yeyun Gong
Nan Duan 3. Ping Wei
National Key Laboratory of Hluman-Maching Hybrid Augmented Intelligence
2 Institute of Artificial Intelligence and Robotics, Xi' an Jiaotong University Microsoft Research Asia
s haannanwustt. pingwei 0 (xixtt edu. a shuai i lu, yegong, manduan s cmicroooott.com
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 significant data scarcity challenge for NTP. To address this issue, this work proposes Alchemy, a general framework for data synthesis that constructs formal theorems through symbolic mutation. Specifically, for each can- didate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. Subsequentl, we mutate the candidate theorem by replacing the corresponding term in the statement with its equivalent form or antecedent. As result, our method increases the number of theorems in Mathlib by an order of magnitude, from 1 110k to 6M. Furthermore, we perform continual pretraining and supervised finetuning on this augmented corpus for large language models. Exper- imental results demonstrate the effectiveness of our approach, achieving a 4.70% absolute performance improvement on Leandojo benchmark. Additionally, our approach achieves 2.47% absolute performance gain the out-of-distributin miniF2F benchmark based on the synthetic data. To provide further insights, we conduct comprehensive analysis of synthetic data composition and the training paradigm, offering valuable guidance for developing a strong theorem prover.
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 al., 2024) seek to automatically generate formalized proof through neural model, known as Neural Theorem Proving (NTP). NTP represents long-standing challenge for machine learning-basee
methods (Li 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 al. 2024 Trinh al. 2024 Due to the difficulties associated with the manual formalization of theorems. formal corpora available on the Internet are relatively scarce compared the general text (Azerbayev et al. 2024). Synthetic data has shown promise in alleviating the data scarcity problem. Some works propose to directly create theorems symbolic space. For instance, WWan Deng (2020) attempts to train neural the- orem generator human- written formal theorems for the low-weighted formal system Metamath.
Other efforts focus on generating theorems based on symbolic rules (Wu et al. 2021 Trinh et al.
Work done during internship at Microsoft Research Asia.
1 corresponding author.
The code is available at
an Al chemy

---

Published as a conference paper at ICLR 2025
2024). which are restricted to specific domain of mathematics, such as inequality theorems and 2D geometry. Additionally, there are endeavors focusing on autoformalization (Xin et al., 2024 Ying et al., ) which typically translates natural language mathematical problems into formalized statements, samples correct proofs, and retrains the theorem prover iteratively. Autoformalization has yielded promising results in competition-level theorem-proving tasks through the use of large autoformalized datasets (Xin et al., 2024). However, the process of formalizing problems and re- trieving proofs is labor-intensive and cost-prohibitive. The distribution of formalized theorems is constrained by the pool of buman-collectee natural language problems and the intrinsic capabiliitiss of the model. 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 (de Moura et al. 2015 we introduce 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. Ini- tially, a new statement (function declaration) is constructed for each candidate theorem. Specifically, with the mathematical library of Lean Mathlit as seed data, aim to find a symbolic manipula- tion between two existing statements. We posit that Lean's 's tactics serve as suitable candidates for manipulation because of their efficacy in handling symbolic expressions. frw, apply) two basic tactics frequently used in theorem proving and capable of handling the equality and implication rela- tionship 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 environment. 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 D Tillustrates 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 1 1006557 to 6,326,649. 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 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- provinnggg capability of these provers on the challenging Leandojo benchmark Yang et al., 2023). Our synthetic data improve the performance by 4.70% (over 70 theorems) on the novel_ premmisss split. Furthermore, the synthesized data exhibit promise in enhancing the out- of-distribution theorem- paonnnnggonggggo ability of LLMs, as evidenced by performance increase of about 2.47% on the competition-Ievel miniF2F benchmark (Zheng et al. (2022).
Our main contributions are as follows. 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 Mathlib by an order of magnitude. Associated code has been made open- to facilitate further research in data synthesis for formal systems. Also, the syn- thesized theorems can serve as valuable supplement to Mathlib. We conduct a comprehensive evaluation on both in-distribution and out-of-distribution benchmarks, providing empirical insights to enhance the theorem provinn capabilities of LLMs.
2 RELATED WORK
Neural Theorem Proving. Proof assistants such 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. [024] Welleck & Saha 2023) Polu
& Sutskever (202)) propose to prove theorems automatically by training decoder-on 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
2

---

Published as a conference paper at ICLR 2025
Formal Knowlodge Base
Simplitied Proof Tree
Mathlib Algebra/ Atgebrralsssmmmmoo.....
theorem Nat disjoint divisors, filter isPrimePow [a b: NJ (bab a. Coprime b): Disjoint divissors, filter lsPrimePow) (b.divisons.fil lsPrimePow) by simp only FFinsct.dssjint left, Finset.mem filter, and imp, Nat.mem divisors, not and] rintro n han ha hbn hb-
(Nat.eq
dvd coprimes hab han hbn)
NL description:
two natural numbers are coprime, then sets of prime power divisons are disjoint.
ab:N
a.Coprime b
Equality
Implication
Find Invocable Theorems
Equality:
a
>.Cprrine
x.Corimn:
theorem coprime isRelPrime {m n: N) i Coprime a +* IsRelPrime in by
NL description:
For two natural numbers m and n, the property of heing coprime equivalent to the property of being relatively prime.
Implicution:
theorem coprime
mq one (b: N) [a NN a [MOD n]) Coprime by
NI. description:
If there exist natural numbers and it, such that the product congruent modulo n, then a and a are coprime.
1dtelhime xb
e:3] = [MCO 3p
Variants of Original Theorem
Construct New Theorems
Equallity-V -arriatt-
example (a b :2) IsRelPrime a b):
Disjoint (uudiiisors filter lsPrimePow) (b.divisors, filter IsPrimePaw) cm by
have Coporie b = by nw [=-Nat. isRelPrime] exact hab
ab:l x.Oayrime
ab: a.Coptine
Irplication-Varianl
example fa 1N) (o: (h:
[MOD b):
Disjoint divivissrs filter LsPrimePow) (b.divisors. filter LsPrimePow):- by have a.Coprime b > by apply Nat.coprime of nul modEq one <p> assumption
kitelhimm ab
e:N af (M0D5))
Figure I: 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 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 antecedent. At the proof tree level, our method merges two existing proof trees.
objectives (Han et al. 2022
conducting reinforcement learning (Polu et al.
2023
Xin et al. (024), refnnigg
2024
improving proof search tragedy (Lample et al.) [022]] Wang et al. [023] Xin et
the premise-selection (Mikula et al. 2024 Yang al. 2023 and so on.
Synthetic Theorem Creation. Data scareity
main challenge for NTP (Li et al. 2024). Syn- thetic data can effectively alleviate this problem alongside manual data collection (Wu et al. (2024) The current approach for synthesizing theorems diverges into two pathways. For autoformalization based methods, the prevalent statement-level autoformalization is translate 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 al. 2024). The proof-level autofor- malization (Jiang et al. 2023 Huang et al. 2024) leverages LLM to generate proof sketch, which completed by symbolic engines such as Sledgehammer (Böhme Nipkow 2010). In contrast, the second pathway focuses on synthesizing theorems in formal space. Wang & Deng (020) 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. Ww et al.) (202T) sequentially edits seed expression according to predefined set of axioms and an axiom order to create new statement, concatenating the implications from all steps to build complete proof. This method is used to create theorems on domains grounded well-established axioms, such as inequality theo- rems and ring algebra (Polu & Sutskever 2020). Beyond these works, AlphaGeometry (Trinh 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.
3

---

Published as a conference paper at ICLR 2025
Benchmarks for Theorem Proving. Most neural theorem provers based on Lean are primarily trained on Lean's 's mathematical library, Mathlib. It encompasses a broad spectrum of mathematical subjects (c.g., algebra and analysis), composed of over 1 110,000 theorems along with their respective axioms and definitions. Researchers test the capability of neural models to prove in-distribution theorems held-out set of Mathlib (Polu & Sutskever 2020 Han al. 2022 Polu al. 2023). Yang et al. (2023) creates a challenging data split of Mathlib (revelppremise 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 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. Following Polu & Sutskever (2020), we use proofstep prediction as the training objective and best-first-seacch as the search tragedy.
3.1 STATEMENT GENERATION
Find invocable theorems. Constructing new statement is the first step in creating Lean theo- rem. The candidate theorem t has a statement denoted as s. In the corresponding Lean repository, We assume that the challenge
there exists M potentially invocable theorems pinne = {t,) in creating new theorem involves effectively leveraging the possibly invocable theorem ty to mu- tate the candidate statement s. This understanding arises from two perspectives. Each theorem in Lean can be represented in the form of proof tree as presented in Fig The leaf nodes represent the assumptions, and the root node signifies the assertion. At the tree level, the task of generating new Lean theorem with existing theorems is equivalent to defining manipulations & that com- bine the proof trees of Lj and L. To streamline this process, our focus is solely on establishing the connection between the root node of ty and the Icaf node (or root node) of the candidate theorem t. From a mathematical standpoint, we can transform a target formula into an equal variant or break it down into multiple subformulas that suffice 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 with their equivalent forms or logical antecedents. For instance, consider the statement a + b > c c d, m > > m(a + b) > m[c + d) and the known theorems can derive new theorems:
>> b a+b> -+bbc+to d > 0 + mm(a+b) > (m(edd) and a > c, > d, m > 0 + m(a + 6) > m(c+ d). In summary, identifying manipulations t that use t, modify the assumptions assertion of is the primary step in constructing new statements.
ea > ex and a > c > d = a+b c+d. From these,
With their intrinsic mathematical meanings and proficiency in manipulating terms within Lean, tac- ties are promising candidates for the manipulations 4. Following the preceding discussion, we choose two frequently used basic tactics, rw and apply formulate 4.
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) or an iff' rule
ru In the presence of an identity h : a 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 hy, where h is an arbitrary assumption of the current proof state.
3 Q. rw [h]
Strictly speaking, the tactic is used to handle equality in Lean. The identity and iff are just some kinds of equality.
4

---

Published as a conference paper at ICLR 2025
Templates for instructions designed be executed in a Lean environment. We determine if a theorem is invocable by running the specific instruction.
Table I:
Tactic
Instruction Template
Description
Equality
invocable_theorem
b or = b
rW finvocable.theoren
replace all in goal with b replace all in goal with a replace all in assumption with b replace all in assumption with a
FW
rW ( invocable ]
TW
invocable_theoree at assumption
rw invocable theorem] at assumption
Implication
mnvocable.theoremt :
=
apply
set assumption as current proof goal, and try to argue backwards
have assumption := by apply invocable_theorem
apply. The apply tactic is a "suffice-to" tactic. Given an implication, 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: = 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 used to modify the assumption by deducing the implication forward. With assumption h1 P. then apply [h] at h will change h into Q which means "If P is true, then we can assert Q is true by the implication".
Algorithm Find invocable theorems
Input: candidate statement s, potential invocable theorems Tpanus instruction templates I Time {(init state, next state, instruction) ... b initialize gym-like environment and retrieve initial state
Output: invocable theorems Tinv (env, ânåt state) <- (NT
Tine <-
for t in Tpine do for i in 1 do instruction inst + FORMAT(L, nert_state and theorem t
for each instruction template
TUN_TAA(EnE,, init_state, inst)
run a tactic specified by instruction i if return a valid proof state
if VALID(nerI state) then Add (inil_state, next_state, insl) to Tino end if end for end for
To generate new statement, need to find the relationship between the candidate statement and the potentially invocable theorems Tpiar- The pseudocode outlined in Algorithm describes the main procedure find invocable theorems. The process involves initializing 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 rewrite apply the candidate theorem leveraging the instruction templates shown in Table [ Suppose the feedback from the interactive environment 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 T Tine- More information about this process described in Appendix C.2
Mutate statements. After obtaining the initial set of invocable theorems, we applied some filtering rules to Time to improve the quality of the data and lower the complexity of mutating statements. With filtered invocable theorems, we construct new statements by replacing the components with their equivalent forms or antecedents. Since we use tactics in Lean to formulate the manipulations bypassed to the Lean proof assistant. What remains is just
C, most symbolic manipulations parsing and replacing. Specifically, for the candidate statement s and instruction i, we utilize its abstract syntax tree pinpoint the exact location within the code that requires modification. Then

---

Published as a conference paper at ICLR 2025
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 are described in C.3
3.2 PROOF GENERATION AND THEOREM VERIFICATION
Mutated statements serve useful lemmas for theorem-proving only if we construct proofs that pass the verification of the proof assistant. We construct the entire proof using symbolic rules. Although neural provers other automated theorem proving tools, such hammer (Böhme Nip- kow (2 can generate more diverse proofs than rule-based methods, they are compute-intensine and do not guarantee the correctness of the generated proofs. The idea of building proof block is intuitive. Given that we only make a one-step modification to the statement, transforming the origi- nal proof state to a mutated proof state, logical approach 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 statement (the original assumption or assertion) by introducing 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 h22 P = Q, a new assumption h Q can be added by have h: = by apply hg at h exact h1- This tactic is usually used to introduce helpful lemmas when proving 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 depicted in the Appendix C.3 We construct the proof block for each mutated theorem. Then we submit the synthesized theorems 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 M variants -M-1 defined by the keyword "example" for each candidate theorem.
V {1g}اfー
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 and apply. Based on these insights, we assume that the synthetic data can serve as an augmented corpus for continual pretraining (CPT) and supervised finetuning (SFT), Specifically, fine-tune LLMs using the proofstep prediction objective proposed by Polu & Sutskever (020), 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
/- ou are proving theorem in Lean 4. ou are given the following information:
The current proof state, inside [STATE].[[/STAT]]
our task generate the next tactic the proof. Put the next tactic inside [TAC]..[/TAC]- [STATE]
[state]
[/SATTE]
[TAC]
Figure 2: Prompt template

---

Published as a conference paper at ICLR 2025
4 EXPERIMENTS
We implement the data-synthesis pipeline described in Section B for rw and apply, constructing a of variants for each candidate theorem in Mathlib. We train the LLMs on 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) Le- andojo Benchmark (Yang et al. 2023), which shares the same distributional characteristics as the seed theorems; 2) miniF2F (Zheng al., 2022). , a challenging benchmark focusing on competition- level problems that exhibits a distinct distribution 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 Mathlib4 which contains around 110k theorems the seed data for data-synthesis. Our synthesis pipeline is built upon Leandoje Fl Yang et al. 2023). a Python module that enables tracing specific Lean repository, extracting the state-tactic pairs and abstract syntax trees (ASTs), and interacting with the Lean environmen the most conee-oouumingg step of our pipeline. For rw, the time overhead amounts to 14 days using 4,096 CPU core?" 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 Onn)) 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 [8] 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 days, obtaining the additional Mate-tactic pairs by parsing the AST of each file.
[ (rum_ac API). Finding invocable theorems
Model Training. We select Llama-3-8B (Dubey et al., 2024) and deepseek-coder, coder-base-rr-... 7B (Guo et al. (024) 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 employ a linear learning rate scheduler with a 3% warm-up period and a maximum learning rate of 2c-5. We set the global batch size 256 and the cutoff length 2,048. All models are trained using Deepspeed ZeRO Stage3 (Rajbhandari et al. 2021) and Flash-Attention 2 (Dao 2024). We utilize the open-sourced codebase Llama Factory (Zheng et al., 2024) for all training experiments.
8 x H10 GPUS. We
Evaluation. We follow the evaluation setting used in Azerbayev et al. (2024). We use best- first-search as our search tragedy with a 10-minute timeout. The search budget represented as atlempt x sample x slep. Here altempl denotes the number of attempts, sample denotes the number of generated tactics per iteration, and step denotes the maximum number of steps per at- tempt. We choose 1 x 32 X 100 as scarch setting. The evaluation script is modified from an open-source implementation (Welleck) 2023) which is based on vLLM (Kwon et al., 2023) and Leandojo (Yang al. 2023). We utilize Leandojo Benchmark (Yang al. (023) 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 Leundojo. There remain 1,929 theorems in random split and 1,659 theorems in premises split. We upgrade the tool-chain version of miniF2F (Zheng al. 2022 to v4.6.0 rel.
4.2 ANALYSIS OF SYNTHETIC DATA
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 assumption. In practice, the synthesis process is divided into two stages. In the first stage, find
*cmmmit: 333077701199ccccooossaaeeeeeeae0
'version: 1.7.1
'lean-toolchain: v4.6.0 rel
7512 CPU nodes, each node has 8 cores and 56GB RAM
7

---

Published as a conference paper at ICLR 2025
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
I 110,657
5,081 ,,544
2,830,817 3,495,832
x25
56%
78,871
9,483,504
x44
37%
potential invocable theorems for each candidate theorem by running a specific tactic. In the second stage, 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 (x25 for and x44 for apply). The conversion ratios from the potential invocable theorems to the outcomes are primarily determined by the method used construct the statements and proofs. We believe that finer implementation could greatly improve the conversion ratio. Fig shows the dynamics of the distribution of mathematical subjects. The rw tactic increases the percentages of Analysis, Ring Algebra, Number Theory, and so The apply tactic mainly contributes to the fields of Analysis and Topology. Further information about synthetic data can be found in the Appendix
a)
b)
Algebra
Data
Analysis
Data
Analysis
Data
Analysis
Algebra
Topology
Topology
Order
Mesnee Thorty
caliggy Dhoar
Dacar
GhnngTeerr Theurr
Topology
Order
Ring Tirirry
Nardee
Musso Thrary
Groogg GomapTrre Throcy
Algebra
Ring Thevey
Measeelten
Ninster Thoay
Under
Limorr
Distribution of mathematical subjects. For each employed tactic, we mix the generated variants with the original theorems. a) The distribution of Mathlib, The distribution Mathlib rw. c) The distribution of Mathlib + apply.
Figure 3:
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-constree ceorrmm-construction 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, each tactic. We combine them with the training set of Leandojo (Mathlib-trainn that composes over 200k data points to form the supervised fine-tuning dataset. A detailed description of the deduplication process and training data are presented in the Appendix D.3
obtain about 30k data points for
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 different mixtures of data. As shown in Table 3, our synthetic data consistently improve the theorem theorem-proving capabilities LLMs. Com- pared with solely finetuning the training split of Mathlib, data augmentation for single tactic
8

---

Published as a conference paper at ICLR 2025
Table 3: Results on Mathlib. tidy: tactic in Mathlib that uses heuristics to complete proof. The results of tidy and GPT4 were reported in Yang et al. (2023). We select the performance of each model solely fine-tuned using Mathlib-train as the main baseline, Mathlib-traiee +x: the performance of the model pre-trained and fine-tuned on mixture of Mathlib-train and additional data about
Methods
random
novel premises
Search Budget
tidy GPT-4
23.8
5.3
29.0
7.4
X 35
Reprover Yang et al. 2023)
47.6
23.2
X 64
w/ retrieval
51.2
26.3
X 64
Ilmstep (Pythia 2.8b) (Welleck & Saha 2023
47.6
x 32
50.1
x 32
Llama3-8b
58.22
38.52
1 x 32
Mathlib-train Mathlib-train + apply Mathlib-train + apply
59.62 (+1.40)
42.13 (+3.62)
1 x 32
58.84 (+0.62)
41.29 (+2.77)
X 32
59.82 (+1.60)
43.22 (+4.70)
x 32
deepseck-coder-77bbbeee-..
57.7
39.24
1 32
Mathlib-train rw
59.25 (+1.55)
42.98 (+3.74)
x 32
Mathlib-train + apply
58.68 (+0.98)
40.51 (+1,27)
1 1x 32
Mathlib-train + rw + apply
60.39 (42.69)
43.46 (+4.22)
1 32
demonstrates a beneficial effect on the theorem- theorem-proving ability of LLMs. Moreover, the positive impacts of each tactic can cumulative. Training on the combination rw variants and apply variants results in significant performance improvement in the challenging novel_premise split of Leandojo benchmark, where the model is required to use at least one new premise to prove the target theorem (+4.70%, 78 theorems for Llama3-8b; +4.22%, 70 theorems for deepxeek-coder-7H5 base-vl.5). Our synthetic data still make a certain improvement on the random split, where the performance of models is over-estimated by allowing 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.
prove many theorems through memoriza-
4.3.2 EFFECTIVENESS 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.
590
572
660
Methods
random
novel. premises
rundom
premmisse
Llama3-8b
deepseck-coder-base-bb----
sft: mathlib-train
w/o ept
58.22
38.5 52
57.70
39.24
Nuzbe (53tttrainnd State Tacie Paira
2.5
154
366
rw
59,56 (+1.34)
42.56 (+1.04)
58.74 (+1.4)
40.69 (+1.45)
Docoronpple Didkylion
apply
58.42 (40.21)
41.29 (+2.77)
58.58 (+0.88)
40.02 (+0.78)
rw apply
59.72 (+1.50)
42.19 (+3.67)
59.67 (-1.97)
41.65 (42.41)
fft mathlib-train mw
260
w/o cpt
57.85
41.59
58.63
41.05 42.98 (+1.93)
555
Tw
59.62 (+1.77)
(40.54)
59.25 (+0.62)
330
mathlib-train apply
545
w/o ept
56.71
40.02
$7.96 58.68 (=0.72)
41.17
640
apply
58.84 (+2.13)
41.20 (x1.27)
40.51 (-066)
17%
Nuzbe
sftt mathlib-train rw + apply
w/o ept
58.53
41.95
58.37
42,92 43.46 (40.54)
Figure 4: Influence the quantity of synthesized data points.
rw apply
(+1.29)
43.22 (+1.27)
60.39 (+2.02)

---

Published as a conference paper at ICLR 2025
To examine the necessity of continual pretraining, assess and contrast the performance of the LLM on Leandojo benchmark when the pretraining stage is included versus when excluded from the experimental setup. We use models fine-tuned 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 positive influence the performance of L.LMs across diverse supervised fine-tuning settings. The experimental results indicate that continual pretraining before the supervised finetuning stage is also beneficial the mneovig-proving ability of the LLM.
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 the selected quantity (30k) achieves 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
ability lies 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-DISTRIBUTTON PERFORMANCE
We evaluate Llama-3-8h using the competition-leva theorem proving benchmark miniF2F. As shown in [5 our synthesized data still helps to improve the theorem-proving ability of LLMs on the out-o--distribution benchmark. The magnitude 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-lewe problems. Through manual inspection of the correct proofs generated by various LLMs trained on Mathlib-train. identify a tendency to favor advanced and automated tactics (e.g., simp, omega, linarith, norm num, etc.). Additionally, 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- perrem-provvig ability of LLMs. The entire analysis process is illustrated in Appendix E.2
analyze the distribution of tactics used in proved theorems across different
Table 5: Results on miniF2F. We evaluate the performance across different data compositions and list the ratio of nw, apply, horm_num and linarith used by Llama3-8b to prove these theorems.
Methods
Fi-eF2F-test
Correct/Total
rw
apply
norm num
linarith
Mathlib-train Mathlib-train +w
34.01
83/244
16.10
0.00
27.12
16.95
35.24
86/244
18.75
0.78
14.84
21.88
Mathlib-train + apply
36.07
88/244
8.87
2.42
20.16
15.63
Mathlib-train + rw + apply
36.48 (+2.47)
89/244
12.31
0.77
26.92
16.92
CONCLUSION
We have presented 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 improv- ing the theorem proninnrovingggg ability of the LLM. Synthesizing formal theorems is an inherently challeng- ing problem. Our approach, much like ancient alchemy, involves experimenting with substantial number of theorems in the hope of uncovering valuable "gold". We aspire for our algorithm to serve foundation for further research, advancing theorem synthesis from alchemy chemistry.
10

---

Published as a conference paper at ICLR 2025
ACKNOWLEDGMENTS
This research was supported by the National Natural Science Foundation of China (No. U23B2060, No.62088 622). We sincerely thank the Lean Community for providing help about this work. We also appreciate the anonymous reviewers for their helpful comments.
REFERENCES
Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen Marcus McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. In the 12th International Conference on Learning Representations, 2024.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean- Shan-Chrittophe 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.
Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement day. In the 5th International Joint Conference on Automated Reasoning, 2010.
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. In Advances in Neural Information Processing Systems, 2020.
Tri Dao. Flashattention-2: Faster attention with better parallelism and work partitioning. In the 12th International Conference Learning Representations, 2024.
Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In 25th International Conference Automated Deduction, 2015.
Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang. Angela Fan, al. The llama 3 herd of models. CoRR, abs/2447.217785 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.
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 10th International Conference on Learning Representations, 2022.
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 12th International Conference on Learning Representations, 2024.
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In the 11th International Conference Learning Repre- sentations, 2023.
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 the 29th Symposium on Operating Systems Principles, 2023.
Guillaume Lample, Timothée Lacroix, Marie-Anne Lachaux, Aurélien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. In Advances Neural Information Processing Systems, 2022.
Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. survey deep learning for theorem proving. CoRR, abs/2404.09939, 2024.

---

Published as a conference paper at ICLR 2025
Norman Megill and David A Wheeler. Metamath: A Computer language for pure mathematics, 2019. CRLLttp:: /us mee amath. wwwg//owwooaaeeeooo htt.ww/wwww///mmmmtaatatt.amaaa. wwt.//tttaaa....aaammam......... pdd.. pdf.
Maciej Mikula, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Q. Jiang, Peng Zhou, Christian Szegedy, Lukasz Kucinski, Piotr Milos, and Yuhuai Wu. Magnusham- mer: A transformer-based approach to premise selection. In the 12th International Conference on Learning Reprexentations, 2024.
Lawrence C. Paulson. Isabelle A Generic Theorem Prover, volume 828 of Lecture Notes in Com- puter Science. 1994.
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009 003993, 2020.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. In the 11th International Con- ference on Learning Representations, 2023.
Samyam Rajbhandari, Olatunji Ruwase, Jeff Rasley, Shaden Smith, and Yuxiong He. Zero-infinity: Breaking the GPU memory wall for extreme scale deep learning. CoRR, 0ans/204400855,, 2021.
Machel Reid, Nikolay Savinov, Denis Teplyashin, Dmitry Lepikhin, Timothy Lillicrap, Jean- baptiste Alayrae, Radu Soricut, Angeliki Lazaridou, Orhan Firat, Julian Schrittwieser, al. Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context. CoRR, abs/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.
Terence Tao. The polynomial freiman-ruzsa conjecture project. https://github.cr com/
teorth/pfr 2023.
Terence Tao. Machine assisted proof. Notices of the American Mathematical Society, 2024.
Trieu H. Trinh, Yuhuai Wu, Quoe V. Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nat., 625(7995):476-485 482, 2024.
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 dynamie-tree sampling guided by proof-level value function. In the 61 Annual Meeting of the Association for Computational Linguistics, 2023.
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 12th International Conference on Learning Rep- resentations, 2024.
Mingzhe Wang and Jia Deng. Learning prove theorems by learning generate theorems. In Advances in Neural Information Processing Systems, 2020.
Sean Welleck. Neural theorem proving tutorial ii https://github.. com cmu 13/ ntptutorial-IN 2023.
Sean Welleck and Rahul Saha. abs/2310.1 18457, 2023.
LLMSTEP: LLM proofstep suggestions in lean.
CoRR,
Yuhuai Wu, Albert Q. Jiang, Jimmy Ba, and Roger Baker Grosse. INT: an inequality benchmark for evaluating generalization in theorem proving. In the 9th International Conference on Learning Representations, 2021.
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Advances in Neural Information Processing Systems, 2022.
12

---

Published as a conference paper at ICLR 2025
Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. Lean- -ean-github: Compiling github LEAN reposito- ries for a versatile LEAN prover. CoRR, abs/2407.17227, 2024.
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. propeeek-prover-v1..5 Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. CoRR, 0ass/208.081155 2024.
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song. Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval- augmented language models. Advances in Neurul Information Processing Systems, 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. In Advances in Neural Information Processing Systems, 2024.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minifff: cross-system benchmark for formal olympiad-level mathematics. the 10th International Conference Learning Represen- tations, 2022.
Yaowei Zheng, Richong Zhang, Junhao Zhang, Yanhan Ye, Zheyan Luo, and Yonggiang Ma. Lla- mafactory: Unified efficient fine-tuning 100+ language models. CoRR, 2tss/2403.13372, 2024.
13

---

Published as a conference paper at ICLR 2025
CONTENTS
Background on Lean
15
Limitations
15
Detailed Information of Synthesizing Algorithms
16
Overview
16
Find Invocable Theorems
16
Construct New Theorems
18
C.3.
rw tactic
18
C.3.2
apply tactic
19
4 Verify the Theorems
20
Limitations of Synthesis Pipeline
D
Deeper Analysis of Synthetic Dataset
22
D.I Numerical Analysis
22
D.2 Examples
22
D.3
Details of Training Data
22
D.3.1
Examples of Training Data
22
D.3.2
Preprocessing
D.3.3
Classification of Extracted Tactics
23
D.3.4
Influence of the Quantity SFT Dataset
23
Additional Experiments
26
Effectiveness of Different Tactics
26
B.2
Analysis of the Tactics to Prove mini Theorems
26
Preference in Used Tactics
26
Influence of Additional Tactics
26
14

---

Published as a conference paper at ICLR 2025
A BACKGROUND ON LEAN
Lean (de Moura et al. 2015 is a functional programming language and interactive theorem prover based on dependent type theory. As one of the most popular formal systems, Lean aids mathe- maticians in formalizing statements and proofs in 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 special variant of functions in general-purpose programming languages. theorem consists of 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 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- prooinng systems focus on tactic-style proof. The synthesis method proposed by our paper can be applied to both styles.
a statement can be formatted
Tactic. Lean offers various advanced tacties 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 only one proof goal at time.
Mathlib, Mathliti is a comprehensive mathematical library for Lean, largely maintained by the community, which encompasses broad spectrum of mathematical subjects (e.g.. algebra and anal- ysis) and consists of over 110,000 theorems along with their respective axioms and definitions. This extensive knowledge base serves the primary corpus for neural theorem provers.
B LIMITATIONS
Our method exhibits some limitations that remain 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 executed 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- or Term-level. Our method synthesizes theorems from top to bottom and introduces additional state-tactic pairs of specific tactics. Synthesizing formal data at the theorem level is not efficient and not consistent with the step-by-step nature of theorem-proving Idcally, we anticipate that we can synthesize formal data directly at the term level, which aligns with the characteristics of interactive theorem proving.
Up-to-down v.s. Down-to-up. We synthesize theorems in an up-to- fashion. We construct the new statements first and then retrieve the correct proofs. The up-to-down fashion depends specific set of seed theorems, which restricts the diversity of synthetic data. A more fundamental idea is that 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-
15

---

Published as a conference paper at ICLR 2025
style idea is hard to implement in Lean and requires 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 mncorem-proving capabil- ities of LLMs. We posit that theorem synthesis in the symbolic space serves valuable com- plement to prevailing auto-formalization methods. For instance, it may contribute to the expansion of autoformalized datasets. Besides,
approach generates substantial quantity of new proven statements which can be utilized as a comprehensive database for Petrieval-Augmentee Generation (RAG) (Yang et al., 2023; Wang al., 2024). Our objective is amalgamate these methodologies to develop robust theorem prover in the future.
C DETAILED INFORMATION OF SYNTHESIZING ALGORITHMS
C.I OVERVIEW
As discussed in Section the entire algorithm is composed of four steps: 1) Find invocable theorems for the candidate theorem by executing 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 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" verify the generated theorems.
C.2 FIND INVOCABLE THEOREMS
For each candidate theorem, check whether other theorems be used rewrite apply to it by executing tactics. We use the runjac API provided by Leandojo to run a specific tactic and extract the valid proof state according predefined criteria. The instruction templates for each tactic are listed in T Here is the code snippet that illustrates this process.
args:
dojo: interactive environment
init_state: initial proot state of target theorem
theorem: a possible invocable theorem
hypos: the assumptions of the target theorem (extracted by parsing the AST)
...
def is invocable theorem in
dojo, init_state, theorem, hypes, mode="rw"
):
= theorem.fulllnaae if mode "rw";
11
12
# e.g. rw [name] at _ypo_name
13
insts = get_rw_insts (name, hypos)
elif mode -- "apply":
e.g. have hypo_str := by apply
16
insts get get_apply_inee insts (name, hypos)
17
res = I|
18
for i, inst in enumerate (insts): run_tac (init_state, inst)
try: next_state - dojoorun_tee except Exception e: else:
20
21
22
state_ing info =
"init_state": init_state $ pp means pretty-printed
"next_state"" next_state.errow if isinstance (next_state,
LeanBrror) else next_state.pp, "rule": inst
25
26
if isinstance (next_state, leankrror)
if mode Aimplication
16

---

e: Char Published as a conference paper at ICLR 2025
and "unsolved goals" in statr. res append (state_info) clif isinstance (next_state, Tasticštate):
30
31
32
res append (state_info)
return res
Listing I: Find invocable theorems by running tactics.
We set different validation criteria for each tactic. For the nw 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, the problem of constructing new theorems. Specifically, we remove the invocable theorems whose next state contains meta-variables (e.g.??a, ?m]23) for the tactic and unnamed meta-variables (e.g.,?e122 (e3844 for the apply tactic. Ultimately, we retrieve the invocable theorems for each candi- date theorem. One example of invocable theorems is shown in Fig
filter the resulting invocable theorems to simplify
theorem name: Char.ofNat toNat rule: have h: ValaidCCarr c.toNat apply List.rel of pairwise cons state:
c: Char
VsValiCCharNat (toNat e)
+- ofNat (toNat =
next state:
unsolved goals
case hp
c: Char
h isValidCharNa (toNat c)
Std.RBNode.Al is VaVaidCChara
casc
iaValidCharrat (toNat e)
+ V (x:NN,, ?lb - isValidCharNat
case
Char
h VaVaidCCarrN (toNaat c)
A.d.RBNNddelooeeBBoundd ?cut ?t ?lb
(toNat
case lb
Char
h asValiCCarrN (toNat c)
Option N
case cut
e: Char
h: isVaiiiCharNa (toNat c)
N Ordering
case
Char
isValidCharNat (toNat c)
Std.RBNode N
Figure 5: Examples of invocable theorems for apply
The experiments a large collection of CPUs (512x8-com for the tactic and 256 x 8-core for apply). The substantial CPU requirement is largely due to the memory-intensee nature Leandojo, which hinders multiprocessing single node. We anticipate significant reduction in the cost of
17

---

Published as a conference paper at ICLR 2025
experiments by implementing lighter interface for Lean interaction. The operation of apply is more complex and come-consuming than rw. We set a one-hour timeout for each dojo environment to reduce the time cost. When running specific tactic, 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 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-off's 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 source code.
C.3.1 FW TACTIC
The logic of constructing a new statement for nw 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 Construct new statement for rw tactic
Input:
candidate statement s, invocable thcorem fime mutated statement 8m
Output:
node +- EXTRACT AST(s)
extract the AST of candidate statement get the next state and instruction flag specifies whether the assumption or assertion should be mutated PARSE(node, times flag) parse AST node and locate the corresponding part that
--neet-state, inst tine
flag - IDENTIFY (i)
location
should to be mutated
mutant m < CONSTRUCT(neeat.ston
parse the next proof state and construct the target
string
new statement 8m REPLACE(ss, m,,
statement, should insert have tactic 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 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 the new one construct the whole proof. Here is simplified code snippet that illustrates this process.
After creating
def proof_geneeteeeee wwe.eeettiion... invocable inst,
flag, proci_strr str, cone_ot_hypoole--ooee is_tactic_style-ralse
): inst invocable_inst ("ruuee ["rule"]
if flag = "hypo":
hypo_name parse (inst, flag)
find the delimiter for precf ser(e.g. := by or :=) (simplifien fied version)
12
if is_tactic_style: delimiter = ":= by"
13
else:
15
delimiter ":-"
18

---

Published as a conference paper at ICLR 2025
splits proof str. split (delimiter)
17
proof_seqs seqs delimiter. (splissssss)))
18
if flag = "hypo":
19
rev_inst = reverse_rw (inyccrrwinyccclle__iss
have_template "have (subgoal) :- by {proof_seqs]
have_inst have_template. format
22
sutspal-=on___rr1ypp..0000
23
pzoof_segs=xev_inst)
24
have_inse += jexat [hype_name]'
end inst proof_
elif flag "conclusion":
27
have_template "have (subgoal) [delimiter] (proof_seqs)
28
have_inst have_template. format(
delimiteer=ellmmteer,,
31
proof_segs==rrof___
32
head = "by if not is_tactic_style else _sffix = at this;exact this"
33
end head + inst _suffix indentation
36
have_inst indent_code (del imiter, proof_str, have_inst, indent_ievel -...)
37
ena inst = indent_ (delimiter, proof_str, andinss, Indent_leved =...)
38
concat the different parts proof
39
prefix splits [0] delimiter + 'An'
40
suffix end_inst if end_inst. starstsitttttttttttot.tt (nn else Ann end_inst
new_proof prefix have_inst + suffix
return new peo_p
Listing Build the whole proof for zw tactic
C.3.2 apply TACTIC
Algorithm 3 Construct new statement for apply tactic
Input: candidate statement invocable theorem time Output: mutated statement 8m
H +-
> initialize the set of new assumptions > extract the AST of candidate statement get the next state and instruction Di get the set of metavaribales and other subgoals Assigning metavariables
node +- EXTRACT AST(s)
neat state, inst line Metaus, Goals +- PARSF(nert_statt))
for metav Metavs do
Add ASSIGN(metav, next_state to H end for
for goal Goals do
> Fill the other subgoals depending on varibblai
Add AgSIGN(goal, next stattsssteeeetee Metavs) to end for H + WAADDLE.NAMING.CONFLICCC new assumption hm +- CONCAT(H)
location + PARSE(node, tixe) be mutated
> parse AST node and locate the old assumption that needs to
8m REPLACE(S, hm,))
Constructing new statements for apply tactic is more complex than Applying theorem may introduce some metavariables and new subgoals into the local context for the resulting proof state as shown in 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 its name and type from the proof state. To avoid naming conflicts, define set of rules to rename
19

---

Published as a conference paper at ICLR 2025
the variable according the naming conversion of Mathlit Ultimately, concatenate all assumptions and replace the old assumption with them. This procedure is shown in Algorithm 3
Similarly, construct the entire proof for the new statement by inserting have lemma. The simplified code snippet illustrates this process.
def proof_generation. _op_applnnlypyapoppppppppppyy laases_gccaly inst, proof_str, is is_tactic_style)
if len (casss_
1:
1emma = inst + "; assumption"
elit Len (cases_ggoals goalss) 1:
lemma inst "<;> assumption"
else:
raise Exception (*no available case and corresponding goal")
if elttaciic_stlle
delimiter ":= by"
11
else:
12
dclimiter ";="
13
splits ato
15
proof_seqs
16
lemma indent_codes (dellimter, proof_str, lemma, indent_level= prefix sp]its[0] delimiter 'An"
17
18
suffix prooř_ seqs if proci_ wtt.seeeesssssttttt... ('aa)) else AAn"
proof seqs
19
new procf prefix 1emma suffix return new_proof
20
Listing 3: Build the whole proof for apply tatic
C.4 VERIFY THE THBOREMS
Our method creates a set of variants for each candidate theorem in Mathlib. 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 "llean" 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
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 several 96-core CPU machines.
single 8-core CPU node res = [] for idx, file in enumerate (files) "rrsile
# for each modified file
file_name: "name the lean file", text: "the content of this file after writing synthesized variants into this file"
"lac": ["theorem_name": (Istartllin__tt end add_iine_bb ... pr
tmp 'loc'; filel'loc' loc'],
10
11
ffile_name filel's file_name")
r "text'; tilel'text')
14
file_name File filel'filenaa
20

---

Published as a conference paper at ICLR 2025
file path os ps.pth.. join (mathlib package path, file name) extract old content this file "r") as f:
16
17
with (p
18
old_str = rerd
replace the old content with new content with open (felle_paaath "*")
21
F.write(fil) ['text'
22
change the build target to current file
23
with open (LIBRARY ( Matalib.Lean
'w') as F: 4 LIBRARY_ ROTT_PATH:
module_nam,
file_name, raplaaaaeeeeplacel /1, (.').replace) .lean', (()
25
(frite(("impon) (module_name)))
26
if have_variants (
*# lake build the new mathlib project wd gs.getcwd()
29
result Lake_buill btw.bbiilmmattliilppaaaaaaeaeaee os chdir (wd)
# helper function
30
## parse the output
subprocess error
if result None: tmp['valid_loc') ["No variants"]
34
elif result -- 0:
35
imp['valid_oont - tmp['loc')
36
print (' successfull build')
timeout error eli# result -1: else:
38
Loc' |NNo variants")
39
40
A find the error (ocatiens(line numbers)
pattern fr" ((file__namm)) : : (Nd+): error;"
re. findall (pattern, result)
43
if (er 0: tmp impl'valid parse exception
["Ne variants")
44
clse:
# extract line numbers from errors error_line_nt
46
47
# get the locations of all variants intervals
48
# drop the error cnes and write back
valid_locs fi write back (valid (valid_locs, tixel'text'
error_line_nbs)
51
52
## rebuilt the project if causes error then remove this
file
wd os. gs ()
result lak._bullddathhhb..ppce....ppp
55
os. chdir (wd)
56
if result != 0: tmpl' vep'vvlid_loe" ["No variants")
rebuild error
else:
pass the rebuilding process
58
tmp voei valid_locs
59
else:
60
tmpl' valid Lociddoooooo = I'No variants']
write back the original content
62
with open (file_path, "*") as
63
f.write (old_atr)
64
aesend (tmp)
Listing 4: Verify the correctness of generated theorems
C.5 LIMITATIONS 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 significant number of temporary files that consume substantial disk space when initializing "dojo" environment. The memory- memory-intensin intensive nature this tool hinders our ability to effectively implement multiprocessing: 2) Moreover, it lacks native support for tracing
21

---

Published as a conference paper at ICLR 2025
local Lean repository, must first upload our data to GitHub; 3) We encounter challenges when tracing a repository of 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 our forthcoming endeavors.
In addition, the process of constructing statements and proofs plays 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 in the future, which is more robust and easier to extend.
D DEEPER ANALYSIS OF SYNTHETIC DATASET
D.I NUMERICAL ANALYSIS
The histogram of the number of variants synthesized by each tactic is shown in Fig
FW
apply
10
Number of Theunams
Number of Drwrems
10"
10
10
10
10a
100
150
100
200
300
400
500
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 Fig
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 subset of demo theorems for reference. The proof lengths of these theorems range from to 3 lines. The synthesized theorems of rw tactic are displayed in Fig g The synthesized theorems apply are displayed Fig
D.3 DETAILS OF TRAINING DATA
D.3.1 EXAMPLES OF TRAINING DATA
As shown in Fig I0 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 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 are extracted by Leandojo rather than manually designed symbolic rules. We have not performed
22

---

Published as a conference paper at ICLR 2025
FW
apply
10090
Noster
500
2090
Maurchhery www.giighhhtmmmcc torr monnnnm
Sea offior an
Iowaaaoooooa tHE oh pare aptar the
www.tttttaiiaii.. of
Mazz MeaNeeeleeeeeee
Mallaaica WorN
14
And Ant wow.mneeeeee.......
Figure 7: The top20 theorems for rw and apply.
any post-proo 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 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 in "rw [A]" or "apply A". These data points have similar changes 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 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 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 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 QUANTITY SFT DATASET
We assess the impact varying quantities of additional state-tactics pairs for each tactic under several conditions: 1) Mathlib-train with no additional data points; 2) Downsampling with 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 deduplication threshold of 1, resulting in 30k additional data points; 5) Deduplication with a threshold of 50, resulting in 500k additional data points; and 6) No deduplication, resulting in 3M additional data points. We fine-tune Llama-3-8h 3h8h on these
23

---

Published as a conference paper at ICLR 2025
Finset.muttipliccttieeeeeggyyy right
theorem mulliplicativeEnerry mono right (ht: b):
multiplicativeEneryy ti multiplicativeEnery t :=
multiplicatiiveEneryy mono Subset.rfl ht
example (ht: b)
multiplicatveeEnery S multiplicativeEneeyy tw:= have ht: t by rw [Finset.inter sg_left] at httexact ht muliiplicatvveEnery mono Subset.rfl ht
example (ht t.val ta.val):
euulipplicatvveEneryy s ui S multiplicativeenery tazm have hi is by [+ Finset.subse def] at htıexact ht multiplicativeFnery mono Subset.rfl ht
example (ht tb):
max (multiplicativeeneryy tx) (multiplicativennenyy ti) multippicativeenneyy s tx have: multiplicativeeinery
multiplicativeennery mulipplicatveenergy mono Subset.rf by m- left iff] this;exact this
Multiset.eard card
theorem card card {s : Multiset a} (h:sst) card s card leInductionOn h lengist le
example (s : Multiset at sh:s [c: card card c:= have : card card := leInductionOn h lungist le
by [=forall It iff _if________ le'] this:exact this
example (s L: Multiset ut (h:s5(): card card card s:=
have : card s card t:= leInductionOn h Sublist.engtth le by rw [-inf eq left] thisgexact this
example {s Multiset a) (h:sst): s- card card t:
have : card $ $ card t: leInductionOn h Sublisttlength lc by rw [le or It] this;exact this
Nat.one It it_pow'
theorem one It_pow' (n m N): <m 2) (n+ I) one _ow_ltoowwww// (n + 1) (m + 2) n.suce_smee zero (Nat.lt of sub succ rfl)
example N): : (m 2) (u 1) (m 2) (n 1) 1:=
have: < (m + 2) (n 1):
one It pow (n + 1) (m + 2) n.suce zero (Nat.lt of sub eq succ rfl)
by [Nat.one
ne zero_errraaa and and_ne__dddaaaaaaaaaeeee _e__ee_on_ pe_one] at this;exact this
example N): (m +2) 2 ()< (m) (n 1) 2) I)==
have < (m + 2) ^ (n 1):= one [t_potwpwwwooo_ (n + (m + 2) n.suce__ zero (Nat.lt_of of sub suce rfl)
by rw [tNlllt mul self iff] at this;exact
Figure 8: Examples of synthesized theorems for zw
different mixtures of data and evaluate their performance random split of Leandojo Benchmark.
The experimental results are shown in Fig demonstrating that our setting achieves relatively optimal balance between overhead and performance.
24

---

Published as a conference paper at ICLR 2025
StrictMonoOn..mpstooo Ioc
lemma StrictMonnOOn.mapslu Ioc (h StrictMonoOn f (lec b)):
MapsTo F [loc b) (loc (f (fb))
fun cc he + (h (left mem_ Ice.2 <| Ih....e.trans hc.2) (loc_subsse subset Icc self he) hc. h.monotoneOn (loc subset Icc self hc) (right mem Icc.2 <| he. Ile.tans hc.2) hc.2)
example (h: StriciMomoOn I' (lcc a b) <- True):
MapsTo f (loc b) (loc af (fb)):
have StrictMonoOn flee a := by apply
true; assumption fun he + (h (left mem Icc.2 <| he. t.lssrans hc.2) (loc subset Ice self he) he. h. h.monotoneOn (locsuubset
subset Icc__elff self he) (right mem Icc.2 <| tc.t..e. hc.2) hc.2)
example (HI:
Prop). (StrictMonnon I' (lee b 1) StrictMonoOn [lec b)):
MapsTT (loc b) (loe afa) (fb))=
have h: StrictMonoOn f flece b) by apply peirce'; assumption
example (h: loc a E {x StrictMonoOn fx)): MapsTo f flac b) (loc (fa) (f))):=
have StrictMonoOn f'cee a b) :- by apply Membership.mme..ov assumption
PNat.KggdTypperrduce
theorem reduce_a {u XgedType) = 0): u.reduce u.ffiish :- by rw [reduce]
exact if _f_poss__ h
example {u XgedType) 01:01r)) u.reduce u.finish:= by have h: u.r := by apply Nat.eq_ zero of zero dvd; assumption rw [reduce]
exact if_pos h
example (u Xyed (H ubbp u.ap 1): u.reduce u.finish:= by have h: u.r ;= by apply Nat.mod_ cq_ zero_ero__oo of dvd; assumption
example (u: Xged (n N) (H: Nat.ged (r u) n= 0) u.reduce u.finish: by have h: u.r = 0 by apply Nat.eq_ _erg___er_o_o_oo__ of _edoooooeddd__e ca__e____________ zero_ _e__zeo__lftpppp>> assumption
Ordnode.not delta
theorem not le delta (s) (H: s s):
delta
le of
example
11 delta * 0=
have H: s : by apply Nat.le of dvd<>> assumption
not not_le le of
0 n)n):: S delta 0: example (s} (n N) (HI s n) (H2
have H: 1 1ss:" by apply Nat.pos of dvd of poss:> assumption
example (1 List N) (p Pairwiee LE.le 1) (a:sel) I): : s delta 0:
have H:; s = by apply List.rel of pwwrwise_consseeeee cons-c: assumption
Figure 9: Examples of synthesized theorems for apply
25

---

Published as a conference paper at ICLR 2025
Variant of Twwroryyyyrrroreee Theory.Limits, Li sigmaa condition variant_
theorem name: Category
file path: Mathlib(Category CateggoyyThooryyllooooo limits ShuntttSSSuseMeiiuuuiiiii
text:
example: MultispanIndex Siiiipaa >> Sigma.dese (it K) [Muutipunnneex..sSiigaaaaa
Signa.dese (x K)]:= by
have Map x> Sigma.desc K.t LsodSigmaMap Sigma.dese K.t := by
simp
mem, singleton] thisçexact this
meta: http:///tttubb.com/eaaooooorrrre httpb//wwwwwaaaaaa/aaaaaa//a/aan
Variant of apply
theorem name: Uniforminducing equicontinuuus variant 26
file path: Mathlib/Topology
text:
example 11:11--aa fu: Set (Set (i)) (s B)) [tg.B/oooooiicSSppeeeoooooooiaao
(hs: 1sppen (U UC Uniformlndueing) s):
Equicontionous F Equicontinuous ((u F):- by
have hu Uniformlnducing by apply Trpooggtallpuu...ooloooooooooaeo wtwp://oeeetoooooolllssseeeeeeee subsets;;>>>> assumption
congrm V rw [hu.equiicontimucusttt iff]
meta: http:///ggiaal.ooo//////ooeeeee/ www.e//ww.....oooooooooooooooooe
Figure 10: Examples of data for pretraining
E ADDITIONAL EXPERIMENTS
E. EFFECTIVENESS OF DIFFERENT TACTICS
We evaluate the effectiveness of different tactics by combining additional state-tactic pairs of 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 introduce lemmas in the process of proving theorem, helping them to prove the theorems in multiple steps. However, experimental data show that have has complex effects on the proving capacity of I.LMs. The performance 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
F.2. PREFERENCE IN USED TACTICS
To see the preference for the tactics used to prove competition-leve 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 (41%) on the test split of miniF2F benchmark. The average length 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 norm num, linarith, omega, simp, etc.). We assume that these tactics play an important role in the fncorem-proving ability of LLMMs 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-leve problems.
proved with advanced and automatic tactics in Lean (e.g.,
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 shown in Fig 15 We assume that increasing the
26

---

Published as a conference paper at ICLR 2025
Table The effectiveness of different tacties
Methods
random
novel premises
Search Budget
Llama3-8b
Mathlib-train
58.22
38.52
x 32
FW tactic
Mathlib-train rw
57.85 (-0.37)
41.59 (+3.07)
X 32
Mathlib-train + have
58.27 (+0.05)
41.29 (42.77)
1 x 32
Mathlib-train + rw have
57.96 (-0.26)
41.53 (43.01)
1 x
apply tactic
Mathlib-train + apply
56.71 (-1.51)
40.02 (+1.51)
1 x 32
Mathlib-train + have
57.44 (-0.78)
39.24 (+0.72)
1 x 32
Mathlib-train apply have
57.23 (-0.99)
38.34 (-0.18)
1 1 32
both tactic
mathlib-train rw + apply
58.53 (+0.31)
41.95 (43.44)
1 x 32
degnsekk-oder-7--besee--.
Mathlib-train
57.7
39.24
x 32
FW tactic
Mathlib-train rw
58.63 (+0.93)
41.05 (+1.81)
x 32
Mathlib-train + have
58.11 (+0.41)
39.06 (-0.18)
1 x 32
Mathlib-train have
58.74 (+1.04)
40.57 (+1.33)
1 x 32
apply tactic
Mathlib-train + apply
57.96 (+0.26)
41.17 (+1.93)
1 x 32 x
Mathlib-train + have
57.02 (-0.68)
39.66 (+0.42)
Mathlib-train + apply have
58. (+0.46)
39.78 (+0.54)
1 x 32
both tactic
Mathlib-train + rw + apply
58.37 (+0.67)
42.92 (43.68)
1 x 32
Table 7: The results of miniF2F for different LLMs. We fine-tune each model with the random train-splic of Leandojo benchmark and evaluate their performance miniF2F benchmark.
Methods
miniF2F-test
Llama-3-8b
34.01
deepseck-coddr-bass---b-
37.70
Srepseek-math-7bbee
34.42
Ilemma-7b
32.38
mistral-7b
32.38
internlm2-math-7b
36.06
Combination
40.98
diversity of synthesized tactics and adjusting the tactic distribution will be beneficial to enhance the theorem-proving ability of LLMs.
27

---

Published as a conference paper at ICLR 2025
instruction:
You are proving theorem in Lean 4. You are given the following information:
The current proof state, inside [[SAAE]
Your task generate the tactic in the proof. Put the next tactic inside [TAC]-.[/TAC]
-/
rw tactic
input:
[STATE]
a: Type u
Type 2
R Type 3_3
st: Finset
a B
n:N
insit Decidablelg
this : s.card = e+ x yx.y}
s.card = + Sct.range x (x. y3, Exists [/STATE]
[TAC]
output:
rw [=SStt.eeiiee exists range iff] at this[/TAC]
apply tuctic
input:
[STATE]
n:N
instf NeZero n
b ZMod n
w val b HAdd.hAdd (val a) Nat.le
in val a val [/SATEE] [TAC]
output:
apply cesmmasSTopreimagg///
Figure 11: Examples of rw and apply data points for finetuning
28

---

Published as a conference paper at ICLR 2025
instruction:
You are proving theorem Lean 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 lactic inside [TAC]_.PTTAC]
have raclie-r
Case
imput:
[STATE]
mnab:: N
cop: Coprime
aa
hb: Int.toNat 0 +m+bbe m
[/STATE] [TAC]
output:
have hb : b 0= by rw [Int.toNat zero] at hbçexact hb[/TA]
Case
input:
[STATE]
Type
instt DecidableEq a
A Finset (Finset a)
vvaa:: Finset a
r:N
huv Equiv.swap u.card v.card Equiv.refl N
Finset
(compress u v a).card a.card
[/SAATE]
[TAC]
output: have huv u.card v.card: = by rw [Equiv.swap eq reft iffl at huv:exact hwv//TA]
have tactic-apply-reltted
Input:
[STATE]
a: Type u
p: Type
inst+': DecidableEq
instt: Fintype a
Perm
n:N
orderOf {x Nat.Coprime x)
+ support (ar n) support
[/SAATE]
[TAC]
output:
have Nat.Copri n (orderOf a) : by apply Membership.mmmm.oom out; assumption[/TAC]
Figure 12: Examples of have data points for finetuning
29

---

Published as a conference paper at ICLR 2025
180
500
400
680
480
Tipikup
HiscTwwg
320
430
1000
1002
Thens
Tapkker
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.
b)
41:60
norm num
50
Jinarith
40-
620
gonla Riternal devide
have
omega simp
fedd. sime
10
4000
musied apirim
matid hander
cumbona sigedoo
nasiau Audertion
Figure 14: a) The distribution of theorems proved by different LLMs; b) The distribution of tactics used in the proved theorems.
30

---

Published as a conference paper at ICLR 2025
b)
norm zum
num
num
linarith
linarith
Flw
havo
Holl stop
norm num
omega
have
Meds simp
grab
d)
norm mum
norm num
linarith
linarith
have
intarral cIans
nw
norm numi
omega
Milebali
have
field simp
omigga
Siat
Figure 15: The distribution used tactics for Llama-3-8h fine-tuned on different SET datasets to prove miniF2F. a) Mathlib-train; b) Mathlib-train rw; Mathlib-train apply; d) Mathlib-train rw apply.
31


Reviews:
[{"review_id": "ura8LOZ0Nv", "reviewer": "Reviewer_EDxu", "summary": "This paper introduces a symbolic method called Alchemy to augment formal theorem proving data. Specifically, it mutates \"the candidate theorem by replacing the corresponding term in the statement with its equivalent form or antecedent\", which increases the number of theorem in mathlib4 from 110k to 6M. After continual pre-training and supervised fine-tuning with the generated data, it improves downstream performances (pass rate) on standard theorem proving benchmarks such as mathlib-test and miniF2F from 2.5% to 5%.", "questions": "How do you explain a Conversion Ratio of only 37% while the idea seems to work with a theoretical guarantee (i.e. 100%)?\nDo you think a framework like Alchemy is the correct way to significantly improve NTP to face challenging problems such as IMO problems?", "limitations": "", "rating": 6, "confidence": 5, "soundness": 4, "presentation": 3, "contribution": 2, "strengths": "Some originality: This is a good and new attempt for augmenting a human-written library (although similar ideas have been applied for \"pure symbolic and from scratch\" methods for generating theorems such as INT, HTPS-Equations and AlphaGeometry)\nGood quality: the paper is well written and all settings are of high relevance\nGood clarity: the paper is presented in a clear manner. The experimental setting and results are presented in a standard way and easy to follow\nFair significance: The improvement on pass rate on mathlib-test and miniF2F is consistent, with almost all differences being positive compared with the baseline.", "weaknesses": "1. Poor improvement: although the improvement on pass rate is consistent, it's very limited: ranging from 0.62% to 4.7% on mathlib and only 2.47% on miniF2F (34.01% to 36.48%). This is pretty marginal in terms of improvement.\n2. Narrow application possibility: the approach highly replies on a library of existing equivalence (or implying) theorems and their usage in proofs of other theorems.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "1pU65rHB7E", "reviewer": "Reviewer_FuWS", "summary": "The paper concerns data augmentation for neural theorem proving. The authors propose a method for augmenting theorem statements and the set of (state, tactic) examples given a collection of Lean statements and proofs. Their method augments theorem statements by (1) rewriting expressions in hypotheses or the statement's goal using a rewrite tactic with a suitable premise, (2) replacing a hypothesis with a different set obtained with an apply tactic with a suitable premise. It augments proofs by undoing the rewrite and/or apply and introducing a have statement, which sometimes introduces new (state, tactic) examples.\n\nThe authors apply their augmentations to Mathlib, and finetune models with (1) continued pretraining on mathlib plus the augmented statements and proofs, followed by (2) finetuning on (state, tactic) examples from Mathlib plus those from their augmentations. \n\nThe models that have undergone continued pretraining and (state, tactic) finetuning outperform the same models when they have only undergone (state, tactic) finetuning on Mathlib alone. For example, there is a 2.69% improvement on the random LeanDojo test split, and a 4.22% improvement on the novel_premises split with DeepSeek Coder.", "questions": "Please see the questions above discussed in the Weaknesses. In particular, if the authors can provide a strong response to the questions regarding the experimental setup I would be willing to raise my score.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "Originality\n- The idea of synthesizing new theorem statements through rewrites and applies is new (as far as I'm aware). \n\nQuality\n- Aside from the concerns discussed below, the experiments were carried out well for several variants while adhering to standard benchmarks and search algorithm protocols.\n- Implementing modifications to data extraction in Lean is likely nontrivial.\n\nClarity\n- The data synthesis methodology was explained clearly.\n\nSignificance\n- Lack of data is widely regarded as a core issue in neural theorem proving. Augmenting data using symbolic techniques is a potential approach to alleviating this issue, and the authors demonstrate a first step in this direction.\n- The general direction of augmenting data using symbolic techniques is interesting and under-explored.", "weaknesses": "As mentioned in the strengths above, the general direction of augmenting data using symbolic techniques is interesting and under-explored. I have two primary concerns: (1) the experimental evaluation of the proposed techniques; (2) the data augmentation techniques explored in the current paper. \n\n### Experimental evaluation\n1. **Baselines**: the baseline method is a LM finetuned on (state, tactic) pairs from Mathlib. However, the proposed method does (i) continued pretraining and (ii) (state, tactic) finetuning. As a result it is difficult to interpret the main results, since there are two finetuning methodologies used. How does the baseline method perform after continued pretraining on Mathlib (without augmentation), followed by (state, tactic) finetuning on Mathlib (without augmentation)?\n\n2. **Possible train-test overlap**: The LeanDojo benchmark consists of theorems from Mathlib. Therefore, there is potential train-test overlap in at least two places. \n    - (i) First, the continued pretraining dataset, if it includes theorems from the LeanDojo test set (or premises used in the novel_premises split). How was train-test overlap prevented for continued pretraining? I wasn't able to find details on exactly what was done for continued pretraining, so it would be great to clarify this.\n    - (ii) Second, the rewrites and applies may use premises that are \"novel\" in the novel_premises split. How do you ensure that these are not used in the data augmentation process?\n\nAs a result of (i) and (ii), it is difficult to interpret the improvement on the novel premises split. Namely, (i) and (ii) may have exposed the model to the premises required in this split, which would negate the purpose of the split. Moreover, (i) may lead to improvements on the random split as well.\n\n3. **Finetuning hyperparameters**. This is perhaps less important than (1) and (2), but the augmented dataset leads to more gradient updates compared to finetuning on the non-augmented dataset, since finetuning is performed for a fixed number of epochs. Do the results change if the baseline is finetuned for the same number of steps as the model finetuned on the augmented dataset?\n\n### Data augmentation techniques\n1. The computational cost is very high; it takes 14 days for the rw operation on 512 CPU nodes. To make the authors' method more practical, it would have been nice to see some innovation that makes the extraction faster (either at the algorithmic level or the implementation level).\n\n2. Currently the methods only modify the statement goal using 1 step of rewriting. The overall scientific contribution could be made stronger with more exploration of techniques (e.g., at least > 1 step of rewriting). Could you clarify why only the 1-step rewriting and apply were explored? I realize that it is hard to say how many techniques are needed (and it's always nicer to have more), so this is less of a concern for me than the experimental evaluation of the two techniques described above.\n\n3. From what I understand, proofs are only modified by introducing a have statement that reverses the 1-step augmentation, and then the proof is the same as the original. Again it would be nice to see additional innovation in this direction.\n\n4. It was unclear why each technique helped on unseen_premises split; could you give an intuition or an analysis of why it might help?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "voaOsEhioE", "reviewer": "Reviewer_BkaD", "summary": "This paper introduces Alchemy, a framework to generate synthetic theorem data by applying symbolic mutations to existing theorems within Lean’s Mathlib. By mutating known theorems through symbolic operations, Alchemy expands the theorem corpus by an order of magnitude (from 110k to over 6M theorems). The authors evaluate Alchemy’s effectiveness on theorem-proving tasks, reporting a 5% improvement on the Leandojo benchmark and a 2.5% gain on the out-of-distribution miniF2F benchmark (to 36.48% test accuracy).", "questions": "1. Given the modest improvement in miniF2F accuracy, are there metrics or quality checks available to assess the mathematical value or diversity of the generated theorems beyond correctness?\n2. Which specific theorems in miniF2F were newly proved by the models fine-tuned with Alchemy data? This would provide insights into the areas where synthetic training data are particularly beneficial.\n3. Given the computational demands, are there potential optimizations in the synthesis process to reduce the time and resources required for theorem mutation?\t\n4. How do you avoid the data contamination problem in the evaluation/generation phase?\n\n[1] Xin, Huajian, et al. \"DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search.\" arXiv preprint arXiv:2408.08152 (2024). \n[2] Ying, Huaiyuan, et al. \"Lean Workbook: A large-scale Lean problem set formalized from natural language math problems.\" arXiv preprint arXiv:2406.03847 (2024).", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The approach is technically robust, with well-documented use of symbolic mutations (specifically rw and apply tactics) to ensure the correctness of new theorems by construction. The improvements seen on Leandojo and miniF2F benchmarks support the framework’s validity.\n2. Alchemy significantly increases the number of available theorems in Mathlib, scaling up to 6 million theorems through systematic symbolic mutations. This large corpus helps address the issue of limited formal proof data for theorem-proving models. By providing a synthetic theorem corpus directly in the symbolic space, Alchemy addresses a key limitation in neural theorem proving, especially in formal languages like Lean where data is scarce and difficult to formalize manually.\n3. The limitations of the approach, such as data diversity and computational cost, are clearly addressed.", "weaknesses": "1. Marginal Gains in Benchmark Performance: Despite generating millions of new theorems, the gains in miniF2F accuracy are limited to 2.5%, notably lower than the >60% accuracy achieved by SOTA models such as DeepSeekProver and InternLM Prover. This modest improvement raises questions regarding the utility and quality of the synthetic theorems for real-world theorem-proving tasks.\n2. Computational Cost: The process of generating and verifying theorems is highly resource-intensive. The implementation reports substantial computational overhead, with 14 days on 4,096 CPU cores for rw mutations and 7 days on 2,048 cores for apply mutations, potentially limiting the accessibility and scalability of Alchemy in practice.\n3. Lack of Quality Metrics for Synthetic Theorems: Although Alchemy generates a large corpus, there is limited analysis of the quality or mathematical significance of the produced theorems. Without metrics or evaluation methods beyond correctness by construction, it is challenging to assess whether the synthetic theorems provide meaningful, diverse training examples.\n4. Limited Innovation Beyond Mutation: The paper relies heavily on mutating existing theorems via basic rw and apply tactics, which may restrict the variety of new insights or concepts that the synthetic data introduces. Advanced tactics (e.g., simp, linarith) and some premise selection approaches are critical in solving more challenging problems, especially in competition-level mathematics. Without these, the generated dataset might lack the depth needed to fully improve theorem-proving performance on complex out-of-distribution tasks.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "3NO63pIHyZ", "reviewer": "Reviewer_NSyk", "summary": "The paper proposes a new method to synthesize theorem training data for improving LLM's ability in theorem-proving. Given an existing theorem, the proposed method finds theorems that can imply its assumptions and assertions. Then, it replaces the corresponding assumptions/assertions and invokes these theorems to obtain the expanded new theorem. Experiments show the proposed method can generate 5M data and improve 7b models by a 2-4% pass rate.", "questions": "Why many generated theorems not pass the Lean prover? Since the generation process is based on symbolic replacement, I suppose most of the theorem should pass the prover.", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The paper is well-written and easy to understand. It has a clear motivation and proposes a novel method to generate a lot of new theorem data.\n\n- The experimental results validate the effectiveness of the generated data. It can improve current LLMs by >4% pass rate on the novel_premises split.", "weaknesses": "The method seems unable to generate diverse theorem data. It mainly expands existing theorem by combining other theorems. The diversity problem may result in a lower improvement on the harder benchmark miniF2F. I guess the generated theorem can be very different from the original theorem if it has a deep variant proof tree. Authors may show the depth statistics of the generated theorem or other statistics to verify the diversity of the generated theorem.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)