Alchemy: Amplifying Theorem-Proving Capability Through Symbolic Mutation

## Abstract

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 5% absolute performance improvement on Leandojo benchmark.
Additionally, our synthetic data achieve a 2.5% absolute performance gain on the out-of-distribution miniF2F benchmark.
To provide further insights, we conduct a comprehensive analysis of synthetic data composition and the training paradigm, offering valuable guidance for developing a strong theorem prover.

## 1 Introduction

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

The key challenge of theorem-proving lies in data scarcity (Li et al., ; Trinh et al., ). Due to the difficulties associated with the manual formalization of theorems, formal corpora available on the Internet are relatively scarce compared to the general text (Azerbayev et al., ).
Synthetic data has shown promise in alleviating the data scarcity problem. Some works propose to directly create theorems in symbolic space.
For instance, Wang & Deng () attempts to train a neural theorem generator on human-written formal theorems for the low-weighted formal system Metamath.
Other efforts focus on generating theorems based on symbolic rules (Wu et al., ; Trinh et al., ), which are restricted to a specific domain of mathematics, such as inequality theorems and 2D geometry.
Additionally, there are endeavors focused on autoformalization (Xin et al., ; 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.
However, the process of formalizing problems and retrieving proofs is labor-intensive and cost-prohibitive.
The distribution of formalized theorems is constrained by the pool of human-collected natural language problems and the intrinsic capabilities of the model.
Compared to autoformalization, synthesizing theorems in symbolic space is a more direct process without intermediate translation, and is also easier to scale up to large, cost-effective CPU units.

Building upon the advanced Lean theorem prover, we introduce a general method that synthesizes theorems directly in symbolic space.
We analogize theorem synthesis to constructing functions in general programming language and adopt an up-to-down approach.
Initially, a new statement (function declaration) is constructed for each candidate theorem. Specifically, with the mathematical library of Lean Mathlib4(^1^11https://github.com/leanprover-community/mathlib4) as seed data, we aim to find a symbolic manipulation $\Phi$ between two existing statements.
We posit that Lean’s tactics serve as suitable candidates for manipulation $\Phi$ because of their efficacy in handling symbolic expressions.
$\{rw,apply\}$ are basic tactics frequently used in theorem proving and capable of handling the equality and implication relationship between terms.
We assign both tactics to the set of manipulations $\Phi$ 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 1 illustrates the entire procedure of our algorithm.
This algorithm is executed on a large CPU-only computing unit for several days.
Our method increases the number of theorems in Mathlib by an order of magnitude from 110,657 to 6,326,679. This significant increase in the number of theorems demonstrates the potential of creating theorems in symbolic space.

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

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

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

## 2 Related Work

##### Neural Theorem Proving

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

##### Synthetic Theorem Creation

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

##### Benchmarks for Theorem Proving

Most neural theorem provers based on Lean are primarily trained on Lean’s mathematical library, Mathlib. It encompasses a broad spectrum of mathematical subjects (e.g., algebra and analysis), composed of over 120,000 theorems along with their respective axioms and definitions. Researchers test the capability of neural models to prove in-distribution theorems on a held-out set of Mathlib (Polu & Sutskever, ; Han et al., ; Polu et al., ). Yang et al. () creates a challenging data split of Mathlib (novel_premise split) which requires testing proofs to use at least one premises not seen in the training stage and mitigates the over-estimated phenomena in the traditional setting of evaluation (random split). Another widely-used benchmark, miniF2F, (Zheng et al., ) 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 function bodies possess precise mathematical meanings.
The initial step in creating a new theorem involves formulating a theorem statement (function declaration) that defines the essence of the theorem.
Then, one must verify its correctness by generating a proof block (function body) and submitting it to the proof assistant for validation. The resulting theorems that pass type checking can serve as supplementary data for training a neural theorem prover.

### 3.1 Statement Generation

##### Find invocable theorems

Constructing a new statement is the first step in creating a Lean theorem.
The candidate theorem $t$ has a statement denoted as $s$.
In the corresponding Lean repository, there exists a set of potentially invocable theorems $T_{p}=\{t_{i}\}_{i=0}^{N}$.
We assume that the challenge in creating a new theorem involves effectively leveraging the possibly invocable theorem $t_{i}$ to mutate the candidate statement $s$.
This understanding arises from two perspectives.
Each theorem in Lean can be represented in the form of a proof tree as presented in Fig 1. The leaf nodes represent the assumptions, and the root node signifies the assertion. At the tree level, the task of generating a new Lean theorem with existing theorems is equivalent to defining operations $\Phi$ that combine the proof trees of $t_{i}$ and $t$. To streamline this process, our focus is solely on establishing the connection between the root node of $t_{i}$ and the leaf 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 to prove the original formula, by employing the equality or “only if” relationship between formulas. The mathematical interconnections between formulas provide heuristic insights on how to mutate $s$ to create a new theorem. Similarly, we can substitute the terms in $s$ with their equivalent forms or logical antecedents.
For instance, consider the statement $a+b>c+d,m>0\rightarrow m(a+b)>m(c+d)$ and the known theorems $a>b\iff e^{a}>e^{b}$ and $a>c,b>d\implies a+b>c+d$. From these, we can derive new theorems: $a+b>c+d,m>0\rightarrow e^{m(a+b)}>e^{m(c+d)}$, and $a>c,b>d,m>0\implies m(a+b)>m(c+d)$.
In summary, identifying operations $\Phi$ that use $t_{i}$ to modify the assumptions or assertion of $s$ is the primary step in constructing new statements.

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

- •
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) rules(^2^22Strictly speaking, the rw tactic is used to handling equality in Lean, the identity and iff are just some kinds of equality.). In the presence of an identity $h:a=b$ or an iff rule $h:P\iff Q$, rw [h] substitutes all occurrences of term on the left side of equality in the proof goal with term on the right side. The direction of substitution can be reversed by adding a back arrow in the bracket (rw [$\leftarrow$ h]). The target of rewriting can also be changed using at, e.g. rw [h] at $h_{1}$, where $h_{1}$ is an arbitrary assumption of the current proof state.
- •
apply The apply tactic is a “suffice-to” tactic. Given an implication, it will match the consequent with the proof goal. If matched, it will transform the goal into the antecedent of the implication. With an implication rule $h:P\implies Q$ and a proof goal $Q$, then apply [h] will reduce the goal to proving $P$, which means that “proving P suffices to prove Q by implication”. Similarly, apply can be used to modify the assumption by deducing the implication forward. With assumption $h_{1}:P$, then apply [h] at $h_{1}$ will change $h_{1}$ into $Q$, which means “If P is true, then we can assert Q is true by the implication”.

Figure: Algorithm 1 Find invocable theorems

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

**Table 1: Templates for instructions designed to be executed in a Lean environment. We determine if a theorem is invocable by running the specific instruction.**
| Tactic | Instruction Template | Description |
| --- | --- | --- |
| rw | Equality invocable_theorem : $\mathbf{a=b}$ or<br>$\mathbf{a\iff b}$ |  |
| rw [invocable_theorem] | replace all $a$s in goal with $b$ |  |
| rw [$\leftarrow$invocable_theorem] | replace all $b$s in goal with $a$ |  |
| rw [invocable_theorem] at assumption | replace all $a$s in assumption with $b$ |  |
| rw [$\leftarrow$invocable_theorem] at assumption | replace all $b$s in assumption with $a$ |  |
| apply | Implication invocable_theorem : $\mathbf{a\implies b}$ |  |
| have assumption := by apply invocable_theorem | set assumption as current proof<br>goal, and try to argue backwards |  |

##### Mutate statements

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

### 3.2 Proof Generation and Theorem Verification

Mutated statements can serve as useful lemmas for theorem-proving only if we can construct proofs that pass the verification of the proof assistant.
We construct the entire proof using symbolic rules.
Although neural provers and other automated theorem proving (ATP) tools (e.g., hammer) can generate more natural and diverse proofs than rule-based methods, they are compute-intensive and do not guarantee the correctness of the generated proofs. The idea of building a proof block is intuitive. Given that we only make a one-step modification to the statement, transforming the original proof state to a mutated proof state, a logical approach is to reverse the mutation and utilize the original proof to complete the remaining proving process.
We use have tactic to restore the modified part of a statement (the original assumption or assertion) by introducing a lemma.

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

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

### 3.3 Model Training

Regarding the synthetic data, we have two observations. At the theorem level, the synthetic data comprises numerous theorems, each with statement distinct from existing theorems. At the state-tactic level, the process of constructing proofs introduces additional state-tactic pairs, primarily centered on rw and apply.
Based on these insights, we assume that the synthetic data can serve as an augmented corpus for continual pretraining and supervised finetuning.
Specifically, we fine-tune LLMs using the proofstep prediction objective proposed by Polu & Sutskever (), 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 (), as shown in Fig.2.

Figure: Figure 2: Prompt template
Refer to caption: x2.png

## 4 Experiments

We implement the data-synthesis pipeline described in Section 3 for rw and apply, constructing a set of variants for each candidate theorem in Mathlib. We train the LLMs on a mixture of human-written theorems and synthetic ones. To examine the effectiveness of synthetic data, we evaluate the theorem prover on two benchmarks that are widely adopted by the research community: 1) Test split of Mathlib, which shares the same distributional characteristics as the seed theorems; 2) miniF2F, a challenging benchmark focusing on competition-level problems that exhibits a distinct distribution 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(^3^33commit: 2iufd 3c307701fa7e9acbdc0680d7f3b9c9fed9081740) which contains 116,695 theorems as the seed data for data-synthesis.
Our synthesis pipeline is built upon Leandojo(^4^44version: 1.7.1) (Yang et al., ), a Python module that enables tracing a specific Lean repository, extracting the state-tactic pairs and abstract syntax trees (ASTs), and interacting with the Lean environment(^5^55lean-toolchain: v4.6.0 rc1) (run_tac API). Finding invocable theorems is the most time-consuming step of our pipeline. For rw, the time overhead amounts to 14 days using 4,096 CPU cores(^6^66512 CPU nodes, each node has 8 cores and 56GB RAM). For apply, it takes 7 days at this stage using 2,048 CPU cores with a one-hour timeout for each theorem. The substantial time cost is attributed to the $O(n^{2})$ complexity of our algorithm and the memory-intensive characteristics of Leandojo. We believe this overhead could be greatly reduced through a more meticulous implementation. After retrieving the invocable theorems, we construct new statements and proofs for the target theorems in approximately an hour using 24 CPU cores. We then write back the mutated theorems and compile the enlarged repository through lake build, utilizing 2,048 CPU cores. We retrieve the error messages returned by Lean, which can be parsed to locate the wrong theorems. Finally, we trace the enlarged repository on a 96-core machine for 3 days, obtaining the additional state-tactic pairs by parsing the AST of each file.

##### Model Training

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

##### Evaluation

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

### 4.2 Analysis of Synthetic Data

**Table 2: Number of theorems. Stage one: the number of invocable instructions for all candidate theorems. Stage two: the number of theorems that pass the verification of the Lean theorem prover.**
| Tactic | Candidate theorems | Stage one | Stage two | Expansion | Conversion Ratio |
| --- | --- | --- | --- | --- | --- |
| rw | 110,657 | 5,081,544 | 2,830,817 | $\times 25$ | 56% |
| apply | 78,871 | 9,483,504 | 3,495,832 | $\times 44$ | 37% |

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

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

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

### 4.3 Experimental Results

#### 4.3.1 Main Results

**Table 3: Results on Mathlib. tidy: a tactic in Mathlib that uses heuristics to complete a proof. We select the performance of each model solely fine-tuned using Mathlib-train as the main baseline. Mathlib-train + x: the performance of the model pre-trained and fine-tuned on a mixture of Mathlib-train and additional data about x.**
| Methods | random | novel_premises | Search Budget |
| --- | --- | --- | --- |
| tidy | 23.8 | 5.3 | - |
| GPT-4 | 29.0 | 7.4 | $1\times 35$ |
| Reprover (Yang et al., ) | 47.6 | 23.2 | $1\times 64$ |
| w/ retrieval | 51.2 | 26.3 | $1\times 64$ |
| llmstep (Pythia 2.8b) (Welleck & Saha, ) | 47.6 | - | $1\times 32$ |
|  | 50.1 | - | $2\times 32$ |
| Llama3-8b | 58.22 | 38.52 | $1\times 32$ |
| Mathlib-train + rw | 59.62 (+1.40) | 42.13 (+3.62) | $1\times 32$ |
| Mathlib-train + apply | 58.84 (+0.62) | 41.29 (+2.77) | $1\times 32$ |
| Mathlib-train + rw + apply | 59.82 (+1.60) | 43.22 (+4.70) | $1\times 32$ |
| deepseek-coder-7b-base-v1.5 | 57.7 | 39.24 | $1\times 32$ |
| Mathlib-train + rw | 59.25 (+1.55) | 42.98 (+3.74) | $1\times 32$ |
| Mathlib-train + apply | 58.68 (+0.98) | 40.51 (+1.27) | $1\times 32$ |
| Mathlib-train + rw + apply | 60.39 (+2.69) | 43.46 (+4.22) | $1\times 32$ |

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

#### 4.3.2 Effectiveness of Continual Pretraining

**Table 4: Effectiveness of continual pre-training. We grouped the dataset for CPT and SFT by the tactic employed in the additional state-tactic pairs.**
| Methods | random | novel_premises | random | novel_premises |
| --- | --- | --- | --- | --- |
|  | Llama3-8b | deepseek-coder-base-7b-v1.5 |  |  |
|  | sft: mathlib-train |  |  |  |
| w/o cpt | 58.22 | 38.52 | 57.70 | 39.24 |
| rw | 59.56 (+1.35) | 42.56 (+4.04) | 58.74 (+1.04) | 40.69 (+1.45) |
| apply | 58.42 (+0.21) | 41.29 (+2.77) | 58.58 (+0.88) | 40.02 (+0.78) |
| rw + apply | 59.72 (+1.50) | 42.19 (+3.68) | 59.67 (+1.97) | 41.65 (+2.41) |
|  | sft: mathlib-train + rw |  |  |  |
| w/o cpt | 57.85 | 41.59 | 58.63 | 41.05 |
| rw | 59.62 (+1.76) | 42.13 (+0.54) | 59.25 (+0.62) | 42.98 (+1.93) |
|  | sft: mathlib-train + apply |  |  |  |
| w/o cpt | 56.71 | 40.02 | 57.96 | 41.17 |
| apply | 58.84 (+2.13) | 41.29 (+1.27) | 58.68 (+0.73) | 40.51 (-0.66) |
|  | sft: mathlib-train + rw + apply |  |  |  |
| w/o cpt | 58.53 | 41.95 | 58.37 | 42.92 |
| rw + apply | 59.82 (+1.30) | 43.22 (+1.27) | 60.39 (+2.02) | 43.46 (+0.54) |

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

#### 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 quantities of additional data points, on novel_premises split of Leandojo benchmark. As shown in Fig 4, the selected quantity (30k) achieves a relatively optimal compromise between the performance and overhead. The experimental results also reveal that enlarging the quantity of state-tactic pairs of a single tactic tends to lead to rapid saturation. We assume that the key to continually improving the theorem-proving ability lies in keeping the diversity of tactics during the process of scaling the synthetic data. More details are presented in Appendix D.3.4.

#### 4.3.4 Analysis of Out-of-distribution Performance

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

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

## 5 Conclusion

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

## Appendix A Background on Lean

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

##### Theorem in Lean

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

##### Tactic

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

##### Mathlib

Mathlib(^7^77https://github.com/leanprover-community/mathlib4) is a comprehensive mathematical library for Lean, largely maintained by the community, which encompasses a broad spectrum of mathematical subjects (e.g., algebra and analysis) and consists of over 120,000 theorems along with their respective axioms and definitions. This extensive knowledge base serves as the primary corpus for neural theorem provers.

## Appendix B Limitations

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

##### Data Diversity and Quality

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

##### The Cost of Synthesizing

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

##### Single-Round v.s. Multi-Round

Theoretically speaking, our algorithms can be iteratively 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-level 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.
Ideally, 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-down fashion. We construct the new statements first and then retrieve the correct proofs. The up-to-down fashion depends on a specific set of seed theorems, which restricts the diversity of synthetic data.
A more fundamental idea is that we can sample some terms in the symbolic space directly, merge them using symbolic manipulations, and then find the corresponding goals for this new theorem.
This AlphaGeometry-style idea is hard to implement in Lean and requires a large amount of domain knowledge and engineering endeavors.

##### Symbolic Synthesis in Conjunction with Other Techniques

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

## Appendix C Detailed Information of Synthesizing Algorithms

### C.1 Overview

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

### C.2 Find Invocable Theorems

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

Figure: Listing 1: Find invocable theorems by running tactics.

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

Figure: Figure 5: Examples of invocable theorems for apply
Refer to caption: x5.png

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

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

### C.3 Construct New Theorems

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

#### C.3.1 rw tactic

The logic of constructing a new statement for rw tactic is simple. We just identify whether a specific assumption or assertion has been rewritten by parsing invocable instructions with regular expressions. 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.

Figure: Algorithm 2 Construct new statement for rw tactic

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

Figure: Listing 2: Build the whole proof for rw tactic

#### C.3.2 apply tactic

Figure: Algorithm 3 Construct new statement for apply tactic

Constructing new statements for apply tactic is more complex than rw. Applying a theorem may introduce some metavariables and new subgoals into the local context for the resulting proof state as shown in Fig 5. We assign values to the metavariables by parsing the next_state and then retrieve all subgoals containing metavariables as new assumptions. For each new assumption, we can extract its name and type from the proof state. To avoid naming conflicts, we define a set of rules to rename the variable according to the naming conversion of Mathlib(^8^88https://leanprover-community.github.io/contribute/naming.html). Ultimately, we concatenate all new assumptions and replace the old assumption with them. This procedure is shown in Algorithm 3.

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

Figure: Listing 3: Build the whole proof for apply tatic

.

### C.4 Verify the Theorems

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

Figure: Listing 4: Verify the correctness of generated theorems

### C.5 Limitations of Synthesis Pipeline

Our synthesis pipeline is mainly based on the advanced Leandojo tool. We use it to interact with Lean, parse abstract syntax trees and trace state-tactic pairs. However, this tool has the following weaknesses. 1) It will generate a significant number of temporary files that consume substantial disk space when initializing a “dojo” environment. The memory-intensive nature of this tool hinders our ability to effectively implement multiprocessing. 2) Moreover, it lacks native support for tracing a local Lean repository, so we must first upload our data to GitHub. 3) We encounter challenges when tracing a repository of a scale significantly larger than that of Mathlib, which makes it hard to do multi-round synthesis. We aspire to enhance the functionality of the Leandojo tool to tackle more demanding scenarios in our forthcoming endeavors.

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

## Appendix D Deeper Analysis of Synthetic Dataset

### D.1 Numerical Analysis

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

Figure: Figure 6: The distribution of the number of variants (only 99% of the data are visualized).
Refer to caption: x6.png

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

Figure: Figure 7: The top20 theorems for rw and apply.
Refer to caption: x7.png

### D.2 Examples

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

Figure: Figure 8: Examples of synthesized theorems for rw
Refer to caption: x8.png

The synthesized theorems of apply are displayed in Fig 9.

Figure: Figure 9: Examples of synthesized theorems for apply
Refer to caption: x9.png

### D.3 Details of Training Data

#### D.3.1 Examples of Training Data

As shown in Fig 10, we synthesize a series of variants for each candidate theorem by employing different tactic instructions to mutate existing theorems. We simply combine these additional theorems with the original theorems in Mathlib and train LLMs on this augmented corpus.
In addition to synthesizing variants for each candidate theorem, symbolic manipulations to construct new theorems 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 any post-processing on the extracted state-tactic pairs.
We group the extracted theorems by the employed tactics (rw, apply, have). The examples of rw and apply are shown in Fig 11. The examples of have are shown in Fig 12.

Figure: Figure 10: Examples of data for pretraining
Refer to caption: x10.png

Figure: Figure 11: Examples of rw and apply data points for finetuning
Refer to caption: x11.png

Figure: Figure 12: Examples of have data points for finetuning
Refer to caption: x12.png

#### D.3.2 Preprocessing

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

#### D.3.3 Classification of Extracted Tactics

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

#### D.3.4 Influence of the Quantity of SFT Dataset

We assess the impact of varying quantities of additional state-tactics pairs for each tactic under several conditions. 1) Mathlib-train with no additional data points; 2) Downsampling with a ratio of 0.25, resulting in 7.5k additional data points; 3) Downsampling with a ratio of 0.5, resulting in 15k additional data points; 4) Our setting with a deduplication threshold of 1, resulting in 30k additional data points; 5) Deduplication with a threshold of 50, resulting in 500k additional data points; and 6) No deduplication, resulting in 3M additional data points. We fine-tune Llama-3-8b on these different mixtures of data and evaluate their performance on random split of Leandojo Benchmark. The experimental results are shown in Fig 4, demonstrating that our setting achieves a relatively optimal balance between overhead and performance.

## Appendix E Additional Experiments

### E.1 Effectiveness of Different Tactics

**Table 6: The effectiveness of different tactics**
| Methods | random | novel_premises | Search Budget |
| --- | --- | --- | --- |
| Llama3-8b |  |  |  |
| Mathlib-train | 58.22 | 38.52 | $1\times 32$ |
| rw tactic |  |  |  |
| Mathlib-train + rw | 57.85 (-0.37) | 41.59 (+3.07) | $1\times 32$ |
| Mathlib-train + have | 58.27 (+0.05) | 41.29 (+2.77) | $1\times 32$ |
| Mathlib-train + rw + have | 57.96 (-0.26) | 41.53 (+3.01) | $1\times 32$ |
| apply tactic |  |  |  |
| Mathlib-train + apply | 56.71 (-1.51) | 40.02 (+1.51) | $1\times 32$ |
| Mathlib-train + have | 57.44 (-0.78) | 39.24 (+0.72) | $1\times 32$ |
| Mathlib-train + apply + have | 57.23 (-0.99) | 38.34 (-0.18) | $1\times 32$ |
| both tactic |  |  |  |
| mathlib-train + rw + apply | 58.53 (+0.31) | 41.95 (+3.44) | $1\times 32$ |
| deepseek-coder-7b-base-v1.5 |  |  |  |
| Mathlib-train | 57.7 | 39.24 | $1\times 32$ |
| rw tactic |  |  |  |
| Mathlib-train + rw | 58.63 (+0.93) | 41.05 (+1.81) | $1\times 32$ |
| Mathlib-train + have | 58.11 (+0.41) | 39.06 (-0.18) | $1\times 32$ |
| Mathlib-train + rw + have | 58.74 (+1.04) | 40.57 (+1.33) | $1\times 32$ |
| apply tactic |  |  |  |
| Mathlib-train + apply | 57.96 (+0.26) | 41.17 (+1.93) | $1\times 32$ |
| Mathlib-train + have | 57.02 (-0.68) | 39.66 (+0.42) | $1\times 32$ |
| Mathlib-train + apply + have | 58.16 (+0.46) | 39.78 (+0.54) | $1\times 32$ |
| both tactic |  |  |  |
| Mathlib-train + rw + apply | 58.37 (+0.67) | 42.92 (+3.68) | $1\times 32$ |

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

Figure: 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.
Refer to caption: x13.png

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

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

#### E.2.1 Preference in Used Tactics

**Table 7: The results of miniF2F for different LLMs. We fine-tune each model with the random train-split of Leandojo benchmark and evaluate their performance on miniF2F benchmark.**
| Methods | miniF2F-test |
| --- | --- |
| Llama-3-8b | 34.01 |
| deepseek-coder-base-7b-v1.5 | 37.70 |
| deepseek-math-7b-base | 34.42 |
| llemma-7b | 32.38 |
| mistral-7b | 32.38 |
| internlm2-math-7b | 36.06 |
| Combination | 40.98 |

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

#### E.2.2 Influence of Additional Tactics

We analyze the distribution of used tactics in proven miniF2F problems across different data compositions. The dynamics of distribution changes are shown in Fig. 15. We assume that increasing the diversity of synthesized tactics and adjusting the tactic distribution will be beneficial to enhance the theorem-proving ability of LLMs.

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

## Peer Reviews

confidence: 5
contribution: 2
initial_rating: 6
presentation: 3
questions: How do you explain a Conversion Ratio of only 37% while the idea seems to work with a theoretical guarantee (i.e. 100%)?
Do you think a framework like Alchemy is the correct way to significantly improve NTP to face challenging problems such as IMO problems?
soundness: 4
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)
Good quality: the paper is well written and all settings are of high relevance
Good clarity: the paper is presented in a clear manner. The experimental setting and results are presented in a standard way and easy to follow
Fair significance: The improvement on pass rate on mathlib-test and miniF2F is consistent, with almost all differences being positive compared with the baseline.
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%.
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.
2. Narrow application possibility: the approach highly replies on a library of existing equivalence (or implying) theorems and their usage in proofs of other theorems.

---

confidence: 4
contribution: 3
initial_rating: 5
presentation: 3
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.
soundness: 3
strengths: Originality
- The idea of synthesizing new theorem statements through rewrites and applies is new (as far as I'm aware). 

Quality
- Aside from the concerns discussed below, the experiments were carried out well for several variants while adhering to standard benchmarks and search algorithm protocols.
- Implementing modifications to data extraction in Lean is likely nontrivial.

Clarity
- The data synthesis methodology was explained clearly.

Significance
- 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.
- The general direction of augmenting data using symbolic techniques is interesting and under-explored.
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.

The 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. 

The 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.
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. 

### Experimental evaluation
1. **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)?

2. **Possible train-test overlap**: The LeanDojo benchmark consists of theorems from Mathlib. Therefore, there is potential train-test overlap in at least two places. 
    - (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.
    - (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?

As 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.

3. **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?

### Data augmentation techniques
1. 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).

2. 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.

3. 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.

4. It was unclear why each technique helped on unseen_premises split; could you give an intuition or an analysis of why it might help?

---

confidence: 4
contribution: 3
initial_rating: 5
presentation: 3
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?
2. 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.
3. Given the computational demands, are there potential optimizations in the synthesis process to reduce the time and resources required for theorem mutation?	
4. How do you avoid the data contamination problem in the evaluation/generation phase?

[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). 
[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).
soundness: 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.
2. 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.
3. The limitations of the approach, such as data diversity and computational cost, are clearly addressed.
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).
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.
2. 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.
3. 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.
4. 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.

---

confidence: 3
contribution: 3
initial_rating: 8
presentation: 3
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.
soundness: 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.

- The experimental results validate the effectiveness of the generated data. It can improve current LLMs by >4% pass rate on the novel_premises split.
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.
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.

Meta-review: This paper concerns data augmentation for theorem proving in Lean through symbolic rewriting of hypotheseses and proofs. Evaluations performed on Mathlib datasets show that, with data augumentation, further pretraining and finetuning improves the performance by 2.69% on the random LeanDojo test split and 4.22% on the novel_premises split. Augmenting training data for theorem proving through rewrites and applies is a novel contribution. Given the augmentation only performs one step rewriting, leaving the augumented theorems and proofs nearly identical to the original ones, there is a concern that whether the fine-tuned model will generalize. Other concerns are possible train-test overlap and data contamination. New results shared during the rebuttal partially addresses some of these concerns (e.g., train-test overlap). Overall, this paper makes valuable contributions with relatively marginal improvement by data augmentation for neural theorem proving.

Decision: Accept (Poster)