LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Authors: Kaiyu Yang
Aidan M Swope
Alex Gu
Rahul Chalamala
Peiyang Song
Shixing Yu
Saad Godil
Ryan Prenger
Anima Anandkumar
Venue: NeurIPS 2023 Datasets and Benchmarks Oral (2023)
Keywords: Automated Reasoning
Theorem Proving
Retrieval-Augmented Language Models
TL;DR: We introduce open toolkit, benchmarks, and retrieval-augmented language models for theorem proving in Lean.

Abstract: Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. However, existing methods are difficult to reproduce or build on, due to private code, data, and large compute requirements. This has created substantial barriers to research on machine learning methods for theorem proving. This paper removes these barriers by introducing LeanDojo: an open-source Lean playground consisting of toolkits, data, models, and benchmarks. LeanDojo extracts data from Lean and enables interaction with the proof environment programmatically. It contains fine-grained annotations of premises in proofs, providing valuable data for premise selection—a key bottleneck in theorem proving. Using this data, we develop ReProver (Retrieval-Augmented Prover): an LLM-based prover augmented with retrieval for selecting premises from a vast math library. It is inexpensive and needs only one GPU week of training. Our retriever leverages LeanDojo's program analysis capability to identify accessible premises and hard negative examples, which makes retrieval much more effective. Furthermore, we construct a new benchmark consisting of 98,734 theorems and proofs extracted from Lean's math library. It features challenging data split requiring the prover to generalize to theorems relying on novel premises that are never used in training. We use this benchmark for training and evaluation, and experimental results demonstrate the effectiveness of ReProver over non-retrieval baselines and GPT-4. We thus provide the first set of open-source LLM-based theorem provers without any proprietary datasets and release it under a permissive MIT license to facilitate further research.

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Kaiyu Yang', Aidan M. Swope', Alex Gu Rahul Chalamala's | Peiyang Song", Shixing Yu², Saad Godil, Ryan Prenger", Anima Anandkumar CCattech, 2NVIDIA, MIT, "UC Santa Barbara, SUT Austin https://leandbjo..cm
Abstract
Large language models (LLMs) have shown promise proving formal theorems using proof assistants such as Lean. However, existing methods are difficult to reproduce or build on, due to private code, data, and large compute requirements. This has created substantial barriers to research machine learning methods for theorem proving. This paper removes these barriers by introducing LeanDojo: open-source Lean playground consisting of toolkits, data, models, and bench- marks. LojnDojo extracts data from Lean and enables interaction with the proof environment programmatically. It contains fine-grained annotations of premises in proofs, providing valuable data for premise selection- a key bottleneck theorem proving. Using this data, develop ReProver (Retrieval-Augmented Prover): LLM-based prover augmented with retrieval for selecting premises from a vast math library. It is inexpensive and needs only GPU week of training. Our retriever leverages LeanDojo's s program analysis capability to identify accessible premises and hard negative examples, which makes retrieval much tive. Furthermore, we construct a new benchmark consisting of 98,734 734 theorems and proofs extracted from Lean's math library. features challenging data split requiring the prover to generalize to theorems relying on novel premises that are never used in training. We use this benchmark for training and evaluation, and experimental results demonstrate the effectiveness of ReProver over non-retrieval baselines and GPT-4. We thus provide the first set of open-source LLM-based theorem provers without any proprietary datasets and release it under permissive MIT license to facilitate further research.
effec-
Introduction
Reasoning is cornerstone of human intelligence and a fundamental goal of AI (3 One prominent task is automated theorem proving (ATP): automatically generating proofs for theorems expressed formal logic. ATP useful for formal mathemattcs, producing mathematical proofs that can be checked rigorously [].. Furthermore, it underpins formal verification, which is essential for proving the correctness and safety of high-stakes applications 6).
ATP is challenging since the search space is prohibitively large. In many applications, it is impractical generate proofs fully automatically. Therefore, interactive theorem proving (ITP) has emerged as an alternative paradigm. In ITP, proofs are constructed by human experts interacting with software tools called proof assistants, such as Coq 77, Isabelle [ and Lean [ Machine learning can automate such interactive theorem proving, opening up new avenue for theorem proving [9]. The model can learn to interact with proof assistants, given data containing human mimannwwittenn proofs.
Research conducted while Saad Godil was at NVIDIA.
37th Conference on Neural Information Processing Systems (NeurIPS 2023) Track on Datasets and Benchmarks.

---

Prove theorems by Interaction
Proof tree
context Goal
prd n
ged 0
KiM
tk 11 linke
Data extraction
Lean Benchmark
roold
unfile
98,734 theorems and proofs
Training
god 1i 1)=b-
129,26 premises
Machine learning model
reomiee sad
aopty aed
State
god [IK + 1) Ik 4 k+
Cencor
Encedendecdd
rew mod
occessible lirrayy
Toctic
Sbeccen HiLE 1.
Breoder
Ercoder
Eireoon aed In. (e (aar) by sand ( Sascees and svit (a se5? a 2.a
33K on average
similrity
Chrooss and aquat, 3t Ca nat3 K. lasseus aucc.aod
Brooder
Recrieved premises
Figure 1: Top right: LeanDojo extracts proofs in Lean [ into datasets for training machine learning models. also enables the trained model prove theorems by interacting with Lean's proof environment. Top left: The proof tree of a Lean theorem A' e N, ged
= n, where ged is the greatest common divisor (details in Sec. 3 When proving the theorem, we start from the original theorem as the initial state (the root) and repeatedly apply tactics (the edges) to decompose states into simpler sub-states, until all states are solved (the leaf nodes). Tactics may rely on premises such as mod_se]] self and gcd_ zero_lettrre defined in a large math library. E.g., mod_self is existing theorem Vn N, n %
used in the proof to simplify the goal. Bottom: Our ReProver model (S.c.5). Given state, it retrieves premises from the math library, which are concatenated with the state and fed into an encoder-decoder Transformer to generate the next tactic.
Formal theorem proving serves an important challenge for machine learning. From computer science perspective, formal proofs can be treated as programs [10]. But unlike conventional programs in C++ or Python, the correctness of proofs can verified using proof assistants. Therefore, theorem proving may be considered special form of code generation, with rigorous evaluation and no room for the model hallucinate. This can be consequential current large language models (LLMs), as they have demonstrated exceptional capability in code generation [11] but have flaws in factuality and hallucination [2]. In addition, augmenting I.I.S with external tools, such as proof assistants, has shown promise in improving their various capabilities, including multi-step reasoning 13
Current research on LLMs for theorem proving is facing many barriers. To our knowledge, none of the existing LLM-based provers are open-source [14H21]. They all use private pretraining data, and the compute requirements can reach thousands of GPU days [17. Furthermore, some rely on tailored infrastructure for distributed training and interaction with the proof aasiisaattbbo are not possible fully reproduce without open- code [7 We change the status quo by introducing LeanDojo: open-source toolkits, models, and benchmarks that give researchers access to state-of-the-ar L.L.- provers with modest computational costs.
Tools for Data Extraction and Interaction. We focus on Lean, proof assistant popular among mathematicians Our framework LeanDojo provides two essential functions for learning- based theorem proving (Fig.) M extracting data and enabling models interact with Lean programmatically.
For data extraction, Dojo extracts training data not directly visible in the raw Lean code (Fig. 2. e.g., proof trees consisting of intermediate states between proof steps (Fig. Top left). In addition, LeanDojo is the first tool to locate premises in Lean proofs, enabling training machine learning models for premise selection. For interaction, LeanDojo turns Lean into a gym-like interactive environment 22] Using LeanDojo. the model can observe proof states, change the state by executing
"Leean" in our paper refers to Lean 3 by default. Lean 4 is not backward-come eooppail but is also supported by LeanDojo. Our Lean 4 results in Appendix D

---

proof steps (referred to as "tactics" in proof assistants), and receive feedback from Lean. LeanDojo the first tool capable of interacting with Lean reliably, reducing proof-checking errors in existing tools 19 (correct proofs misjudged as incorrect) from 21.1% % to 1.4%.
Retrieval-Augmented LLMs for Theorem Proving. LeanDooo addresses a key bottleneck in theorem proving: premise selection [23 24]. Existing LLM-based provers generate the next proof step (tactic), taking only the current state as input. However, proving theorems depends critically on the premises, such as lemmas and definitions, from a math library.
For example, Fig. (Top left) illustrates the proof of "vn E N, ged n = n", where ged stands for greatest common divisor. The proof starts from the original theorem as the initial state and repeatedly applies tactics to decompose states into simpler sub-states, until all states are solved. Tactics may rely on premises such as mod_ self and ged_zero left defined in large math library. E.g., mod_self is an existing theorem "V'n E N, n % n = O" useful for simplifying the goal.
Incorporating all possible premises is too large to fit into LLMs' input, given the limited context window. Existing methods must learn to memorize the association between the proof state and the name mod_self. It works if the premise has been used in the training data to solve similar goals, but does not generalize to truly novel scenarios, e.g., theorems requiring lemmas unseen in training.
One potential solution is to complement memorization with explicit premise selection. LeanDojo extracts premise data from Lean, including where they are defined and used. It enables us to tackle premise selection by augmenting LLMs with retrieval. We introduce ReProver (Retrieval-Augment Prover) (Fig. T Bottom): Given the current state, it generates a tactic conditioning on a small number of premises retrieved from Lean's math library, mathlib 25
We need to limit retrieval to a small number of premises for to be effective, and ideally, they should contain the ground truth premise. Our retriever builds upon Dense Passage Retriever (DPR) [26) but incorporates two algorithmic innovations: First, not all premises are accessible when proving a theorem (Sec. 3. LeanDojo can perform program analysis on Lean code to determine accessible premises. On our data, that reduces the average number of premises from 128K to 33K, significantly simplifying the retriever's 's task. Second, DPR needs negative examples in training and benefits from hard negatives, ie.. irrelevant premises that are hard to distinguish from ground truth ones. We propose in-file negatives: simple mechanism to find hard negatives in premise selection, which samples negative premises defined in the same Lean source file as the ground truth premise.
LeanDojo Benchmark. Using LeanDojo, we construct a benchmark containing 98,734 theorem- s/proofs extracted from mathlib. Our benchmark is one of the largest math-focused dicorem-proving datasets. We find that the common practice of splitting theorems randomly into training/testing has led to an overestimated performance in the previous papers. LLMs can prove seemingly difficult theorems simply by memorizing the proofs of similar theorems during training. In LeanDojo Bench- mark, we mitigate this issue by designing challenging data split requiring the model to generalize to theorems relying on novel premises that are never used in training.
We use LeanDojo Benchmark to train and evaluate ReProver. Training takes only five days single GPU. In evaluation, ReProver can prove 51 31.2% theorems, outperforming a baseline that generates tactics directly without retrieval (47.6%) and another baseline using GPT-4 (27) to generate tactics in zero-shot manner (9..%) We also test ReProver on two existing datasets, MiniF22 (28) and ProofNet (29). It can prove 26.5% 5 theorems in MiniF2F and 13.8% in ProofNet, which is competitive with state-of-the-art methods without reinforcement learning [19), even though trained using far fewer resources. Moreover, it can prove 65 theorems that currently do not have proofs in Lean. Thus, our tool can also serve as an effective tool for augmenting existing math libraries in Lean.
Contributions. In summary, we make four main contributions: First, we introduce tools for extracting data from and interacting with Lean. Second, we develop ReProver, the first retrieval- augmented language model for theorem proving. Third, we construct a challenging benchmark for learning-bast based theorem proving and use it to validate the effectiveness of ReProver. Finally, we facilitate open research on LLMs for theorem proving by releasing our data, model, and code. Our method does not rely on private datasets and can be trained on a single GPU within a week. We believe this will significantly lower the barriers to academic research in this area and establish the first accessible baselines for future work to build upon. Further, our method can be used to automatically generate new Lean proofs without requiring human effort.
3

---

2 Related Work
Theorem Proving. Classical provers express theorems in first-order logic and search for proofs automatically in a large space 30 B1]. Even with data-driven search heuristics [32] they fail to scale to large formalization projects. Therefore, recent work on learning-based theorem proving has focused on an alternative paradigm: automating the interaction with proof assistants.
The architecture of learning- bastn provers progressed from classical machine learning algorithms such as KNN [3],, to graph neural networks explicitly encoding the syntax of formal expressions [2] and now Transformer-based LLMs treating expressions plain strings [4]. Besides the model architecture, researchers have explored several complementary dimensions: proof search algorithms for assembling model-generated steps into complete proofs 17 21]; overcoming data scarcity through reinforcement learning (RL) [7 19 36 outsourcing some proof goals classical provers [8 43). Our base model without retrieval is a combination of straightforward design choices. It generates tactics by finetuning an encoder-decoder Transformer, ByT5 [44), via supervised learning without RL or auxiliary data. Then it searches for proofs using best-first search. Our model's algorithmic novelty lies in the retrieval.
37 or synthetic/auxiliary data [16] 38 40]; as well
Premise Selection.
Selecting useful premises is recognized as key challenge in theorem prov- Machine learning methods for premise selection have also progressed from 48), recurrent neural networks (24). graph neural networks [38], to Trans- However, cxisting methods either tackle premise selection in isolation without feed the premises to a symbolic prover 41 47 49]. To our knowl- edge, we are the first to augment a learning- based formal theorem prover with retrieved premises so them effectively. For example, it can decide whether to
ing 23
24
45
46).
classical models [4]
47
formers 49 50
theorem proving 24
38
that the prover learn how explicitly retrieved premise or an implicitly memorized one.
Data and Tools for Theorem Proving. Tools for data extraction and interacting with proof assistants have been crucial drivers of learning-basee theorem proving. Existing tools and datasets can be divided by proof assistants: Coq has GamePad [51]. CoqGym [9], and PRISM [52]; Isabelle has IsarStep (53) and PISA [5]; HOL Light has HOList (54) and HoLStep (55), and Lean has
LeanStep [16] and lean- gym [19.. MiniF2F (28) is the only cross-system dataset, with 488 theorems
for evaluation. However, it does not have training theorems and is restricted to the domain of math olympiads.
Among available tools extracting data from proof assistants, LeanDojo is the only one that can extract premises for retrieval-augmented theorem proving. A few existing datasets also have premises [49 (4), but their data extraction tools are not public, making difficult to construct new datasets. In addition, LoanDojo is the only tool that can interact with Lean robustly (Sec. 4 and can extract data from Lean 4. See Appendix A.3 for a detailed comparison between LeanDojo and alternatives.
Mathematical Reasoning in Natural Language. We focus on proving theorems expressed in formal logie, whereas researchers have also produced plethora of work on mathematical reasoning in natural language [56] 63 A particularly relevant task is autoformalization, translating natural language texts into formal theorems and proofs 22 72).
Retrieval-Augmenter Language Models. Our ReProver is the first retrieval -arreeeelaugmmented language model for formal theorem proving, though similar architectures have been studied extensively in
NLP 73 In addition, there have been many retrieval-augmenner methods for code generation (82- 88 Most of them retrieve from corpus directly related the current file, e.g., GitHub Stack Overflow. In contrast, our retrieval corpus consists of premises accessible to the current file, which is determined by program analysis using LojnD This is similar what CoCoMIC (88 does for Python. However, their retrieval is based on heuristics, whereas ours is learned.
Background: Theorem Proving in Lean
At high level, Lean is programming language that allows you to write not only conventional programs but also theorems and proofs. To that end, it provides two pieces of machinery: First, it provides a unified language for defining programs, mathematical objects, theorems, and proofs, based on functional programming with dependent types [89]. Second, provides a tactie system for constructing machine-checkable proofs semi-automen cemi-automatically.

---

data/nat/lemaas.len
theoren mod_aelr (n. nat) X
begin [nod_eq_euu___ sub__sub__ee (le_refl ,), nat. bat.subbeelle zero_nod]
Math library
end
data/nat/god.len
def ged nat nat nat.
god
7 y god (y & (x
Case 1:
thaoran gcd_zero_lefs (x pat)
ged
bagin simp [gcd] end
theoren ged_self (a nat) ged
begin
Import
cases n,
unfold ged },
unfold ged,
resrite ael,
apply ged_ _eft end
Figure 2: Definition of greatest common divisor (ged) in Lean and two related theorems. The proof of ged_sell (between "begin" and "end") relies on premise mod_self imported from another file in the math library. Lean can run this proof to produce the proof tree in Fig left).
We use a simple example Fig. 2 to illustrate how theorems are formalized and proved Lean Here we want to formalize the greatest common divisor (ged) of two natural numbers. First, we define ged as recursive function, taking two natural numbers as parameters and returning their ged via the _leff Euclidean algorithm. Then, we state lemma named gcd_zero zef__left that Vz E N, ged 0 x x. which can be proved simply by the definition of ged. Finally, we state main theorem ged_self that Vn E N, ged n n n, followed by its proof consisting of five tactics. In theorem proving, we only concerned with generating the proof, i.e., the part between "begin" and "end"; everything before "begin" " is known, including other files imported.
The syntax of tactics is quite expressive. They can take arguments and can be combined into compound tacties. You can think of tacties as programs a domain-specific language (DSL.). Users can extend the DSL by defining new tactics. This discrete, combinatorial, and unbounded action space makes theorem proving challenging for machine learning.
Another challenge is premise selection. Premises are existing lemmas or definitions useful for proving theorem. They are used as arguments in tacties. For example, in Fig. and Fig. (Top left), the tactic "rewrite mod_self" rewrites the goal using the premise mod_ se_eef. which is defined in another file imported by the current file. Proofs cannot use premises that haven't 't been defined. For example, ged_self cannot be used to prove ridd_eero_eef_ not imported to the current file. Still, premises come from a large math library containing hundreds of thousands of existing definitions and theorems, making it hard, for humans and machines alike, to select the right premises when generating tactic. This a key bottleneck in theorem proving and what we aim to address through retrieval-auge -aievvee- LLMs.
In addition, they cannot use premises
4 LeanDojo: Toolkit and Benchmark
LeanDojo serves two essential needs of learning-based theorem proving in Lean. First, it extracts training data from Lean, and we use this capability to construct a challenging theorem proving benchmark. Second, it enables the model interact with Lean programmatically.
Data Extraction. Lean repos (c.g., mathlib or Lean-liquid liquidd contain source code of human- written theorems/proofs. However, the raw code unsuitable for training the prover. lacks runtime information that humans can access when using Lean, such intermediate states between proof steps. Therefore, LeanDojo extracts the following information not directly visible the code:
Thhe process is similar in many other proof assistants, though they may have different logical foundations.
5

---

File dependencies and abstract syntax frees (ASTs): LeanDojo processes the repo to produce a directed acyclic graph whose nodes are files and edges are import relations between files. In addition, LeanDojo produces the AST of each file. File dependencies and ASTs are useful for program analysis, e.g., collecting theorems defined in file or premises accessible to theorem.
States and tactics:
LeanDojo extracts all tactics in proofs. For each tactic, also extracts the states before/after the tactic, which allows us to reconstruct the proof tree Fig. (Top left).
Premises: For each premise, such as mod_ self in Fig. LeanDojo records where it is defined (location in data/nat/ /1emma..eeaa and where it used used (locations across many files). In addition, premises have unique fully qualified names (e.g.. nat mod_self) but are often used by ambiguous short names mmod_self), relying on Lean to perform name resolution. LeanDojo is capable of recording their full names.
Lean has basic support for exporting dependencies, ASTs, states, and tactics. However, it cannot resolve the premises' full names and locate their definitions. Therefore, we modify Lean to record this information (details in Appendix(A.1) The modified Lean is used only for data extraction but not for evaluation, so we do not risk accidentally breaking Lean's logical soundness.
LeanDojo Benchmark. We construct benchmark for premise selection and theorem proving, named LeanDojo Benchmark. The data extracted from mathlib Lean's 's centralized math library covering diverse topics such as analysis, algebra, and geometry LeanDojo Benchmark is one of the largest math-focused theorem proving datasets, consisting of 98,734 theorems from 3,384 Lean files. Unlike existing datasets in Lean [16]. LeanDojo Benchmark also contains the definitions of 130,262 premises. including not only theorems but also other definitions that can be used as premises (e.g.. ged in Fig. 2 Furthermore, the dataset has 217,776 tactics, 129,243 of them with at least one premise. The average number of premises 2.13 among tactics with premises. Appendix contains additional information on data format, datasheet [00, hosting, and licensing.
stng/algebra/guuteriion...
Lenma conj_mul (a b) con b.con] c.no
begin
ext: simp; ring_exp
end
lemma conj_conj_mm (a.conj * b) b).conj = b.conj * := begin rw [con]_mul, conj_conj] end
Lemma conj_mul_conj (a b.con)) .cojj a. conj begin
Iw [conj_mut mull conj_conj]
end
Figure 3:
Similar theorems/proofss are common. If splitting them randomly into training/tessinng, the model can prove testing theorems by memorization.
LeanDojo Benchmark has 94,734/2,000/2.000 theorems for training/valiccatoo//esingg It features a challenging data split for testing the prover's generalization in more realistic scenarios. Splitting theorems randomly can overestimate the prover's performance, by allowing to prove many theorems through memorization. In human--ritter Lean code, common idiom is to have block of similar theorems/proofs for slightly different properties of the same math concept. For example, in Fig. 3 the last two theorems not only look similar but have identical proofs. If one of them is in training, the model can easily prove the other one by memorization. This shortcut enables the model to prove seemingly nontrivial theorems, including those requiring premises to prove.
To mitigate this issue, besides the random split, we create a challenging data split named novel_premised It requires testing proofs to use at least one premise that has never been used in training. For example, the last two theorems in Fig. 3 both use the premise conj mul. If one theorem is in the training set of the noveelppremiie split, the other one must also be in training.
We use commit wtt.aaeeeeaaeaee000044000000eeea released on October 11, 2023. Moore details, statistics, and visualizations of mathlib can be found al github. io/mathlib berbbbtttsssttte html
communityymy

---

Interacting with Lean. Another important function of LeanDojo is to interact with Lean program- matically. It turns Lean into gym-like environment [22]. in which the prover can observe the proof state, run tactics to change the state, and receive feedback on errors on proof completion. This environment indispensable for evaluating/deploying the prover or training it through RI..
Below is LeanDojo's main interface for interacting with Lean through tactics. Lean also supports other proof styles not based on tactics. Although we only support tactic-style proofs, they are sufficiently general since any proof can be converted to a tactic-style proof
initiall ize (theorem): Given the theorem to prove, LeanDojo returns the initial state, A valid state is string representing current proof goals and local contexts (see the nodes in Fig. Top left). When there are multiple goals, their strings are concatenated.
run_ tac (state, tactic): Run a tactic on a given state and return the next state. The returned state will be an error state if the tactic execution is not successful, e.g., due timeout or inapplicable tactic. If the input state is an error, the result can only be an eπгоr.
Building this environment is technically challenging, as Lean is designed for human users, not machines. LeanDojo is the first tool that interact with Lean reliably. Existing tool [9 is limited: 21.1% of the ground truth proofs are misjudged as incorrect, due to issues with how they construct the proof environment, which distorts the reported performance and produces unreliable feedback when used in reinforcement learning. In contrast, LoanDojo reduces the number of misjudgments to 1.4%. Details in Appendix A.2
5 ReProver: Retrieval-Augmented Theorem Prover
We develop the ReProver model that uses retrieval to select premises explicitly. At its core is a aarrivval-uugentee tactic generator (Fig. [ Bottom). Given the current proof state, it retrieves handful of potentially useful premises and generates a tactic conditioning on the concatenation the state and retrieved premises. When proving theorems, the model generates multiple tactic candidates at each step, which are used a standard best-first search algorithm to find proof's [6 18 28).
Premise Retrieval Our retriever is based on Dense Passage Retriever 226] Given state s as the query and library of candidate premises p {p, ) it retrieves ranked list of premises {r') from P. In DPR, s and p; are both raw texts but are embedded a vector space, and we retrieve the top m premises maximizing the cosine similarity between the state and the premise.
More formally, we have a function /f parameterized by for embedding both the state and the premises into h--dimensional vector space: [(s 0), [pi, 0) E TRA,. We retrieve premises maximizing fs,,)) ff" () 12ll 1l2) We choose f to be a Transformer encoder 2 followed by average pooling: f(,, 0) AvgPool(Enc(-.00
The retrieval is efficient. The premise embeddings f(p;, 0) can be pre-computed, and we only need one forward pass to compute f'(s, 0). We do not rerank the retrieved premises as in Mag- nushammer (49, which is more costly since requires separate forward pass for each retrieved premise.
Similar DPR, train the retriever by minimizing contrastive loss between positive premises and in-batch negative premises. Specifically, suppose we have batch of b states. For each state, we sample positive premise from the ground truth and n negative premises from They They are called "in- batch" negatives because they are shared by all states in the Eeechy-veryy- state is associated with all b- (n + 1) premises; least I of them is positive. Let 4i {0, 1} denote whether a state-premise pair (s;,P)) P2) is positive. We minimize the mean squared loss:
b b((++1) Σ
f(s 03" f(pj, 0) [f 0)1l211 0)
((0)
"Another common type proofs "term-style proofs". Any term-style proof "X" can always be converted into an equivalent tactic-style proof "exact x", though such conversion may lead to unidiomatic proofs. When training the retriever, we ignore proof states followed by tactics without using any premise.
7

---

Retrieving from Accessible Premises. We incorporate into DPR two insights tailored to premise selection. First, instead of retrieving from all premises in the math library, we restrict to premises accessible to the current theorem. They include premises defined in the same file before the theorem, as well as those imported from other files. We compute accessible premises for each theorem, relying on LeanDojo's s capability in program analysis (Sec. 4). Focusing on accessible premises makes ' much smaller. LeanDojo Benchmark contains 130,262 premises in total, but the average number of accessible premises is only 33,160.
In-file Negative Examples. DPR's performance depends critically on the quality of negative examples [9I 92]. In early experiments, we sampled all n negative premises randomly, and the model often mistakenly retrieved other premises from the same file as the positive one. Therefore, we propose a scheme that samples l in-file negatives and n k random negatives for training.
Tactic Generation. As Fig. I (Bottom), retrieved premises are concatenated with the state Then an encoder-decoder Transformer, ByT5 [44], takes them as input and generates the tactic. The model is trained to minimize the cross entropy loss w.r.t. Human-written tactics.
Training ReProver takes substantially less compute than prior methods (120 GPU hours vs. more than 1000 hours [16 (7)). All existing LLM-based provers pretrain datasets specific math and coding [4H20]] The pretraining is computationally expensive, and the datasets are kept private. In contrast, choose to avoid domain-specific pretraining and build upon goog hogglee/bytssaalll
model checkpoint that is generic, publicly available, and relatively small (299M parameters vs. 837M [16] or 600M (T7). We could further benefits from domain-specific pretraining, Minerva [57], or stronger LLMs like LLaMA [93] or StarCoder [94). but that is beyond our scope. In addition, our model is finetuned on numan-writter tacties only. without auxiliary data [16] or data collected through online interaction with Lean [7 19]. These orthogonal directions are valuable but will significantly increase the method's 's complexity and compute requirements.
in
Experiments
We evaluate ReProver on LeanDojo Benchmark. It outperforms baselines on premise selection and theorem proving, demonstrating the promise of theorem proving with aargenel-augmenteed language models. Experimental details and hyperparameters are Appendix C.T
Premise Selection. For premise selection, we only use tactics in LeanDojo Benchmark that have at least one premise. The model, based on ByT5 encoder, uses the state hefore tactic as the query to retrieve 100 premises. Then, we calculate standard metrics in information retrieval: R @ (recall for the top k retrieved premises) and MRR (mean reciprocal rank).
Our first baseline is a classical BM25 retriever (95] without machine learning. Results in Table I show that our method outperforms BM25 significantly across the board. However, it exhibits large performance degradation on the challenging data split (comparing novel_premise
random).
This is consistent with the general observation that machine learning can be brittle in the presence of distribution shifts. In addition, we compare with two ablations: one retrieving from all premises (instead of accessible premises only) and the other without in-file negatives. They perform worse than our method, demonstrating the effectiveness of our two improvements upon DPR.
Theorem Proving Experimental Setup. Then we evaluate ReProver on theorem proving. The training has two stages: First, we train the retriever and use it to retrieve 100 premises for all proof states in LeanDojo Benchmark. Second, we train the tactic generator, taking as input the concatenation of the state and retrieved premises (truncated to a length limit). During evaluation, the tactic generator is combined with best-first search to prove theorems. We evaluate the Pass @ metric: The prover is given only one attempt and must find the proof within a wall time limit of 10 minutes. Training takes five days on a single NVIDIA A100 GPU with 80GB memory, and evaluation takes two days on eight V 100 GPUs. Please see Appendix C.1 for details.
Baselines. Following prior work [16 28 we include tidy as a baseline. It is a tactic in mathlib that tries complete the proof using heuristies (without machine learning). We apply tidy directly
We retrieve 100 premises, concatenate them with the state, and truncate the concatenation fixed length.
8

---

Table I: Premise selection testing performance. For each method, train and evaluate two models independently using different data splits (random and novel_premises see Sec. 4 recall for the top k retrieved premises, and MRR is the mean reciprocal rank metric (higher is better). Our retriever outperforms BM25 and ablations. Results for Lean 4 are in Appendix
@@k is the
Method
random
R
R@ 10
MRR
R@1
R@ 10
MRR
BM25
6.7
17.2
0.15
5.9
13.5
0.14
w/ all premises
1.9
11.9
0.08
2.1
12.4
0.08
Ours
13.5
38.4
0.31
9.1
27.6
0.24
w/ all premises
11.7
36.2
0.27
7.1
23.1
0,20
w/o in-file negatives
10.8
33.1
0.25
7.9
25.7
0.22
to the original theorem and see it can succeed within the wall time limit. Another baseline uses GPT-4 the tactic generator. Given state, queries GPT-4 to generate 35 tactics in zero-shot. After removing invalid ones, the remaining tactics are combined with best-first search to find proofs. Data contamination is possible: Many proofs had been publicly available on GitHub before GPT-4's data cutoff date (September 2021). See Appendix C.2 for details.
Unfortunately, it is not feasible compare with existing LLM-based provers in Lean [6 None them are open-source or can be reproduced with reasonable effort. Furthermore, we cannot compare directly with the numbers reported in their papers, due differences in data, infrastructure, and training procedures (details in Appendix C.3) Many difficulties are due to the private nature of existing methods. By releasing our code and models, we hope to create accessible baselines for future work to build upon.
Table 2: Theorem proving Pass@1 (%) the testing data of LeanDojo Benchmark. Our ReProver model outperforms tidy, GPT-44 and a baseline that generates tactics directly without retrieval. Results for Lean 4 are in Appendix
Method
random
novel pareiise_emsesssssse
tidy
23.8
5.3
GPT4
29.0
7.4
ReProver (ours)
51.2
26.3
w/o retrieval
47.6
23.2
Results. Table shows the results on the testing data of LeanDojo Benchmark. ReProver outper- forms all baselines on two different data splits, demonstrating the effectiveness of retrieval-augment theorem proving. GPT-4 performs substantially worse than our method, even though it may have seen the ground truth proofs due to data contamination. The task cannot be solved out of the box by state-of-the-aar LLMs, calling for algorithmic innovations to make further progress.
Testing theorems in novel_premin perform substantially worse on novel_ wereelprreiiseee than the random split. We argue that performance on challenging splits is more indicative of the prover's capability and should be emphasized in the future development of theorem proving.
are indeed much more challenging. All methods in Table 2
Evaluation on MiniF2F and ProofNet. We run ReProver prove theorems in MiniF2F 28 and ProofNet (29). These two datasets are for testing only and do not have training theorems, which makes them challenging since the distribution of theorems is quite different from mathlib used to train ReProver. MiniF2F focuses on math olympiads, and ProofNet focuses on exercises in undergraduate math textbooks. On MiniF2F's s test set in Lean, ReProver achieves Pass @ of 26.5%. 5%,, which is competitive with state-of-the. the-art methods without RL (25.9% in Polu et al. [19 On ProofNet, our @ass is 13.8%, which the first reported theorem proving result on this dataset. Further, many theorems do not have ground truth proofs in Lean. Our prover discovers 33 proofs in MiniF2F and 39 proofs in ProofNet that currently do not have Lean proofs. Please see Appendix C.4 for details, examples, and caveats.

---

7 Conclusion
We have introduced LeanDojo: an open-source playground for learning-based theorem proving in Lean, consisting of toolkits, models, and benchmarks. It extracts data from Lean and enables the model to interact with Lean programmatically. We have developed ReProver, the first retrieval- augmented LLM for theorem proving. Limitations and future work are discussed in Appendix [F]
We have released code, data, models, and documentation facilitate future research:
LeanDojo's codebase for data extraction and interaction with Lean: https://github com htne//eannaaa
LeanDojo's documentation: jttppe//eendojo.readhhlccs-
Datasets: (1) LeanDojo Benchmark: http:://dbl..rrg//0.555/////// 80163885
with DOI 10. 528102oooo 8016388 (2) LeanDojo 4 (Append D https
7/ 10.
with o00.0000000000101000000000000000
ReProver's code and models: hwtph:/tttp./ggaah..ccccooaaaaat
ChatGPT plugin
LeanDojo Website:
Acknowledgments and Disclosure of Funding
This work is partially supported by Caltech's Center for Autonomous Systems and Technologies. Kaiyu Yang is supported by the Computing, Data, and Society Postdoctoral Fellowship at Caltech. Alex Gu supported by the National Science Foundation (NSF) Graduate Research Fellowship. Rahul Chalamala and Peiyang Song are supported by the Summer Undergraduate Research Fellowships (SURF) program Caltech. Anima Anandkumar partially supported by the Bren endowed chair. We appreciate the valuable feedback from Logan Murphy and members of the Anima AI+Science Lab on an initial version of this paper. We thank Junyan Xu for manually inspecting the proofs generated by model ProofNet. We also thank Jeremy Avigad and Mario Carneiro for insightful discussions on supporting Lean LeanDojo.
10

---

References
[1] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean thcorem prover (system description). In International Conference on Automated Deduction (CADE), 2015.
22
[2] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Neural Information Processing Systems (NeurlPS), 2017.
7
[3] Allen Newell and Herbert Simon. The logic theory machine- a complex information processing system. IRE Transactions on information theory, 2(3):11 79, 1956.
[4] Kevin Buzzard. The future of mathematics. CRNS-Imperial Lecture. 2019.
[5] Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. CompCert a formally verified optimizing compiler. In Embedded Real Time Software and Systems, 2016. !
[6] Talia Ringer, Karl Palmskog. Ilya Sergey, Milos Gligoric, Zachary Tatlock, et al. QED at large: A survey of engineering of formally verified software. Foundations and Trends in Programming Languages, 2019.
[7] Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean- -hrrithitt 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. |
[8] Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: proof assistant for higher- order logic. 2002. [
[9] Kaiyu Yang and Jia Deng. Learning prove theorems via interacting with proof assistants. In Interna- tional Conference on Machine Learning (ICML), 2019. 35
[10] William A Howard. The formulae-as-type notion of construction. To HB Curry: Essays Combinatory Logic, Lambda Calculus and Formalism, 1980.
[11] Mark Chen, Jemry Tworek. Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph. Greg Brockman, et al. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03334, 2021. 2
[12] Ziwei Ji, Nayeon Lee. Rita Frieske, Tiezheng Yu. Dan Su, Yan Xu, Etsuko Ishii, Bang, Andrea Madotto, and Pascale Fung. Survey of hallucination in natural language generation. ACM Computing Surveys, (5rng),,5((1))))) 55(12):1-33 2023.
[13] Timo Schick, Jane Dwivedi- Yu, Roberto Dessi, Roberta Raileanu, Maria Lomeli, Luke Zettlemoyer, Nicola Cancedda. and Thomas Scialom. Toolformer: Language models can teach themselves to use tools. arXiv preprint 230x:2302..4761. 2023.
[14] Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009. 03393, 2020.
g
[15] Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. LISA: Language models of ISAbelle proofs. In Conference on Artificial Intelligence and Theorem Proving (AITP). 2021.
[16] Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. In International Conference Learning Representations (ICLR), 2022.
6
20 26 36
[17] Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. HyperTree proof search for neural theorem proving. In Neural Information Processing Systems (NeurIPS), 2022.
26 36
[18] Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygó2dZ, Piotr Milos, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. In Neural Information Processing Systems (NeurIPS), 2022.
26
[19] Stanislas Polu, Jesse Michael Han, Kunhao Zheng. Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. In International Conference on Learning Representa- tions (ICLR), 2023.
g
9
20
26
36

---

[20] Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. arXiv preprint arXiv:2303. 049900 2023.
S 35
[21] Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, et al. DT-Solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Annual Meeting of the Association for Computational Linguistics (ACL), 2023.
4
[22] Greg Brockman, Vicki Cheung, Ludwig Pettersson, Jonas Schneider, John Schulman, Jie Tang, and Wojeiech Zaremba. OpenAl Gym. arXiv preprint arXiv:/606.01540 2016.
7
[23] Josef Urban. MPTP motivation, implementation, first experiments. Journal of Automated Reasoning. 33:319 129199339, 2004.
[24] Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. DeepMath- deep sequence models for premise selection. In Neural Information Processing Systems (NeurlPS), 2016. 3
[25] The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New York, NY, USA, 2020, Association for Computing Machinery. ISBN 9781450370974. 3373824, Utttttss::///o/ org/ 10. 1145/3372865 3373824
doi: 10. 10.1145/3372885.
[26] Vladimir Karpukhin, Barlas Oguz, Sewon Min, Patrick Lewis, Ledell Wu, Sergey Edunov, Danqi Chen, and Wen-tau Yih. Dense passage retrieval for open-domain question answering. In Conference on Empirical Methods Natural Language Processing (EMNLP), 2020.
33
[27] OpenAI. GPT-4 technical report. arXiv preprint arXiv:2303.08772 2023.
[28] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: a cross-system benchmark for formal dlympiad-leve mathematics. In International Conference on Learning Representations (ICLR), 2022.
3
26 27
[29] Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad, ProofNet: Autoformalizing and formally proving undergraduate- mathematics. arXiv preprint arXiv:2302. 12433, 2023.
26
28 29
[30] Alan JA Robinson and Andrei Voronkov. Handbook of automated reasoning, volume 1. 2001.
[31] Laura Kovács and Andrei Voronkov. First-order thcorem proving and vampire. In International Conference on Computer Aided Verification (CAV), 2013.
[32] Sarah Loos, Geoffrey Irving. Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. arXiv preprint weXiv:170106977 2017.
[33] James Bridge, Sean B Holden, and Lawrence C Paulson. Machine learning for first-order theorem proving: learning to select a good heuristic. Journal of Automated Reasoning, 53:141-172, 2014.
[34] Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. TacticToe: learning to prove with tactics. Journal of Automated Reasoning, 65:257-286, 2021.
[35] Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. In AAAI Conference Artificial Intelligence, 2020. 4
[36] Kshitij Bansal, Christian Szegedy, Markus Rabe, Sarah Loos, and Viktor Toman. Learning to reason in large theories without imitation, arXiv preprini 1905: 10501, 2019.
[37] Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. TacticZero: Learning to prove theorems from scratch with deep reinforcement learning. In Neural Information Processing Systems (NeurIPS), 2021.
[38] Mingzhe Wang and Jia Deng. Learning prove theorems by learning to generate theorems. In Neural Information Processing Systems (NeurIPS), 2020. 36
[39] Markus Norman Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self supervised skip-tree training. In International Conference on Learning Representations (ICLR), 2021.
12

---

[40] Yuhuai Wu, Markus N Rabe, Wenda Li, Jimmy Ba, Roger B Grosse, and Christian Szegedy. LIME: Learning inductive bias for primilives of mathematical reasoning. In International Conference Muchine Learning (ICML), 2021. 4
[41] Sascha Böhme and Tobias Nipkow. Sledgehammer; judgement day. In International Joint Conference on Automated Reasoning (ICARR), 2010.
[42] Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C Paulson, and Josef Urban. Hammering towards QED. Journal of Formalized Reasoning, 91):1011-44, 2016.
[43] Lukasz Czajka and Cezary Kaliszyk. Hammer for Coq: Automation for dependent type theory, Journal of Automated Reasoning, 2018.
[44] Linting Xue, Aditya Barua, Noah Constant, Rami Al-Rfou. Sharan Narang, Mihir Kale, Adam Roberts. and Colin Raffel. ByT5: Towards token-free future with pre-trained byte-to-byy byte models. Trunsactions of the A Association for Computational Linguistics (TACL), 10:291-306, 2022.
24 32
[45] Christian Szegedy, Markus Rabe, and Henryk Michalewski. Retrieval-augmenned proof step synthesis. In Conference Artificial Intelligence and Theorem Proving (ATTP), 2021.
4
[46] Yuhuai Wu. Formal premise selection with language models. In Conference on Artificial Intelligence and Theorem Proving (AITP). 2022. 4
[47] Jesse Alama, Tom Heskes, Daniel Kühhwwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. Journal of Automated Reasoning, 191-11,,
2014. 4
[48] Bartosz: Piotrowski, Ramon Fernández Mir, and Edward Ayers. Machine-learned premise selection for Lean. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLFAUX), 2023.
[49] Maciej Mikula, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Lukasz Kuciński, Piotr Mitoš, and Yuhuai Wu. Magnushammer: A transformer- based approach premise selection. arXiv preprint arXiv:2303..m 234404430 2023.
[50] Eric Yeh, Briland Hitaj, Sam Owre, Maena Quemener, and Natarajan Shankar. CoProver: A recommender system for proof construction. arXiv preprint arXiv:2.304. 10486, 2023.
[51] Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: learning environment for theorem proving. In International Conference on Learning Representations (ICLR), 2019. g
[52] Tom Reichel, R Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer. Proof repair infras- tructure for supervised models: Building large proof repair dataset. In International Conference on Interactive Theorem Proving (ITP), 2023.
[53] Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C Paulson. IsarStep: benchmark for high-level mathemat- ical reasoning. International Conference on Learning Representations (ICLR), 2021.
[54] Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An envi- ronment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning (ICMI), 2019. 4
[55] Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A machine learning dataset for higher-order logic thcorem proving. In International Conference Learning Representations (ICLR), 2017.
[56] Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song. and Jacoh Steinhardt. Measuring mathermatica problem solving with the MATH dataset. In Neural Information Processing Systems (NeurIPS), Datasets and Benchmarks Track, 2021.
[57] Aitor Lewkowyez, Anders Johan Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Venkatesh Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo et al. Solving quantitative reasoning problems with language models. In Neural Information Processing Systems (NeurIPS), 2022. g
[58] Deborah Ferreira and André Freitas. Premise selection in natural language mathematical texts. In Annual Meeting of the Association for Computational Linguistics (ACL), 2020.
13

---

[59] Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi. Yejin Choi, and Kyunghyun Cho. NaturalProofs: Mathematical theorem proving in natural language. In Neural Information Processing Systems (NeurlPS), Dutasets and Benchmarks Track, 2021.
[60] Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. NaturalPrower: Grounded mathematical proof generation with language models. In Neural Information Processing Systems (NeurlPS), 2022.
[61] Swaroop Mishra, Matthew Finlayson, Pan Lu, Leonard Tang, Sean Welleck, Chitta Baral, Tanmay Rajpurohit, Oyvind Tafjord, Ashish Sabharwal, Peter Clark, et al. Lila: A unified benchmark for mathematical reasoning. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2022.
[62] Pan Lu, Liang Qiu, Wenhao Yu, Sean Welleck, and Kai-Wei Chang- A survey of deep learning for mathematical reasoning, arXiv preprint urXiv:2212.10535, 2022.
[63] Jordan Meadows and Andre Freitas. A survey in mathematical language processing. arXiv preprint arXiv:2205. 15231, 2022. 4
[64] Qingxiang Wang. Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Conferences on Intelligent Computer Mahematics (CICM), 2018.
[65] Matthias Coster, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. 2023.
arXiv preprint
[66] Jiayi Pan, Glen Chou, and Dmitry Berenson. Data-efficient learning of natural language to linear temporal logic translators for robot task specification. In International Conference on Robotics and Automation (ICRA), 2023.
[67] Christopher Hahn, Frederik Schmitt, Julia Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner. Formal specifications from natural language. arXiv preprint arX1v:2206.0166,, 2022.
[68] Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy, Autoformalization with large language models. In Neural Information Processing Systems (NeurlPS), 2022.
[69] Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, Sketch, and Prove: Guiding formal theorem provers with informal proofs. In International Conference on Learning Representations (ICLR), 2023. 26
[70] Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-basee based demonstration learning for formal theorem proving. arXiv preprint arXiv:2305.166366 2023. 26
[71] Garett Cunningham, Razvan C Bunescu, and David Juedes. Towards autoformalization of mathematics and code correctness: Experiments with elementary proofs. arXiv preprint arXiv:2301.02195, 2023.
[72] Yongchao Chen, Rujul Gandhi, Yang Zhang, and Chuchu Fan. NL2TL: Transforming natural languages to temporal logics using large language models. arXiv preprint arXiv:2305.07766, 2023. 4
[73] Urvashi Khandelwal, Omer Levy, Dan Jurafsky, Luke Zettlemoyer, and Mike Lewis. Generalization through memorization: Nearest neighbor language models. In International Conference on Learning Representations (ICLR), 2020. 4
[74] Kelvin Guu, Kenton Lee, Zora Tung, Panupong Pasupat, and Mingwei Chang. Retrieval augmented language model pre-training. In International Conference Machine Learning (ICML), 2020.
[75] Patrick Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, Vladimir Karpukhin, Naman Goyal, Heinrich Küttler, Mike Lewis, Wen-tau Yih, Tim Rocktäschel, et al. Retrieval-augmenteed generation for wwwwlldgg-inntnsive NLP tasks. In Neural Information Processing Systems (NeurIPS), 2020.
[76] Sehastian Borgeaud, Arthur Mensch, Jordan Hoffmann, Trevor Cai, Eliza Rutherford, Katic Millican, George Bm Van Den Driessche, Jean- Baptiste Lespiau, Bogdan Damoe, Aidan Clark, et al. Improving language models by retrieving from trillions of tokens. In International Conference on Machine Learning (ICML), 2022.
[77] Zonglin Li, Ruiqi Guo, and Sanjiv Kumar. Decoupled context processing for context augmented language modeling. In Neural Information Processing Systems (NeurIPS), 2022.
14

---

[78] Zhengbao Jiang, Luyu Gao, Jun Araki. Haibo Ding, Zhiruo Wang, Jamie Callan, and Graham Neubig. Retrieval attention: End-to-end learning of retrieval and reading within single transformer. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2022.
[79] Yuhuai Wu, Markus Norman Rabe, DeLesley Hutchins, and Christian Szegedy. Memorizing transformers. In International Conference on Learning Representations (ICLR), 2022.
[80] Gautier Izacard, Patrick Lewis, Maria Lomeli, Lucas Hosseini, Fabio Petroni, Timo Schick, Jane Dwivedi- Yu, Armand Joulin, Schastian Riedel, and Edouard Grave Few-shot learning with retrieval augmented language models. arXiv preprint arXiv: 03299, 2022.
[81] Zexuan Zhong, Tao Lei, and Danqi Chen, Training language models with memory augmentation. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2022. .
[82] Shirley Anugrah Hayati, Raphael Olivier, Pravalika Avvaru, Pengcheng Yin, Anthony Tomasic, and Graham Neubig. Retrieval-basee neural code generation. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2018. A
[83] Md Rizwan Parvez, Wasi Ahmad, Saikat Chakraborty, Baishakhi Ray, and Kai- Wei Chang. Retrieval augmented code generation and summarization. In Findings of the Association for Computational Linguistics: EMNLP, 2021.
[84] Shuai Lu, Nan Duan, Hojae Han, Daya Guo, Seung-won Hwang, and Alexey Svyatkovskiy. ReACC: A retrieval-augmeeted code completion framework. In Annual Meeting of the Association for Computational Linguisties (ACL), 2022.
[85] Shuyan Zhou, Uri Alon, Frank F Xu, Zhengbao Jiang, and Graham Neubig. DocPrompting: Generating code by retrieving the docs. International Conference on Learning Representations (ICLR), 2023.
[86] Disha Shrivastava, Hugo I arrccellee, and Daniel Tarlow. Repository-level prompt generation for large language models of code. arXiv preprint arXiv:2206. 12839, 2022.
[87] Fengji Zhang, Bei Chen, Yue Zhang, Jin Liu, Daoguang Zan, Yi Mao, Jian-Guang Lou, and Weizhu Chen. RepoCoder: Repository-Ievel code completion through iterative retrieval and generation. arXiv preprint arXiv:2303. 12570, 2023.
[88] Yangruiho Ding, Zijian Wang, Wasi Uddin Ahmad, Murali Krishna Ramanathan, Ramesh Nallapati, Parminder Bhatia, Dan Roth, and Bing Xiang. CoCoMIC: Code completion by jointly modeling in-file and cross-file context. arXiv preprint arXiv:2212. 10007, 2022.
[89] David Thrane Christiansen. Functional programming in Lean, 2023.
[90] Timnit Gebru, Jamie Morgenster,, Briana Vecchione, Jennifer Wortman Vaughan, Hanna Wallach, Hal Daumé fii, and Kate Crawford. Datasheets for datasets. Communications of the ACM, 64(12):86 92, 2021.
22
[91] Jingtao Zhan, Jiaxin Mao, Yiqun Liu, Jiafeng Guo, Min Zhang, and Shaoping Ma. Optimizing dense retrieval model training with hard negatives. In International ACM SIGIR Conference on Research and Development in Information Retrieval (SIGIR), 2021. 8
[92] Jing Lu,, Gustavo Hernandez. Abrego, Ji Ma, Jianmo Ni, and Yinfei Yang. Multi-stage training with improved negative contrast for neural passage retrieval. In Conference Empirical Methods in Natural Language Processing (EMNLP), 2021. g
[93] Hugo Touvron, Thibaut Lavril, Gautier Izacard, Xavier Martinet, Marie-Anne Lachaux, Timothée Lacroix. Baptiste Rozière, Naman Goyal, Eric Hambro, Faisal Azhar, et al. LLaMA: Open and efficient foundation language models. arXiv preprint arXiv: 13971, 2023. R
[94] Raymond Li, Loubna Ben Allal, Yangtian 7i, Niklas Muennighoff, Denis Kocetkov, Chenghao Mou, Mare Marone, Christopher Akiki, Jia Li, Jenny Chim, al. StarCoder: may the source be with you! arXiv preprint arXiv:2305.06161. 2023. 32
[95] Stephen Robertson, Hugo Zaragoza, et al. The probabilistic relevance framework: BM25 and beyond. Foundations and Trendy@ in Information Retrieval, 3(4):333-389 2009. g
[96] Leonardo de Moura, Jeremy Avigad, Soonho Kong, and Cody Roux. Elaboration in dependent type theory. arXiv preprint A.d.:1555504324.. 2015. 18
15

---

[97] Colin Raffel, Noam Shazeer, Adam Roberts, Katherine Lee. Sharan Narang. Michael Matena, Yanqi Zhou, Wei Li, and Peter J Liu. Exploring the limits of transfer learning with unified text-to-text transformer. The Journal of Machine Learning Research, 21(1):5485-5511 2020.
[98] Jeff Rasley, Samyam Rajbhandari. Olatunji Ruwase, and Yuxiong He. DeepSpeed: System optimizations enable training deep learning models with over 100 billion parameters. In International Conference on Knowledge Discovery and Data Mining (KDD), 2020. 24
[99] Ilya Loshchilov and Frank Hutter. Decoupled weight decay regularization. In International Conference on Learning Representations (ICLR), 2019.
24
[100] Mathlib Community, Mathport: tool porting Lean projects to Lean 4. URL htttps://githbb
27
[101] OpenAl. ChatGPT plugins. lattps://
//openai.com com hatpe////oooo/ooo//////////a/// wttpoo///ggttttpltoggaeeeo http::///pppaaa..oooo/////aaaagp
2023, URL https
29
[102] Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Thomas Griffiths, Yuan Cao, and Karthik Narasimhan. Tree of thoughts: Deliberate problem solving with large language models. arXiv preprint
wiXiv:2355.0661 2023.
33
[103] Erik Nijkamp, Bo Pang, Hiroaki Hayashi, Lifu Tu, Huan Wang, Yingbo Zhou, Silvio Savarese, and Caiming Xiong. CodeGen: An open large language model for code with multi-turn program synthesis. arXiv preprint MxXi::203.133744 2022.
32
[104] Qinkai Zheng, Xiao Xia. Xu Zou, Yuxiao Dong. Shan Wang. Yufei Xue, Zihan Wang, Lei Shen, Andi Wang. Yang Li, et al. CodeGeeX: A pre-trained model for code generation with multilingual evaluations on HumanEval-X X. arXiv preprint arXiv:2303.17566 2023. 32
[105] Lili Yu, Dánicl Simig, Colin Flaherty, Armen Aghajanyan, Luke Zettlemoyer, and Mike Lewis. MegaByte: Predicting million-byte sequences with multiscale transformers. arXiv preprint arXiv:2305.07/8. 2023.
[106] Gautier Izacard and Édouard Grave. Leveraging passage retrieval with generative models open domain question answering. In European Chapter of the Association for Computational Linguistics (EACL), 2021.
33
[107] Yi Tay, Vinh Tran, Mostafa Dehghani, Jianmo Ni, Dara Bahri, Harsh Mehta, Zhen Qin, Kai Hui, Zhe 7hao, Jai Gupta, et al. Transformer memory as differentiable search index. In Neural Information Processing Systems (NeurlPS), 2022. 34
[108] Michele Bevilacqua, Giuseppe Ottaviano, Patrick Lewis, Scott Yih, Sebastian Riedel, and Fabio Petroni. Autoregressive scarch engines: Generating substrings document identifiers. 2022.
[109] Ronak Pradeep, Kai Hui, Jai Gupta, Adam D Lelkes, Honglei Zhuang, Jimmy Lin, Donald Metzler, and Vinh Q Tran. How does generative retrieval scale to millions of passages? arXiv preprint arXiv:2305. 1841, 2023. 34
[110] Norman Megill and David A Wheeler. Metamath: computer language for mathematical proofs. Lulu. com, 2019. 36
16

---

Appendix
LeanDojo Technical Details
18
A.1
Extracting Premise Information from Lean's Elaborator
18
A.2
Reliable Interaction with Lean
18
A.3
Comparison with Existing Tools for Learning- Boaning-BBased Theorem Proving Lean
19
LeanDojo Benchmark
20
Dataset Format
20
2 Datasheet
22
B.3 Data Hosting, Licensing, and Maintenance
23
Experiments
23
Details and Hyperparameters
23
The GPT-4 Baselinel
24
Justifications for Not Comparing with Existing LLM-Based Provers
26
Evaluation on MiniF2F and ProotNet
26
D LeanDojo for Lean 4
27
ChatGPT Plugin for Theorem Proving
29
Limitations and Future Work
32
17

---

A LeanDojo Technical Details
We provide more information on how LeanDojo extracts data from and interacts with Lean For further details, please check our open-source implementation.
A.1 Extracting Premise Information from Lean's Elaborator
"Premises" in this paper belong category of Lean expressions called "constants." In Lean, definitions of constants are grouped into nested, hierarchical namespaces Therefore, each premise has unique fully-qualified name. For example, mod_sel2 in Fig. 2 iis defined in the namespace nat; therefore, its fully qualified name is nat mot_mood_eef, However, it would be too verbose if premises had to be referred using full names. In practice, tactics often refer premises using short names such as mod_ __eeff. f. In case multiple premises share the same short name, Lean automatically infers the correct one from the context through process called "name resolution". LeanDojo able to trace the input/output of Lean's 's name resolution and thereby extract accurate premise information for training the retriever.
Name resolution in Lean is implemented in a process called "elaboration," which happens after parsing but before the parsed expressions checked by Lean's trusted kernel. Elaboration takes as input user-entered expressions (called "pre-expressions)) that are concise, partially specified, and potentially ambiguous. It turns them into complete expressions ready to be checked by the kernel. This is realized by inferring not only full names but also missing types, implicit arguments, overloading, type coercion, etc. Please refer to de Moura et al. [96] for details on Lean's elaboration process. In LeanDojo, we modify Lean's 's internal implementation, intercepting the elaborator to record its input/output:
Pre-expression: The input to Lean's elaborator, including where premises are used in proofs.
Expression: The output of the elaborator, including the premise's 's full name and where it is defined.
Locations are spans the source code, specified by the file name and the row/column numbers of its start/end, Our modification takes the form of a Git patch that LeanDojo can automatically apply to any version of Lean after March 24, 2022.
A.2 Reliable Interaction with Lean
Polu et al. 19 introduced lean- gymm To our knowledge, it the only mature, open-source tool before LeanDojo for interacting with Lean programmatically. However, found severe issues with lean-gym: About 21.1% %% of the correct, human- wurtten proofs are misjudged as incorrect, leading to two problems: First, it underestimates the prover's evaluation performance. Second, the results too noisy as feedback signals for reinforcement learning.
After carefully analyzing lean- -at--sysss implementation, identified the root cause of the problem. When proving a theorem, the environment used by lean- lean-gym is subtly different from the original environment used by humans. Specifically, lean- gym fails to handle namespaces correctly (illustrated in Fig. A). As a result, name resolution fails unexpectedly when checking correct proofs.
For example, Fig. A A compares the correct environment and the environment constructed by lean- gym. The theorem should be inside the namespace "buffer". However, in bean-gym,, merely opens the namespace. These two scenarios are different when it comes name resolution. Being inside a namespace instructs Lean favor constants defined in that namespace, whereas opening namespace does not have such effect. In this example, the short name "read" is ambiguous: We have imonad_reader read" defined in cinit/controo// defined in "data/buffes er lean". In the correct environment, the "read" in "unfold read" resolves to "buffer. read". Whereas in lean- 'ss environment, "mmondd_readd"" reader read". Lean complains that "read" is not equational lemma, because it is referring to a wrong "read". LeanDojo does not suffer from this kind of error since uses a different mechanism for constructing the environment. Specifically, it wraps the interaction code Lean tactic, which is inserted into the proof. Therefore, the environment is guaranteed to be correct.
lean" and "buffer read"
incorrectly resolved to
'LLean" in our paper refers to Lean 3 by default. Lean 4 is not backward cooppall-compatible but is also supported by LeanDojo. Our Lean 4 results in Appendix D
18

---

We quantitatively compare lean-gyn gym and LeanDojo on the number of proof check- ing errors. In this study, we use Lean v3.42.1 paired with mathlib version 355 19774447777 since they are supported by both tools. We use Lejo to extract all tactic-style proofs and enter them into both tools. These proofs are correct, but lean- -ym failed on 21 1.1% % of them. In contrast, LeanDojo only failed on 1.4%, and its failures are a subset of lean-gym gym s. We include this study in our open-source repo and document example proofs from the remaining 1.4% to provide transparency on LeanDojo's limitations 10
import bata.butfar universe u
inport Sata.buffee universe a
naraspace baffer
open buffer
theoren ny my_read_ag_ rggar <a Type u) [Snhablitad a] buffer (1 bat) busize)
theoren ny_read, rea.e_eeerredddd (a Type ut (inbsbited a] (b. buffer a) (1 nat) (h : b.sise) :
read b (1, b) read? ze begin
1)
begin
casea unfold read. unfold read',
unfold read, unfold read',
slap (array.ress re____e____rrddddd
cimp (array rww.deeddd__oooo... rq_raddd and
butfor
Correct environment
lean-gym's environment
ERROR: unfold tactic failed, 'zead' does not have equational lemmas nor is a projection
Figure A: An example of correct proofs misjudged as incorrect by lean-gym, adapted from the theorem heaadee__redd in "data/buffer: lean" of Lean's standard library. The error message because lean-gym failed to resolve the short name "read" to the correct fully-qualified name. The Lean code in this figure is only for illustrative purposes. It does not reflect the implementation technique used by lean-gym construct the environment. Instead of generating actual Lean code, lean- gym uses Lean's 's metaprogramming APIs to construct the environment.
A.3 Comparison with Existing Tools for Learning-Based Theorem Proving in Lean
To our knowledge, LeanStep [6 and lean-gym [9] are the only published tools for learning- theorem proving in Lean. There are few unpublished prototypes, such reep lean-client-pyttee and lean- gym for Lean 4) none of which is mature enough or is under active development. Therefore, only compare LeanDojo with LeanStep and lean-gyn gan (summarized in Table
LeanDojo supports both data extraction and interacting with Lean programmaticallyy In contrast, LeanStep is only for data extraction, and lean-gy gean-gym is only for interacting with Lean. They are not actively maintained, so they do not support recent versions of mathlib (tested on August 11, 2023, using mathlib commit 0cc86699t26bb685500774440000
Functionality.
ledbfa28c). Also, neither of them support Lean 4 (Appendix() D). LeanDojo fully supports recent mathlib and Lean 4. Furthermore, LeanStep cannot extract premise information and is not applicable to repos other than mathlib. Last, LeanDojo comes with comprehensive documentation and unit tests, whereas other tools barely have any.
Implementation details. LeanStep and LeanDojo use different mechanisms to extract ASTs and proof trees. LeanStep implements ad-hoc parser in Python for parsing Lean code into ASTs. It also intercepts Lean's 's tactic system to insert logging code. Then the logs are used to reconstruct proof trees. This implementation is brittle and does not work for the current versions of Lean/nathlib. In contrast, LeanDojo relies on Lean's 's built-in mechanisms for exporting ASTs and proof states (lean --ast -stsatt -stpp), which works robustly for recent Lean/nathlib. This mechanism was developed after LeanStep.
LeanStep is technically dataset. We referring to the caan__profffecordie tool for extracting
19

---

Regarding interaction with Lean, both 1ean gym and LeanDojo rely on Lean's metaprogramming APIs, and LeanDojo partially builds upon lean- lean-gym's code. However, 1ean- gym has critical issue in that it misjudges many correct proofs as incorrect (Appendix A.2). The main reason is that lean-gym fails distinguish two subtly different cases when constructing the proof environment: (1) opening a namespace; (2) being inside namespace. LeanDojo does not suffer from this issue. Instead of operating as a standalone program in the 10 monad, it wraps the interaction code into special tactic, which is inserted into the correct location in the proof. Therefore, the interaction code guaranteed run in the same environment as the original human- proof.
LeanStep 16
lean gym
19
LeanDojo (ours)
Premise information
N/A
Lean 4 support
N/A
Data extraction
Recent mathlib
N/A
Repos other than mathlib
N/A
Estimated errors
N/A
21.1% %
1.4%
Interaction
Lean 4 support
N/A
Recent mathlib
N/A
X
Repos other than mathlib
N/A
Documentation & unit tests
Table A: Comparing LeanDojo with existing tools for data extraction and interaction with Lean.
B LeanDojo Benchmark
B.1 Dataset Format
We describe the data format of LeanDojo Benchmark, which has the following directory structure:
corpusjjsoni
All premises defined in mathlib and Lean's standard library Metadata
metadata.json.
licenses
lean....
Attribution Lean's Apache 2.0 license Attribution to mathlib's Apache 2.0 license
mathlib
README md
Statement that Lojo Benchmark released under CC BY 2.0 Theorems/proofs of the random split 94,734 theorems
random.....
train.json train..soon.....................
val. json
2,000 theorems
test. jest
2,000 theorems
novel_ novel_premisee
Theorems/prooff of the novel premises split
train.jse val. json
94,734 theorems
2,000 theorems
json
2,000 theorems
Premise Definitions. corpus. prppus.soonl contains the definition of premises. It has 3,280 lines. Each line is in JSON format and corresponds to Lean file. Below is an example for Liit/con. trol/functor. :lean which directly imports three other files: fiiit/core lean 'init/func tion.lean and
aamee. lean It defines two constants that can be used as premises: "functor" and "functor, won_ccost.... const_rrvv" For each premise, we have access to full name, the source code, and its start/end location within the file.
"path": "anper//ap///a////llar////ttttte "imports "imports": farrgr//opp//aaa/ibaaa//tttoooo lean",
.,
"_aage///gg//eea///bbb////ttttit lean" "_target/
":carge///epp/eee////bbaa///a// lean"
premises":
20

---

Ffmee_name"; "functor",
"code": "class functor (f Type + Type v) Type (max u+1) v) :mpp f B) (mmpp_ooonst
{a B Type u}, (a + f a 7
II {a B : Type ut, + f 3 - a aas :=
À a B, map o const 3)", "start": [11, 1], "end": [13, 70],
"kind": "class"
},
"full "full_name", name":
"functor. pap_const_ree
"code": "Ø [[reuucieee] def functor cap_const. {f Type
+ Type v} [functor f] {a B Type u} f 8 + a - f a :=\nd b, b <$ a", "start": [18, 1],
"end": [19, 14],
"kind": "definition"
Theorems and Tacties. Theorems in LeanDojo Benchmark are split into trainingvvalidatioonessigg using two different strategies (Sec. They are formatted in JSON, and below is example corresponding to the theorem 'real. angle to tetttto_______ div two"" LeanDojo has recorded two tacties: "split" and "linarith [pi_pos]] For each tactic, we have the proof states before/after it. The "linarith [pi_pos] tactic illustrates how premises are recorded: They are annotated using HTML-like strings such as "1 "linarith <a>pi_pos</a>>> followed by "provenance list". Each element in the list corresponds to a premise in the tactic.
"url": "ttpp://gthaubb.cm///pppooggr commit": "b66@dtebaaa00777777778010122213 "file_path" "src/ http:///aaaaspccaaaaaaooo/orrrrn angle. lean",
/
to to_real___ppee "full_name" "real. wtw.aglgee..rr.............oooo.
"startt; [512, 9], : [513, 56],
praced_tacticss
"tactic": "split",
pepootated_tacttin ["split", []] 'state_before": " - π / 2 A π < T" n S π
"state_after"; "2 goals\n
},
"tactic": "linarith [pi_pos]",
"aatttt "linarith <a>pii_os</a>]1 [
"full_name": "real pip "def "def_path": "src/ trigonometric/ basic. lean"
"def_pos": [122, 7],
]
},
"state "iaeteebefore "I - < π / 2" "state_after"" afterr; "no goals" "
21

---

mathlib released on Not all theorems have tactic-style proofs. For those without tactic-style proofs, concatenating the tactics does not lead to complete proof of the original theorem. However, this is not an issue when using the data for theorem proving evaluation or for training tactic generators.
B.2 Datasheet
We present a datasheet 900 for documentation and responsible usage of LeanDojo Benchmark.
Motivation.
For what purpose was the dataset created? It was created as benchmark for learning-hased theorem proving Lean.
Who created the dataset (e.g., which team, research group) and on behalf of which entity (e.g.. company, institution, organization)? It was created by the authors of this paper.
Who funded the creation of the dataset? See the acknowledgments in Sec.
Composition.
What do the instances that comprise the dataset represent (e.g., documents, photos, people, coun- tries)? The dataset consists of formal definitions, theorems, and proofs written in Lean [T]
How many instances are there in total (of each type, if appropriate)? The dataset has 98,734 theorems and their proofs, as well as 130,262 premises defined in 3,384 files.
Does the dataset contain all possible instances or is it a sample (not necessarily random) of instances from larger set? The dataset contains all theorems/proofs that LeanDojo extract from the commit 150601a8bbb55077740772222ee October 11, 2023.
What data does each instance consist of? Theoremssproofs in the dataset are Lean code written by programmers and mathematicians.
Are relationships between individual instances made explicit? Definitions in the dataset are linked to proof's using them as premises.
Are there recommended data splits? Yes, we recommend two data splits: random and novel_premises. Please Sec. 4 for details.
Are there any errors, sources of noise, or redundancies in the dataset? ASTs extracted by LeanDojo contain a small number of errors due to potential flaws in Lean's AST exporting mechanism. However, they do not have a tangible impact on our work.
the dataset self-contained, or does link to or otherwise rely on external resources (e.g., websites, tweets, other datasets)? The dataset is self-contained.
Does the dataset contain data that might be considered confidential (e.g., data that is protected by legal privilege or by poctor-patient confidentiality, data that includes the content of individuals' non-public ? No.
Does the dataset contain data that, if viewed directly, might be offensive, insulting, threatening, or might otherwise cause anxiety? No.
Collection Process.
How was the data associated with each instance acquired? The data is directly observable by opening mathlib in VS Code with the Lean plugin. However, we had to instrument Lean export the data programmatically.
Whut mechanisms procedures were used to collect the data (e.g., hurdware apparatuses or sensors, manual human curation, software programs, software APIs)? The data was generated by building Lean repo using modified Lean and postprocessing the exported data.
22

---

Who was involved in the data collection process (e.g., students, crowd workers. contractors), and how were they compensated (e.g., how much were crowd workers paid)? ? No manual effort was involved in the data collection process.
Over what timeframe was the data collected? The final version of the dataset was generated in October 2023.
Uses.
Has the dataset been used for any tasks already? We have used the dataset for training and evaluating machine learning models on the tasks of premise selection and theorem proving.
Is there repository that links any all papers systems that the dataset? Yes, https //leandojo.oo org
Distribution.
Will the dataset be distributed to third parties outside of the entity (e.g., company, institution, organization) on behalf of which the dataset was created? Yes, the dataset is publicly available on the Internet.
How will the dataset be distributed (e.g., tarball website, API, GitHub)? The dataset can be downloaded as a tarball.
Will the dataset be distributed under a copyright or other intellectual property (IP) license, and/or under applicable terms of use (ToU)? The dataset is distributed under CC BY 2.0. The data generation code is distributed under the MIT license. The dataset was extracted from mathlib which depends on Iean Both of them are distributed under the Apache 2.0 license. We include their licenses in the dataset as attribution (Appendix[B..)
Have any third parties imposed IP-based other restrictions the data associated with the instances? No.
Do any export controls or other regulatory restrictions apply the dataset or individual instances? No.
Maintenance.
Who will be suppertinghossing/miinttiiiiniit the dataset? The authors of this paper.
How the owner/curator/maaaaerr of the dataset be contacted (e.g., email address)? Please contact Kaiyu Yang at kaiyuy@caltech.edd
there an erratum? No.
Will the dataset be updated (e.g., correct labeling errors, add new instances, delete instances)? org for any update.
Please check htttt:tt/t//eaddee
If others want to extend/augmenn/build on/contribute the dataset, is there a mechanism for them to do so? Yes, they can use our data generation code, which is publicly available.
B.3 Data Hosting, Licensing, and Maintenance
LeanDojo Benchmark is distributed under the CC BY 2.0 license. The data is hosted on zenodooorg (a long-term data repository operated by CERN). The LoanDojo tool for data extraction and interaction with Lean is released at htthpps: ///::t////ttt /ggbttttubb..g com lean- /ooooLLenDoooppp under the MIT license. Our model checkpoints are hosted on Hugging Face Hub. LeanDojo's 's documentation is hosted on Read the Docs at hhttt::/ /tttp:://leand//// readthedocs. io, LeanDojo's website (https: //lenddojojooo org) the entry point for everything related to it, including any future updates or maintenance.
C Experiments
C.1 Details and Hyperparameters
The premise retriever and tactic generator in ReProver are initialized by the golgollelytt-smma. checkpoint Hugging Face. It is T5-like (97] encoder-decoder Transformer that operates directly
23

---

on UTF-8 bytes without tokenization. We choose ByT5 44 instead of T5 because Lean code makes extensive use of Unicode math symbols, which may cause problems to T5's pretrained tokenizer, The retriever uses the encoder only, whereas the generator uses both the encoder and the decoder.
In training, we PyTorch and PyTorch Lightning, with bfloat 16 mixed precision and DeepSpeed ZeRO Stage 2 [98]. Both the retriever and the generator are optimized using AdamW [99 with batch size of 8. In the first 2,000 steps, the learning rate warms up linearly from 0 to the maximum value. Then it decays to 0 following cosine schedule. The maximum learning rate 10-4 for the retriever and 10 for the generator. When training the retriever, we sample 3 negative premises for each example, including I in-file negative premise. When training the generator, we apply dropout retrieved premises with a dropout rate of 0.5. Then, we truncate the generator's input to 2,300 tokens.
NVIDIA A A100 GPU with 80GB of memory. The code is implemented in
During evaluation, the tactic generator combined with best-first search find proofs. At each search step, it produces 64 tactic candidates using beam search. Each tactic associated with a log-likelihood score. In best-first search, we prioritize the states by the sum of likeliiels of tactics leading to that state.
C.2 The GPT-4 Baseline
Now we describe the GPT-4 27 baseline in Sec. 6 Similar to ReProver, it is a tactic gen- erator combined with best-first search. However, the tactic generator is based GPT-4's capability to follow instructions in zero-shot. Specifically, given a proof state, we use the following prompt to instruct GPT-4 produce list of tactics, each paired with confidence score:
Prompt Template:
You are an expert in Lean3 theorem proofs. We are trying to solve the Lean3 theorem ' TTHEOREMFUULL_C NAME" from the mathlib file FILE_PATH" The current tactic state is: 'TACTIC STATE'. Suggest exactly 35 unique tactics to progress in solving 'THEOREM FULL NAME along with their conf confidence levels as a float between and 1. Rank them in order of effectiveness. Present the tactics and their confidence levels as comma- separated tuples in this format: #(tactic_[1) confidence_ tic_(2}, confidence_(2)))
#(tac- .... # #(tactic_(35), confidence_f35 (it )
We adapted the prompt to particular theorem and state by substituting the variables with the appropriate values. Given the inherent variability GPT-4's outputs, we requested 35 and filtered out invalid ones. We used a token length limit of 1,024 and kept all other API parameters at their default values. Below are a few example prompts and GPT-4's responses:
Example Prompt 1:
You are an expert in Lean3 theorem proofs. We are trying to solve the Lean3 theorem 'polynomial, cwwbyshev.eeeeee www..aaaa....e.ee.......... aeval_U' from the mathlib file 'mathlib/ httrr//annlysissspciaalll
lean', http:////rroootoeie/eeeteeeeeeee
The current tactic state is: 'R Type u_1, A Type u_2, _inst_1
: comm_ring R, inst_2 comm_ring A, _inst_3 algebra R A, x : A, n N (aeval x) (chebyshev. R n) eval x (chebyshev.U) " Suggest exactly 35 unique tactics to progress in solving 'polyno- mial. cal.cchbyssev.cc beebyshev.aeval_U7 aeval_U', along with their confidence levels as float between 0 and 1. Rank them in order of effectiveness. Present the tactics and their confidence levels as comma-separated tuples in this format: #(tactic_(1), confidence_(1)) #(tactic_(), confidence_(2)) #(tactic_(3)), anfidence_(355)tt

---

Example Response 1:
# #(rw chebyshev U, 0.9)#, #(simp only [chebyshev. U] 0.9)#, #(simp_rw chebyshev. U, *,8)#, # (apply aeval_add, 0.75)# #(apply seval_mul, 0.75) #apply aeval_sub, 0.75)#, #apply aeval_X, 0,7)#, #(ap- ply C, #,7)#, # #(apply aeval_pow, 0. 0.7)#, #(ru |u2190aeval_pov, 0.65)) #(rw 2190aeval mul, 0.65) #(rw (u2190aevalladd, 0.65)#, #(rw (u2190aeval_sub O. H, #(apply aap_b 0.6)# #(intro ae- val aagaaaeebra_ap..c.o 0.6)#, #applly eval_map, 0.55) #(rw eval_map,
0.55)) #(apply seval, #.55)# # #(rw_for_targe aeval_eq_eval) 0.5)#, #(apply aeval_eq_eval', 0.5)#, ftr__for_target aeval_eq_eval" 0.5)#, # #(apply
ply deval_eq_offe ott__oo____s__slllrattttttte 0.45)# #(rw
0.45)#, # #(ap-
www_ssaaalaseeeeeee 0.4)# #(rw is is_scalar_tower aeval_apply,
0.4)#, # #(try_for 100 exact_mod bhebyshev.U_eq_reee #, # #(simp
at *, 0.3) #(simp Int.coe_nat..... wwt.coo__t_riinghoooeeee 0.25) #(apply cheby-
shev. Chev.U_i__por www.U_is_pooyymmal,, 0.2)) #(ru_algebra_mg
Segebra__mp__eeee map_eq_of ot_.e__ii___ooooeee___ee_e__eoeo
0.15) #,
#(unfold chebyshev. 0.1)## #(congr, 0.05)) #(change (chebyshev. U R 0.05)) # #(change (\u21d1 (aeval x) (cheby-
eval = chebyshev.U
shev. R n) chebyshev. A n), 0,05)), # (applyy_ful fun aeval x, 0, # (apply__fe fun eval 0.05) #, #(simp context md := reducible [], 0.01)
Example Prompt 2:
You are an expert in Lean3 theorem proofs. We are trying to solve the Lean3 theorem 'euler_sing sine. integral coseralllosssso ccs_pco_________ _tt_pos_pps__ from the math- 1ib file "matil.b/srre/mmalyyss//pppee
Veulor_sine_prod_eeee lean'. The current tactic state is: 'n N + 0 Suggest exactly 35 unique tactics J (x R) 0.. / 2, cos www..iiteeraa.ll................ petterral_cos_px__pee to progress in solving 'euler puler_sine... their confidence levels as float between and Rank them or- der of effectiveness. Present the tactics and their confidence levels as comma-separated tuples in this format: #(tactic_1, confidence_1)4t # #(tactic_2, conf confidence_2)) ..., # #(tactic_35, confidence_35).
along with
Example Response 2:
#exact integral_pos_dd _ww.imooooooooo_m_ooooooomoooo.a increasinng.on cos. cos.pow_antimge www.mmoooooono____........ in- creasing_ov creasing_onn_oot wwwooonooooooooooooooooooooo cass__ven__maee avven_nnreal, 0. # #apply if anttimmno__
increasing_on 0, # itw.raaaiiitrrblllittnneaalllll
#,90) #(ex-
act integral_pos.pre, 0,85)# F(nterval_intee.tinedoo 8, #(in- terval_ intaelggeeerrbbepps,,, 0.75)# #(exact integral_pos nonnenndintt_nn 0, #(exact val_ integrable_pos_right 0. 0, #(exact intograil.pos.offommme... o. +, #(rw of supporting, 0.45)# #(ww htteraa.p..sstt..trrrraa.iigggp. #, #applyy 0,35)# #(nom_caas apply_pos, 0.30) HCapply_pos_of__onncee
0.65) #(exact inter-
0.50)) #(rw interval_intterral.po.
poa.
0. 0,25) #(rw attervalinttrralppoooo..aaaaaai cos wtw_sllo_mmoooo_ppso 0. 1,) ht,.10H|_aacpyyyooaaaoooooooooo, 0.10)# # #eex- act 0, #(rw cotegpaal_poaooocmommmmottteette mos_possconsttatt_squueeeeee 0.06) cos.posscoctstttttssseeeeee
2. #use
0.09) #norm_cast apply_nonneg_por
0.0 #
0,) #usse art.gaalpee.oo...acauuueeeeeeer. 0.04)
# of wnt.s/oooottimmooo__mooooooooo wtt.:aaaiiiioo.ccccrrsiiinnooooo
0.03) #(inter-
#, (norm_caas cast
apply_pos_ of__onzero_ppss 0. 0, # (apply_pos_off soayypoo_ooooonzerrooo _pos, 005)
# (rw of_neeeeg_oottteeoooooooooeee monotone,
oooep 0.001)#
25

---

Data contamination is possible. Our GPT-4 experiments were performed in 2023, but many theorems and proofs the dataset have been publicly available on GitHub before GPT-4's data cutoff date (September 2021).
C.3 Justifications for Not Comparing with Existing LLM-Based Provers
In Table 2 we do not empirically compare ReProver with any existing LLM-based prover. Unfor- tunately, such a comparison is infeasible. Provers targeting different proof assistants are generally not comparable, so we focus the discussion on the three existing provers in Lean [66 importantly, they are impossible to reproduce with reasonable effort, due to private code and pretrain- ing data. Therefore, the only potential comparison is evaluate ReProver under their experimental settings and compare with the numbers reported in their papers. However, that is also impractical for numerous reasons:
17 19]. Most
The data is different. All existing methods used an outdated version of mathlib more than two years ago. We cannot use LeanDojo to extract data from this version. As mentioned in Sec. 4 LeanDojo only supports repos released after March 24, 2022. Also, we cannot use their dataset directly, since it does not contain premise information required by ReProver.
Lample et al. 77 trained on synthetic dataset named Equations, which not publicly available.
All existing methods co-train the tactic generator auxiliary tasks from the PACT dataset [[6]. Co-training increases the data/compute requirements by an order of magnitude, which cannot be afforded by us (or probably most academic labs). All existing methods were developed by researchers in the industry.
Polu al. [9] and Lample et al. 17 further finetuned their models on new proofs collected through online interaction with Lean, whereas method is only trained on human-written proof'.
The tool for interacting with Lean may impact the performance. Han et al. [16] and Polu et al. [19 used gym, which has severe limitations (Appendix A.2 Lample al. developed their own private tool, which is not publicly available.
Most of these difficulties are due to the private nature of existing methods. By releasing our code and models, we take a major step in establishing accessible baselines for future work to build upon.
C.4 Evaluation on MiniF2F and ProofNet
We evaluate our ReProver model on Mini 28 and ProofNet 29 (Sec. 6 to test its capability in proving theorems outside its training data distribution. We use the same hyprrparameters and evaluation setup as the previous experiments (Appendix C.I.
3at. 8a061388c66669888 0066)/88000000000 Meta's version of MiniF2F [17. ReProver achieves Pass @ of 26.5% on the test set, which is competitive with state-
MiniF2F. We use the commit 527 (dcccddd7777788111111 5cf
of-the-art art methods without reinforcement learning (25, 9% in Polu et al. [19). Moreover, ReProver can prove 33 theorems that currently do not have Lean proofs (examples in Fig. Bp. For the complete list of 33 new proofs, please see our pull request to MiniF2F.
There caveats about quantitatively comparing ReProver with existing methods on MiniF2F. Many difficulties in Appendix C.3lstill still apply, e.g., different tools for interacting with Lean may impact the performance. Also, MiniF2F is test-only dataset without training theorems, and existing methods focus on reinforcement learning (RL) to learn from proofs collected via online interaction with the proof assistant [17 [9] In contrast, ReProver is trained via supervised learning on static dataset, so we only compare with the non-RL baseline in existing methods (Polu et al. [19] achieves Pass @ of 25.9% without RL and 29.6% with RL). Furthermore, we do not compare with Lample et al. [T]] due to differences in the evaluation metric. They use Pass@ @6,, which requires running the prover on each theorem 64 times. We use Pass @ 1, and it already takes one day for single evaluation on MiniF2F's test set. Therefore, evaluating Pass @ 64 would be too computationally expensive for the resources we have access to. Finally, MF is available multiple proof assistants [8 69 70). Results across different proof assistants are not comparable, so we only compare with existing work in Lean.
ProofNet.
We use the commit Prover can prove 48 out of 349 theorems, achieving a Pass @ 1 of 13.8%, which is the first reported
ProofNet. Re-
26

---

theorem mathd mathd_numberthee www.nnneneeerrye2222
( in (finset. range 101), k) % 6
begin
[finset. sur_rtttssmaaneeeeeeeeee rai__rrane__ucce sunse_sscc',, norm_num [finset. sum ranng___nng___ end
theorem mathd hotrndnnmmerrrrryy.oomom __5
(2>2010) ==
begin
norm_num [pow_succ]
end
theorem mathd_numberthheory
(n N)
(he n s 9)
(h: 11120 * 100 + 10 * 7)
n = 5 :=
begin
contrapose! h,, norm_num [h.],
dec_trivial!, end
theorem mathd algebra_662 _16
(f R R)
(he x, f = x + + 1) 1)
(h1 x,
f (g 1) :=
begin
simp only [ho, h1, pow_one],
ring,
end
Figure B: Examples of new proofs discovered by ReProver on MiniF2F 28
theorem proving result ProofNet. Moreover, 39 out of the 48 proved theorems do not have existing Lean proof's (examples in Fig. []. and 3 of them can only be proved with the help of premise retrieval (Fig. D). We have contributed the 39 new proofs ProofNet, which helped them reveal and fix problems in the formalization of 7 theorems (details in our pull request).
D LeanDojo for Lean
Lean and Lean two incompatible major versions of Lean and both are widely used. Lean 3 was the latest stable version until recently (June 2023). Also, Lean 3 and Lean 4 have separate versions of mathlib. The Lean/mathlib community has recently finished porting theorems and proofs from mathlib 3 to mathlib 4 [TOO]. Therefore, Lean 3 will gradually become deprecated, and future Lean projects will be using Lean Therefore, it is important for LcanDojo to support Lean 4.
Since Lean 4 is relatively new, we are not aware of any existing work on learning- theorem proving in Lean Furthermore, no existing tool is available for extracting data from Lean LeanDojo fills in this gap and fully supports Lean 4. Given any repo in Lean 4, LeanDojo can extract
"attps://eeapproree github. http://wwwrgiiiit..o///eee/////e htt//eean//bo//eeaaattaaagggee/ html
27

---

theorem exercise_2_32 {G Type*} [group G] (a b G) 3 G, * a begin
* b * gm :=
exact (b, by simp), end
theorem exercise exercise_11____1 (a (of_int a gaussian_ _intt begin
int a
contrapose,
simp, end
theorem exercise_1_1 ____1_ {G Type*) [group G] fx G} in N (hxn: order_o x n)
x-1 = (n 1 : Z) :=
begin
rw zpow_sub_one,
simp,
rw [- hxn, pow_order__f_ee__nne
end
theorem exercise Saarciseee___22000 3_1_22b {G Type*} [group Type*)
subgroup (hH :
I, subgroup. normal (H i))
subgroup. normal (n (i I), i):
begin
infi,
-set. i-set.imag__uniy
Inf Inf_image,
simp [hH],
haveI := i, (H i). normal, split,
intros hx g, rw subgroup. mecuup.emmuiae mem_infiiiiiiieiiieee at hx H,
intro i,
apply (hH i) ct.coojjmaa mem (hx i),
end
theorem exercise_3.1 ____________a____ {G : Type*} [group G] subgroup G) [is_ sol_ablee is_ solvable :=
begin
apply ipply_instance, end
Figure C: Examples of new proofs discovered by ReProver on ProofNet 29
data, including file dependencies, ASTs, proof states, tactics, and premise information. In addition, enables the model to interact with Lean 4 through tactics, in the same way as Lean 3 (Sec. 4
Similar to constructing the Lean 3 version of LeanDojo Benchmark, we extract data from the commit 3ce43c18ff1 4b76e 161991 1b75a3e 1e644462066 of mathlib4 released on October 21, 2023. The resulting dataset is named LeanDojo Benchmark 4. It is released under the CC BY 2.0 license and hosted on zenodo.org with DOI "10. 5281/zenodo. 8040109". LeanDojo Benchmark consists of 102,514 theorems/proofs. 213,067 tactics, and 152,695 premises. We use 2,000 theorems for
28

---

theorem exercise_ 13_ 13_6_10 {K Type*) [field K] [fintype K*] (x K*), = :=
begin
exact finite field. prod_um _ni___units______________ ee_neg_one, end
theorem exercise_1_1
(n N)
(x y euclidean_spaa (fin n)) - R
lix + yll llx yl 2*|1xiI~2 + 2+1ly|l := begin
rw Inorm_add_sq, reall,, hamm__uu_pow.____ Bacpo_powtww_rrrreeeeee tea_ttto_rel_l real],
ring, end
theorem exercise_2 2_25 {K Type*} [metric_sppae spacee_peeeeeeeeeeee__ K] [compact_space K] (B (set K)), countable is_topological __basis
begin
rcases ceasts_couttable _esisssbbbsss____e K with (B, hBc, hB),
exact (B, hBc, hB.2),
end
Figure D: Three new proofs discovered by ReProver on ProofNet 29 that cannot be found by baseline without premise retrieval. All of the three proofs rely on premises: wwtppprrrdddddieeeeeeepppppppppp uniu www.nuuutiddd... ses__ddd___ee__onee
"finite_ prod_
"norm_add__ uadd_sq_real" "norm_sul pow__wo_real"" and "exissts_coutable__u basis".
validation, 2,000 theorems for testing, and the rest for training. LeanDojo Benchmark 4 also has two different data splits: random and hovel_premises.
We use LeanDojo Benchmark 4 to train and evaluate our method. The model architectures and experimental details are the same as those Sec. Results on premise selection are in Table and results on theorem proving are in Table
Table B: Premise selection testing performance on LeanDojo Benchmark 4 (Lean 3 results in Table T]. We train and evaluate models independently using different data splits (random and novel-premiss R @@k is the recall for the top & retrieved premises, and MRR is the mean reciprocal rank metric.
Method
random
novel _ivel_premiss
R@D 1
R@ 10
MRR
R@1
R@ 10
MRR
Ours
12.8
34.7
0.29
9.8
32.1
0.24
Table Theorem proving Pass@1 (%) on the testing data of LeanDojo Benchmark 4 (Lean results in T
Method
random
novel_premiser
ReProver
48.6
19.9
W/o retrieval
44.5
16.2
E ChatGPT Plugin for Theorem Proving
LeanDojo provides general tool for interacting with Lean programmatically. As demo of how it might bridge L.LMs and theorem proving, we build a ChatGPT plugin [TOT] enabling ChatGPT to prove theorems by interacting with Lean through LeanDojo. Plugin developers wrap any software
29

---

as web service and describe its APIs to ChatGPT. Then, ChatGPT can automatically call the APIs and incorporate the results into the response to the user. Below is summary of our API description corresponding to the interface in Sec.
Title: Lean
Description: Plugin for proving user specifeed theorems automatically by interacting with Lean. The user enters information of how to find a theoren (e.g., theorem name and file path). Based on the user's input, ChatGPT first initializes the proof search with the given theorem as the initial state. Then, ChatGPT will first explain the choice for the next tactic step using LaTeX and run that tactic step to the state. ChatGPT can backtrack to previous states by decrementing the "state_id" parameter. current state specified by the "state_id" parameter returns an error message, ChatGPT should explain the error, and repetitive errors occur, ChatGPT should decrement the state_id" parameter and try a different approach on a previous state. The theoren is successfully proved if there are no unsolved goals in the current state
current state is not promising,
applying tactics to the
Endpoints:
initialize.proff_eeet
Given the theorem name and file path of a Lean theorem, initialize the proof search. The response includes the initial state and its state ID.
Args:
theorem_namm (string): The name of the target theoren to prove.
theorem_file.cee (string): The file path of the target theorem.
run_ Run a tactic on a state (specified by its state ID), assuming the proof search has been initialized and some state available. The response is either the next state and its state ID an error message, in which ChatGPT should explain the error and consider decrementing the "state_id". Args:
state_id (string): The ID of the state which to run the tactic.
tactic (string): The tactic specified by its state ID), assuming the proof search has been initialized.
state (
After exposing the APIs to ChatGPT, we can ask it to prove theorems by specifying the theorem's 's name and path in any public Lean repo on GitHub. Fig. H show an example with the GPT-3.5 version of ChatGPT. And Fig. M are the same example with the GPT-4 version. The captions provide detailed step-by-stey step explanations.
We highlight a few key strengths of ChaiGPT observed in multiple examples we evaluated. First, unlike specialized methods for theorem proving (this paper and its prior works), ChatGPT interleaved informal mathematics with formal proof steps. This resembles how humans interact with proof assistants and opens up new avenues for integrating natural language and formal theorem proving. Second, ChatGPT demonstrated impressive capability explaining error messages from Lean that are quite opaque even to humans. It was able to incorporate the enror message to refine its proof strategy. Last, ChatGPT's behavior more steerable than specialized provers. Fig. F we simply gave it the theorem to prove, but could also provide more detailed instructions. For example,
30

---

could say: "Please describe high-level proof plan before trying any tactic." This kind of steerability enables future research on prompt engineering for theorem proving, and we have already seen initial benefits in an ongoing work named Sagredo [3]
However, these strengths failed to find proof for most theorems we tried. Hallucination was common. In Fig. L ChatGPT falsely asserted the theorem was proved, while we knew it was not, by looking at Lean response. This demonstrates the value of theorem proving as a rigorous benchmark for addressing LLMs' hallucination problem. Another key limitation of ChatGPT was its inability to search systematically in large space. We frequently found it stuck to an unpromising path when the correct solution could be found by backtracking and exploring alternative paths. This behavior is consistent with the general observation that LLMs are weak at search and planning. Addressing this weakness is an active area of research 102
means imply ChatGPT already solve theorem proving. In fact, it
We emphasize a few caveats about our study of theorem proving with ChatGPT. First, data con- tamination likely. Many theorems we evaluated have been publicly available on GitHub before ChatGPT's data cutoff date. Therefore, ChatGPT may have seen them in training. Second, our study exploratory. more detailed and quantitative study is needed characterize ChatGPT's capability in theorem proving. Such a study with ChatGPT plugins is challenging, as plugins currently only support interaction through the browser. Also, OpenAl has taken measures block automated access by bots. Using humans may be an option, but that is beyond the scope of this paper.
want you to prove theorem in Lean. The theorem's name is 'hlloo, world' aad It is defined the 'rr//exappleJean" httts//jitob.ommmannyylllaaaaaaa
S
Used Lean
LOCALHOST
REQUEST LEANDOJO
"thecren_ nane": "hello, world'
"thecron, saccsson_rillppaee rill__ath" 'axo/exangle.2ee
RESPONSE FROMLEANDOIO
"state, id';
"state': : "a b Man a
The theorem 'hello, world' states that for three arbitrary complex numbers "a', 'b", and 'c', the
equal the sum b'. In other words, asserts the commutativity addition for complex numbers. goal prove this statement:
Copy
c
C
Figure E: (ChatGPT-3.5, 1/8) After receiving theorem to prove, ChatGPT first called "initialize", which returned the initial state. Then it tried to interpret the theorem in natural language. Note that it made mistake here. The theorem was about natural numbers (N), not complex numbers (C).
31

---

To prove this, we can use the fact that addition is commutative for real numbers, and complex numbers are composed of real numbers. Let's start by using the "zw' (rewrite) tactic to apply the commutativity of addition to the middle term "b c'
Used LeanDojo
LOCALMOST
REQUEST TO LEANDOJO
istato_id": 9,
"tactic":
RESPONSE FEANLOANDOUO
'('arror:: 'gen, tac, and capture, ree, failed: pos-(some (1, 21) mag-\"roarite ractic failec. did not find instance the pattern in the target expzessioni statoo MM
ay", proof, finished': False]"
looks "xw" tactic failed apply the commutativity addition to the middle term
c The error message indicates that the tactic not an instance of the pattern
c' in the target expression.
The issue is that the "xw" tactic not able match pattern e' the expression "a
b c' because addition is associative, and Lean is treating the expression as "(a b)
Figure F: (ChatGPT-3.5, 2/8) ChatGPT tried to rewrite the goal using the lemma "b + c b". This reasonable but incorrect move. After receiving the eиror message from Lean, ChatGPT explained the error in natural language. Here the explanation is quite accurate, which impressive given that the error message looks opaque anyone not familiar with Lean.
Limitations and Future Work
Our work one step toward unlocking the potential LLMs for generating verifiable formal proofs, and see abundant space for future exploration. learning- based prover is complex system consisting multiple components: data extraction, interaction with proof assistants, model training, and proof search. While navigating the design space spanned by various components, side of simplicity and efficiency, instead of pushing performance to the limit. This helps us deliver reliable, open, and accessible system, laying the foundation for further research. There many directions in which the system can be improved, and we discuss a few of them here
on the
Stronger LLMs. Our backbone model, ByT5 44,, was published in 2021 and has 299M parameters, which is very large by today's standard. Recently, there have been plethora of open-source LLMs demonstrating strong capabilities in writing code, e.g., CodeGen [103]. StarCoder [94), and how they might impact theorem proving and, more generally, how far we can by pushing the limit of the model/data scale.
CodeGeeX [104] We are excited
ByT5's fokenizer-free nature helps sidestep the difficulty with pretrained tokenizers that may not work well for Lean's 's Unicode-rich code. However, treating texts as raw bytes makes the sequence length much longer than necessary. Long sequences harm efficiency, Transformers scale quadratically w.r.t. the sequence length, which may become a bigger problem when we further seale up the model. To solve the issue, it might be helpful to pretrain customized tokenizer adopt more advanced tokenizer-free models such as MegaByte [105..
Our ReProver model is based on the following LLMs such as GPT-4 (7 has led to successes in many applications by prompting the model without any finetuning. Our preliminary results show that GPT-4 and ChatGPT (Appendix
paradigm. Recent work instruction-
Additional limitations:
32

---

To address this, we can use the 'ring" tactic, which is a powerful tactic for solving equalities involving basic arithmetic operations. Let's try using the "ring" tactic to prove the goal.
REQUEST LEANDCJO
"state_id": C, 'tactic": "xing"
RESPONSE FROM LEANDOJO
"('ezzor': gen, tac, capture, res, failed: posenonn rageV/prree itactic fuiled "zirg'\" tastic, state=\'a b M\n- False]"
bi" 'proof finished';
seems the "ring" tactic available in the context, indicated by the message "parse, itactic failed 'ring
In that case, let's different approach. commutativity addition complex numbers, ihich given by the lemma _od_conn
the 'apply tactic apply
O)
Let's use the 'apply" 'aattc apply this lemma the
subterm goal.
Used LeanDajo
LOCALHOST
REQUEST LEANDOJO
'state, idf:: C,
"tactic": "apply (add_corm b e)*
RESPONSE FROM LEANDOJO
"('error'; 'gen, capture, failed: pos-(sone iinvalid apply tactic, fasled to unifyl'n a + = bilmmstn)nn a bi* tactio_ stato=)*a NMm
by"" 'proot findshed' 's False]"
It looks like the 'apply" tactic failed to unify the goal
with the
b The error message indicates that the tactic was unable to match the entire with the lemma.
lemma
Figure G: (CharGPT-3.55, 3/8) Then it tried to prove the theorem using "ring". This was another good move. The ring tactic can prove this theorem, but Lean could find it since it was not imported into the current file. Again, ChatGPT was able to interpret the eтrоr message correctly and concluded that ring was available. Next, tried another tactic but failed again.
and E) cannot solve theorem proving out of the box and are currently far behind finetuned models. However, the way we prompt these models quite naive, and better strategies, such as Tree of Thoughts [102], may lead to further improvements. We consider theorem proving promising task for studying L.LMs' capabilities planning and search.
Improving Premise Retrieval. ReProver uses DPR 26 to retrieve premises and fuses them with the current proof state by concatenation. This architecture is simple and effective does not scale to large number of retrieved premises. With a length limit of 2,300 tokens, we can fit only 10-15 premises into the input of the tactic generator. mitigate the problem, we may need an architecture that fuses the retrieved premises in the hidden space, e.g., Fusion-in -n-oooeeerr [166).
33

---

To resolve this, let's use the "apply. Eun tactic, which allows us to apply function to both sides of an equality. We can use aaplyy_ _un to add "a" to both sides of the lemma "b b which will g lvv us the desired goal. Let's try this approach.
Used LoanDojo
LOCALHOST
REQUEST TO LEANDOIO
"state, 10": O.
"tactic"; "apply,
using
RESPONSE FROM LEANDOJO
"( ('ezzorr' 'gen, tac, ttc.ttaaaaaaaaaaeeeeeee capture, .zes, foiled: posmnonn magel "parse, itactic failed "apply fun (A x) using bi", "proot #insshed": False))
e'\" pactic.stateml b Ma
seems that apply_fun tacticis not available the current context, as indicated by the error message "parse, itactic failed on "apply_ _un x, at using add comn
Given the limitations the available tactics, we can take more direct approach by using the "have" tactic to introduce an intermediate equality. Specifically, we can introduce the equality 'h
using the "'dd_comm comn lemma, and then use this equality to rewrite the goal. Let's try this approach.
LeanDojo
REQUEST TO LEANDOJO
"state_id"; D, "tactic": "have
add
RESPONSE FROM LEANDOID
"('error" igee_tac_aaeee ael_add_appttt prd_ccp res, ree__eee_leeeeeeeeeeeeeeerrrrese failed: posn(sone (1, 421) mege) 'zewrite tactic fazled, did not find instance of the pattern in the target expressiontin b ci state=)*a Voh proof, finished': False]"
It looks like the "xw" tactic still failed to apply the intermediate equality 'h cecc b to the goal 'a b
b". The error message indicates that the tactic did not find an instance of the pattern e" in the target expression.
Figure H: (ChatGPT-3.5, 4/8) ChatGPT made another two failed attempts. Here, the second attempt had the same problem as in Fig. ("4" is left associative).
In addition, one can also switch from DPR to radically different retrieval architectures. For example, generative retrieval 109 is recent class of models performing retrieval by directly predicting the document IDs, which could be the premise names in our task.
Linitations of Imitating Human-Written Proofs.
Human-writter proofs extracted by LeanDojo provide valuable data for training the prover. However, we have also observed limitations of using them as the sole training target:
First, they are relatively searce for today's data-hungry LLMss. LeanDojo Benchmark has 98,734 proofs, covering large portion of available data in Lean (as of October 2023). The number of proofs
34

---

To address this, use "simp" tactic, more powerful tactic for simplifying expressions. The "simp"
automatically apply the commutativity adcition simplify the goal. Let's try using the 'sinp" tactic to prove the goal.
LeanDojo
LOCALHOST
REQUEST
'state, id"; O, 'tactic"; "sinp"
RESPONSE FROM LEANOOLO
ercor': 'gen, tac.ttatccaaaaaaaaaaaaa captuue, res, failed: pas=(sona (1, 21) neg-\"sinpliff feiled to simplity"" tactic, staliccttttt"aa Vi-e- 'proof, finished'; Fallse)"
bi"",
seems that the "sinp" tactic also failed to simplify the goal
The message indicates that the tactic failed simplify the expression.
Given the limitations of the available tactics, let's try different approach. We the "zw" tactic apply the commutativity addition to the subterm
the goal. This
will allow rewrite the goal
Let's this approach.
Used LeanDojo
LOCALHOST
LOLANNDOOO
"tactic": : "Iw add_comm b"
stato_id'; 'state': Min- False]"
proof #inished's
After applying commutativity of addition the subterm 'a b we have successfully rewritten the goal a The updiated goal
lean
Copy oode
Figure I: (ChatGPT-3.5, 5/8) ChatGPT tried to simplify the goal using the simp tactic but failed. Then tried the "rw add comm b" tactic, which successfully rewrote the goal from "a + b" b =
in other proof assistants has the same order of magnitude (tens or hundreds of thousands). Due to limited data, we cannot constantly improve the performance simply by scaling up the model size. Second, theorem proving in proof assistants is an interactive process, but the proof only captures the final successful trajectory. Without the intermediate history of trial and error, it can quite opaque how final proofs are derived. Therefore, tactics in human-written proofs can be difficult for the model learn from. Third, models trained on proofs in one project often struggle to generalize to theorems in new domains [9] 120), e.g., from mathlib to MiniF2F and ProofNet (Appendix C.4
35

---

Now, we can use the "rw' tactic again apply the commutativity addition to the subterm in the goal. This will allow us to rewrite the goal as 'b try this approach.
Let's
LeanDojo
REQUEST TO LEANDOOO
"state_sd": 1, "tactic": "sw add, corm
RESPONBE LEANDOJO
"('state_id" 'state': bab b Mar False)"
b',
"pzoof_ finished':
After applying the commutativity of addition the subterm c' we have successfully rewritten the
The updated goal is:
code
Figure J: (ChatGPT-3.5, 6/8) Then it successfully performed another rewrite from "b a c bo "b
b".
To overcome these limitations, existing work has explored learning from auxiliary data data collected via online interaction with the proof assistant. For example, Proof Artifact Co- Co-Training (PACT) co-trains the tactic generator on nine auxiliary tasks, such as predicting types and theorem names [6]. MetaGen 38 trains a neural network to generate synthetic theorems/proofs as training data in the Metamath proof assistant [110. Polu et al. [19 and Lample et al. [7 improve the prover by training on successful proofs found by itself. Incorporating these techniques into our system may lead to substantial improvements.
36

---

Now, we can use lactic one more apply commu lativity of addition subterm
goal. This allow rewrite the goal
b which matches the right-hand side original goal. Let's try this approach.
Used LeanDojo
LOCALHOST
REQUEST
'state,1d"; id": 2, 'tactic"; "Iv ado cdom b a"
RESPONSE FROW LEANDOJO
"("stato_id": 3, 'state': M False?"
prood,
After applying the commutativity of addition to the subterm "b we have successfully rewritten the goal as b b' The updated goal is:
lean
Copy code
Figure (ChatGPP-3.55, 7/8) Another rewrite tactic, transforming the goal to b + b".
Finally, tactic time apply commutativity of addition subterm the goal. This will allow rewrite goal
which matches original goal and completes proaf. Let's finish the proof.
Used LeanDojo
LOCALHOST
"state_sd"
"tactic": ; "zw add comn
LEAMMED
"('state_aae 'state": False)"
Mine
"proof, :inished::
looks like the goal 'a
b" remains unchanged after applying the
commutativity of addition to the subterm "c This because the goal already in the
desired form, and the proof is complete.
Since the goal matches the original statement of the theorem, we have successfully proved the theorem 'hello, world", The proof demonstrates that for three arbitrary complex
numbers 'a', "b", and "c", the sum confirms the commutativity of addition for complex numbers.
is equal to the sum
b. which
Figure L: (ChatGPT-3.55, 8/8) It performed one last rewrite, which brought the goal back to the original goal "a without making meaningful progress. However, it asserted that the theorem had been successfully proved, even though the response from LeanDojo clearly indicated "proof finished: False".
b". At this point, ChatGPT went back the starting point
37

---

want you prove theorem Lean. The thecrem's Dello_workds and defined the file src/example.ean in htttss//itthubbooom//a/y//////ae
Used LeanDojo
LOCALHOST
REQUEST TO
"hello, world",
"theozen, file, psth" "sxc/exarple.. wea.nleeeeenn
RESPONSE FROM FANDOIOO
"state": b Mn
The theorem hello, world' statedd as follows:
For any three integers 'a', "b" and "c", the sum "a o' is equal to the sum "a
other words, asserts the commulativity of addition integers, which as well-known property of integers, Let's start the proof. The first step is to apply the "rw' (rewrite) tactic
with the 'add, assoc" lemmma, which statess that "(a b)
(b This will
allow us to rearrange the terms sum.
LeanDojo
REQUEST
"state id":
"Luctic" "Iw add, assoc*
RESPONSE FROM LEANDOJO
'C'state.id"s
finished's
Falee)
After applying the ''dd_assed assoc
lemma, we have new goal:
any integers and sum
eequllt sum
Figure M: (ChatGPT-4, 1/3) The same theorem using the GPT-4 version of ChatGPT. Despite minor eтror when interpreting the theorem (natural numbers, integers), generated sensible tactic. rewriting the goal to "a + (b c) = b".
38

---

The next step is apply the "zw' (rewrite) tactic with the 'add_comn' lemma, which states that bb b This will allow us to swap the terms "b" and the sum.
Lean
LOCALHOST
REQUEST
"tactio": : "Iv add_comm c*
"('stttoidd" 'state's Wine to #inished': False)"
applying add__com comn lemma, have new goal:
any integers
b)" equal
Figure N: (ChatGPT-4, 2/3) A good move, rewriting the goal to "a + (c b)
b".
39

---

Now, we can see that the left-hand side and the right-hand side of the equation are Idiettical. Therefore, we can finish the proof by applying the 'zefl' ttactic, which asserts that any mathematical objjet equal to itself.
LeanDojo
REQUEST LEANDOJO
"siate, ;i";: 2, "tactic"; "rofl"
LEANDOJO
"C'erzor' 'gen, tactic, Iwiled to unifylin # failed: b Milm- (e b) + ht" "proof, Finished's False])
roge) "invalid apply
blAmmttnil 7m ?t,21"
tactic, stater) tactic,atater"
It seems there was an error when trying to apply the 'refl tactic. This error occurred because the Lean prover expected the left-hand side and the right-hand side the equation to be syntactically identical, but they are not due to the parentheses.
To resolve this, we can apply the 'add assec" lemma again to remove the parentheses on the left-hand side. This will make the left-hand side and the right-hand side syntactically identical, allowing us to apply the 'refl' tactic.
LeanDojo
LOCALHOST
REQUEST TO LEANDOJO
"state, id"; 2. "tactio"; "Iw +add, azgoe"
RESPONSE FROM LEANDOJO
'U'pzoot, sinsshet Txuel"
applying 'add, assoc lemma again remove parentheses, For any integers and sum
equal the
Now, the left-hand sidee and the righl-hand side of the equation syntactically ideettiall.
Therefore, the theorem is proved. The proof finished.
Figure O: (ChatGPT-4, 3/3) It tried the refl tactic but failed. refl requires the goal to be an equation whose both sides are identical up to trivial transformations. However, "a (c + b) a + + b" trivial since "+" left associative. ChatGPT was able interpret this error accurately and finish the proof using the correct premise "add_assoc",
40


Reviews:
[{"review_id": "uU2mfWfOCb", "reviewer": "Reviewer_CZ3x", "summary": "", "questions": "", "limitations": "**Questions/Suggestions:**\n- The authors clearly indicated which mathlib3 commit / ProofNet commit uses to extract the data and that LeanDojo cannot extract those (somewhat rare) theorems that are defined using the keyword “def” (see line 169 from the appendix).\nIt would have been very helpful though, if the authors had given a precise number of how many such theorems actually are in that commit so that we don't have to rely on a somewhat vague adjective of \"rare\". Would it be possible to do that?\n\n- LeanDojo doesn't support Lean proofs that are not based on tactics; although the authors state (line 254) that \"tactic-style proofs [...] are sufﬁciently general since any proof can be converted to a tactic-style proof\", which vindicates their approach.\nNonetheless, to ease the burden on the reader regarding the details of the Lean system, would it be possible to add a small paragraph or a reference that explains why (and how) a proof not based on tactics can be converted to one?\n\n**Observations:**\n- LeanDojo for Lean4 is only in alpha stage. But I am confident the authors will work towards the goal of advancing that codebase as well.\n- data contamination when using GPT-4 for tactic generation (line 340) is acknowledged\n- appendix C.3 contains a detailed and convincing account of why a comparison with LLMs is not meaningful\n- For Lean 4, LeanDojo Benchmark 4 is generated, but ReProver is not trained because a dataset split cannot be performed since premise extraction is not yet implemented.\n \n(Lastly, I have some doubts about whether a premise selection approach will ever be able to be scaled to the point where mathematical statements --formalized in Lean-- that are currently unproven statements on the frontier of mathematical research will generate a proof; but this is not a criticism of this paper, but rather of the general research direction.)", "rating": 9, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "**Overall Strength:** \nAs mentioned in the *Summary and Contributions* section, this paper fills an essential gap in the literature by making research in the domain of formal theorem proving *accessible*. As the authors also state in their paper, there are several other papers that deal with automatic theorem proving but suffer from not open-sourcing the dataset/environment, model, or both. Unfortunately, it seems that for some papers, after they have been accepted, the code is not provided. This shows the importance of being up front with data, which the LeanDojo paper achieves.\n(To illustrate the point above, consider the paper [1] (which the authors cite). Even though in that paper, the authors state in the Checklist (section 7) that \"the code for the Equations environment will be open-sourced. We also plan to make our trained model publicly available to help people in the formal community\", it seems this has not been followed through. I was not able to find the mentioned code/models, there seems to be no GitHub repository -at least not one that can be easily found- by any of the three main authors of that paper; and the code listed on the Openreview site of that paper [2] seems to point to existing Github repositories of Lean etc. rather then this code. I\n[1] G. Lample et al., HyperTree Proof Search for Neural Theorem Proving, https://arxiv.org/pdf/2205.11491.pdf\n[2] https://openreview.net/forum?id=J4pX8Q8cxHH )\n\n\n**Other noteworthy points:** \n\n- the paper consistently uses best practices (reproducibility - e.g., specifying exact commits on which the version of mathlib3 they base their paper on; training - hyperparameters, training setup, etc. are all carefully specified; comprehensive section on *Related Work*)\n\n- the paper bases its environment on Lean 3, but also considers Lean4 (in the supplementary materials) and hints that Lean4Dojo will be made available for Lean4 as well. This is very important since progress on Lean4 and mathlib4 is developing rapidly, and it is expected that Lean4 will become the standard in the near future.\n\n- issues in lean-gym are noticed, their root cause is identified (appendix A.2), and these are fixed by LeanDojo.", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": ""}, {"review_id": "CW9hKTUc9M", "reviewer": "Reviewer_crGr", "summary": "", "questions": "", "limitations": "The paper does have an extensive limitation section in the Appendix.", "rating": 8, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "- A new dataset for building stronger theorem provers\n- A benchmark for fair and reproducible comparison of theorem provers\n- An efficient retrieval-based approach that outperforms prior work.", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": ""}, {"review_id": "sVs8J3uo5o", "reviewer": "Reviewer_AsmJ", "summary": "", "questions": "", "limitations": "Limitations have been comprehensively discussed in the supplementary material. There seems to be no direct societal impact with this work.", "rating": 9, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "* This work contributes very valuable open resources to the theorem proving community. It is also very relevant to the broader AI community, since theorem proving is one of the most difficult open problems in AI.\n* This work also has potential to make open-source contributions to the Lean interactive theorem prover. It is shown in the paper that the proposed model automatically found new proofs for dozens of theorems in the library that are still missing proofs.\n", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": ""}, {"review_id": "YXLZHL6aFW", "reviewer": "Reviewer_xf1r", "summary": "", "questions": "", "limitations": "The content of this article is very comprehensive and substantial. It is a very interesting and excellent article.", "rating": 8, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "(1) the authors introduced LeanDojo, an open-source tool for theorem proving that fills the gap in existing resources. In addition, they proposed a retrieval-augmented prover named ReProver, addressing the critical issue of premise selection in theorem proving.\n(2) they have significantly reduced computational requirements, making it possible to train the model within five days on a single GPU. This increases the model's practicality and accessibility.\n(3) the paper is committed to the open-source ethos by providing the data, model, and code to the research community. This contribution will significantly facilitate further research in this field.\n\n\n\n\n", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": ""}, {"review_id": "qN2EXX7wey", "reviewer": "Reviewer_fFD9", "summary": "", "questions": "", "limitations": "There is probably no potential negative societal impact of their work.\n\nThe limitations of the method has been briefly mentioned, but not explained (in contrast to the limitaions of the competing methods).\nFor example, the authors explain why lean-gym fails to type-check 21% of the proofs, but do not explain why Lean Dojo failes to proof-check 1.4% of them.", "rating": 7, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "Lean is one of the most significant theorem provers and its size is very appropriate for machine learning. Given that the community is very actively \"translating\" mathlib to Lean 4, the work here might be of interest to many members of the community.\n\nThe paper is well structured and does not go into too many details regarding Lean, so it is accessible to the machine learning community. All the components of LeanDojo are well described, and the paper is easy to follow.\n\nThe experimental setup is mostly well-designed and the results are encouraging.", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": ""}]

Author rebuttal:

Meta-review: The paper introduces an open-source environment (LeanDojo) to extract proof trees out of Lean3, together with the premises of those proofs. These exacted proof trees are then used to build a new dataset for building stronger theorem provers.
Finally, this dataset is used to train a sota retrieval augmented automated theorem proving model (ReProver) which performs premise retrieval. This model outperforms GPT-4 on tactic generation, and also finds proofs to theorems in the library that are missing proofs. This model also uses significantly less compute that previous models i.e. one GPU for 5 days. 

Strengths:
1. This paper has overwhelming support from all reviewers.
2. The paper fixes issues with previous environments LeanStep and Lean-gym and advances the sota quite considerably in this area.
3. The paper execution is thoughtful with excellent and user-friendly documentation, and uses the very best practices.
4. Unlike previous works with empty claims to be open source, this paper is actually already open-source, and will help the community make large strides of progress.

Weaknesses:
1. The only main weakness is that the paper can be hard to understand for folks outside the area of theorem proving - but the authors have taken efforts to address this in the rebuttal.
Decision: Accept (Oral)