LeanAgent: Lifelong Learning for Formal Theorem Proving
Authors: Adarsh Kumarappan
Mo Tiwari
Peiyang Song
Robert Joseph George
Chaowei Xiao
Anima Anandkumar
Venue: ICLR 2025 Poster (2025)
Keywords: Theorem Proving
Formal Theorem Proving
Neural Theorem Proving
Lifelong Learning
Formal Mathematics
Large Language Models
LLMs
Curriculum Learning
Proof Search
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)

Abstract: Large Language Models (LLMs) have been successful in mathematical reasoning tasks such as formal theorem proving when integrated with interactive proof assistants like Lean. Existing approaches involve training or fine-tuning an LLM on a specific dataset to perform well on particular domains, such as undergraduate-level mathematics. These methods struggle with generalizability to advanced mathematics. A fundamental limitation is that these approaches operate on static domains, failing to capture how mathematicians often work across multiple domains and projects simultaneously or cyclically. We present LeanAgent, a novel lifelong learning framework for formal theorem proving that continuously generalizes to and improves on ever-expanding mathematical knowledge without forgetting previously learned knowledge. LeanAgent introduces several key innovations, including a curriculum learning strategy that optimizes the learning trajectory in terms of mathematical difficulty, a dynamic database for efficient management of evolving mathematical knowledge, and progressive training to balance stability and plasticity. LeanAgent successfully generates formal proofs for 155 theorems across 23 diverse Lean repositories where formal proofs were previously missing, many from advanced mathematics. It performs significantly better than the static LLM baseline, proving challenging theorems in domains like abstract algebra and algebraic topology while showcasing a clear progression of learning from basic concepts to advanced topics. In addition, we analyze LeanAgent's superior performance on key lifelong learning metrics. LeanAgent achieves exceptional scores in stability and backward transfer, where learning new tasks improves performance on previously learned tasks. This emphasizes LeanAgent's continuous generalizability and improvement, explaining its superior theorem-proving performance.

Published as a conference paper at ICLR 2025
LEANAGENT: LIFELONG LEARNING FOR FORMAL THEOREM PROVING
Adarsh Kumarappan" Mo Tiwari*: Peiyang Song', Robert Joseph George', Chaowei Xiao", Anima Anandkumar' Callifornia Institute of Technology. 2Stanford University, University of Wisconsin, Madison {adarsh, psong, rgeorge, anima) @caltech.edu, motiwari @ stanford.edu, cxiao34 2iia34@wiss.edu
ABSTRACT
Large Language Models (LLMs) have been successful in mathematical reasoning tasks such as formal theorem proving when integrated with interactive proof assis- tants like Lean. Existing approaches involve training fine-tuning LLM specific dataset to perform well on particular domains, such as undergraduate- mathematics. These methods struggle with generalizability matics. A fundamental limitation is that these approaches operate on static do- mains, failing capture how mathematicians often work across multiple domains and projects simultaneously or cyclically. We present LeanAgent, novel lifelong learning framework for formal theorem proving that continuously generalizes and improves on ever-expanding mathematical knowledge without forgetting pre- viously learned knowledge. LeanAgent introduces several key innovations, in- cluding curriculum learning strategy that optimizes the learning trajectory in terms of mathematical difficulty, dynamic database for efficient management evolving mathematical knowledge, and progressive training to balance stability and plasticity. LeanAgent successfully generates formal proofs for 155 theorems across 23 diverse Lean repositories where formal proofs were previously miss- ing, many from advanced mathematics. It performs significantly better than the static LLM baseline. proving challenging theorems in domains like abstract alge- bra and algebraic topology while showcasing clear progression of learning from basic concepts to advanced topics. In addition, analyze LeanAgent's superior performance on key lifelong learning metrics. LeanAgent achieves exceptional scores in stability and backward transfer, where learning new tasks improves per- formance previously learned tasks. This emphasizes LeanAgent's continuous generalizability and improvement, explaining its superior sesoorempproving perfor- mance.
advanced mathe-
INTRODUCTION
Mathematics can be expressed in informal and formal languages. Informal mathematics utilizes natural language and intuitive reasoming, whereas formal mathematies employs symbolic logic to construct machine-verifiale
proofs (Kevin Buzzard 2019). State-of-the-art large language models (LLMss, such ol (OpenAl 2024 and Claude (Claude Team 2024), produce incorrect informal proofs (Zhou et al.] 2024). This highlights the importance formal mathematics in ensuring proof correctness and reliability. Interactive theorem provers (ITPs), such Lean (De Moura al. (005)), have emerged as tools for formalizing and verifying mathematical proofs. However, constructing formal proofs using ITPs complex and conscmnnsmmin:: it requires extremely detailed proof steps and involves working with extensive mathematical libraries.
Recent research has explored using LLMs generate proof steps or complete proofs. For example, LeanDojo (Yang et al. 2023) introduced the first open-source framework to spur such research. Ex- isting approaches typically involve training or fine-tuning LLMSs on a specific dataset (Jiang al.) 2022). However, data scarcity in formal theorem proving (Polu al., (022) hinders the general- izability of these approaches (Liu et al. 2023). For example, ReProver, the retrieval- aaugmeellaugmeented
"Equal contribution.

---

Published as a conference paper at ICLR 2025
LLM from the LeanDojo family, uses retriever fine-tuned Lean's math library, math ib4 mathlibb Community, 2024p. Although mathlib4 contains over 100,000 formalized mathemat- ical theorems and definitions, it covers primarily up to undergraduate mathematics. Consequently, ReProver performs poorly on more challenging mathematics, such as Terence Tao's formalization of the Polynomial Freiman-Ruzsa (PFR) Conjecture (Taoo et al. 2024).
GitHHub Repositories
Extract Dana
LeanAgent
Dynamic Database
Per Repository
Uluoman prout theoren en proof
Curriculum Learnnng
Repeat For Each Repository
Corpus
Progressive Training
sorry Theorem Proving
Curriculum Leeming
Theorem Complexities
complexity: complexity:
Camplexity
it Proof Steps
Easy Medium Hard
Descending Theorems
Pragressive Training
Latest Retrievar
Limited Expasure
Belanced Treining
New
Retriever
spoch
Stabiiity
sorry Theorem Proving
Retrieved Premisses
w/ Updated Retriever
Cenersted Tactics
Beat-First Tree Search
sorry Theorems
New Proofs
LeanAgent overview. LeanAgent searches for Lean repositories and uses LeanDojo to extract theorems and proofs. uses curriculum learning, computing theorem complexity as e (S proof steps) and calculating the 33rd and 67th complexity percentiles across all theorems to sort repositories by easy theorem count. LeanAgent adds the curriculum to its dynamic database. As retrieval-based framework, LeanAgent generates dataset (premise corpus and collection of theorems and proofs) for each repository in the curriculum and progressively trains its retriever. Progressive training happens over one epoch prevent forgetting old knowledge. Then, LeanAgen uses the updated retriever in a seurch-based method to generate formal proofs for theorems where formal proofs were previously missing, known as sorry theorems. It adds new proofs to the database.
Figure 1:
The dynamic nature of mathematical research exacerbates this generalizability issue. Mathemati- cians often formalize across multiple domains and projects simultaneously or cyclically. For exam- ple, Terence Tao has worked various projects in parallel, including formalizations of the PFR Conjecture, symmetric mean of real numbers, classical Newton inequality, and asymptotic anal- ysis (Tao: 2024a| Tao al., 2024 Tao 2024b). Patrick Massot has been formalizing Scholze's condensed mathematics and the Perfectoid Spaces project (Community) 2024a b). These examples highlight a critical gap in current theorem-pre preorem-proving.oo AI approaches: the lack of a system that can adapt and improve across multiple, diverse mathematical domains over time, given limited Lean data availability.
Connection to Lifelong Learning, Crucially, how mathematicians formalize is relevant to lifelong leamiin, i.e. learning multiple tasks without forgetting (Wang al.) 2024b). A significant challenge is catastrophic forgetting: when adaptation to new distributions leads to loss of understanding of old ones (Jing et al. 2024). The core challenge is balancing plasticity (the ability to learn and adapt) with stability (the ability to retain existing knowledge) (Wang al. 2024b). Increasing plasticity to learn new tasks efficiently can lead to overwriting previously learned information. However, en- hancing stability preserve old knowledge may impair the model's 's ability acquire new skills (van) de Ven et al. 2024). Achieving the right balance is key to continuous generalizability theorem proving.
LeanAgent. We present LeanAgent, a novel lifelong learning framework for theorem proving. As shown in Figure LeanAgent's workflow consists of (1) deriving complexity measures of theorems
2

---

Published as a conference paper at ICLR 2025
to compute curriculum for learning, (2) progressive training to learn while balancing stability and plasticity, and (3) searching for proofs of sorry theorems by leveraging a best-first tree search, all while using a dynamic database to manage its evolving mathematical knowledge. LeanAgent works with any L.M;; we implement it with retrieval for improved generalizability (Yang et al. 2023).
We employ simple progressive training method to avoid catastrophic forgetting. Progressive train- ing allows LeanAgent to continuously adapt to new mathematical knowledge while preserving pre- viously learned information. This process involves incremenaally training the retriever on newly generated datasets from each repository in the curriculum. Starting with a pre-trained retriever (e.g., ReProver's retriever based on ByT5 (Xue et al. 2022)), LeanAgent trains on each new dataset for one additional epoch. Restricting progressive training to one epoch helps balance stability and plasticity. Crucially, this training is repeated for each dataset generated from the database, gradu- ally expanding LeanAgent's s knowledge base. This approach increases the space of possible proof states (where state consists of a theorem's hypotheses and current proof progress) while adding new premises to the premise embeddings. More sophisticated lifelong learning methods like Elastic Weight Consolidation (EWC) (Kirkpatrick et al. (017). which uses the Fisher Information Matrix to constrain important weights for previous tasks, result in excessive plasticity. The uncontrolled plas- ticity is due to the inability of these methods to adapt parameter importance as theorem complexity increases. This forces rapid changes in parameters crucial for learning advanced concepts. Such methods fail to adapt to the evolving complexity of mathematical theorems, making them unsuitable for lifelong learning in theorem proving.
Extensive experiments across 23 diverse Lean repositories demonstrate LeanAgent's advancements in lifelong learning for theorem proving. LeanAgent successfully generates formal proofs for 155 theorems across these 23 repositories where formal proofs were previously missing, known as sorry theorems, many from advanced mathematics. For example, it proves challenging sorry theorems in abstract algebra and algebraic topology related to Coxeter systems and the Hairy Ball Theorem (Coxeter 2024] Hairy Ball Theorem. 2024). LeanAgent also proves theorems using exploits found within Lean's 's type system. We find that LeanAgent demonstrates progressive learning in theorem proving, initially proving basic sorry theorems and significantly advancing to more complex ones. It significantly outperforms the static ReProver baseline in terms of proving new sorry theorems. We have issued pull requests to the respective repositories with the newly proven sorry theorems. Some of these proofs utilized unintended constructs within the repositories' implementations, which are currently being addressed through appropriate fixes.
In theorem proving, we find that stability, without losing too much plasticity, is crucial for tinuous generalizability to new repositories. Backward transfer (BWT), where learning new tasks improves performance previously learned tasks, is essential in theorem proving (Wang et al., 2024b). Mathematicians require a lifelong learning framework for theorem proving that is both continuously generalizable and continuously improving. We conduct an extensive ablation study using six lifelong metrics carefully proposed or selected from the literature. LeanAgent's 's simple components of curriculum learning and progressive training improve stability and BWT scores sub- stantially, emphasizing its continuous generalizability and improvement and explaining its superior sorry theorem proving performance.
PRELIMINARIES
Neural Theorem Proving. The current state-of-the-arr of learning-based provers employs Transformer-ban based Vaswani et al. 2017) LLMs that process expressions as plain text strings (Azer- bayev et al.] 2024 Xin et al., 2024b) [haa et al. 2024). In addition, researchers have explored complementary aspects like proof search algorithms (Lample et al., Wang al. 2023). Moreover, other works break the theorem- prrooin--rovingggg process into smaller proving tasks (Song et al. 2024 Wang
et al.
2024a
Lin et al. 2024).
Premise Selection. A critical challenge in theorem proving is the effective selection of relevant
premises [rrvng et al. 2016: Tworkowski et al.). However, many existing approaches treat premise
selection as an isolated problem (Wang & Deng 2020 Piotrowski et al. 2023) or use selected
premises only input symbolic provers (Alama et al. 2014 Mikula et al. 2024
3

---

Published as a conference paper at ICLR 2025
Eetrieval-Augmentte LLMs. While augmented language models have been extensively studied in areas like code generation (Lu et al., 2022 Zhou et al. 2023), their application to formal theorem proving is relatively
However, relevant architectures have been researched in natural
language processing (NIP)
(Lu et
2024 Borgeaud et al. 2022 Thakur et al. 2024).
Lifelong Learning. Lifelong learning addresses catastrophic forgetring in sequential task learning
Chen et al. 2024). Approaches include regularization methods [Kirkpatrick et al. (017]. memory-
based techniques Lopez-Paz & Ranzato 2017 Chaudhry al. 2019 Shin al. (017). and knowl- edge distillation (Li & Hoiem] 2017: Kim el al. 2023). Other strategies involve dynamic architec-
ture adjustment (Mendez Eaton
2021 and recent work on gradient manipulation and selective
re re-initialization Chen et al.
2024
Dohare et al. 2024). We justify not using these strategies in
Appendix A.6
Curriculum Learning in Theorem Proving. Prior work created a synthetic inequality generator to produce curriculum statements of increasing difficulty (Polu et al. (022). For reinforcement learning, existing work used the length of proofs to help determine rewards (Zombori et al.) 2019).
3 METHODOLOGY
A useful lifelong learning strategy for theorem proving requires (a) repository order strategy and (b) a learning strategy. We solve (a) with curriculum learning to utilize the structure of Lean proofs and (b) with progressive training to balance stability and plasticity. LeanAgent consists of four main components: curriculum learning, dynamic database management, progressive training of the retriever, and sorry theorem proving. Further methodology details are in [Appendix A.I and dis- cussion of why curriculum learning works in theorem proving is available in in/Apendix A.6
3.1 CURRICULUM LEARNING
LeanAgent uses curriculum learning to learn on increasingly complex mathematical repositories. This process optimizes LeanAgent's learning trajectory, allowing it build upon foundational knowledge before tackling more advanced concepts.
First, we automatically search for and clone Lean repositories from GitHub. We use LeanDojo for each repository to extract fine-gra -ne-grained information about their theorems, proofs, and dependencies. Then, we calculate the complexity of each theorem using e where S represents the number proof steps. However, sorry theorems, which have no proofs, are assigned infinite complexity. We use an exponential scaling to address the combinatorial explosion of possible proof paths as the length of the proof increases. Further justification for considering this complexity metric is in Appendixx A.6
We compute the 33rd and 67th percentiles of complexity across all theorems in all repositories. Using these percentiles, categorize non-sorry theorems into three groups: easy (theorems with complexity below the 33rd percentile), medium (theorems with complexity between the 33rd and 67th percentiles), and hard (theorems with complexity above the 67th percentile). We then sort repositories by the number of easy theorems they contain. This sorting forms the basis of our curriculum, with LeanAgent starting on repositories with the highest number of easy theorems.
3.2 DYNAMIC DATABASE MANAGEMENT
Then, we add the sorted repositories to LeanAgent's custom dynamic database using the data Lean- Agent extracted. This way, we can keep track of and interact with the knowledge that LeanAgent is aware of and the proofs has produced. We also include the complexity of each theorem computed in the previous step into the dynamic database, allowing for efficient reuse of repositories in future curriculum. Details of the database's contents and features can be found in Appendixx A.I
For each repository in the curriculum, LeanAgent uses the dynamic database to generate dataset by following the same procedure used to make LeanDojo Benchmark (details in Appendix A.I) This dataset includes collection of theorems and their proofs. Each step of these proofs contains detailed annotations, such as how the step changes the state of the proof. A state consists a theorem's hypotheses and the current progress in proving the theorem. As such, this pairing of
4

---

Published as a conference paper at ICLR 2025
theorems and proofs demonstrates how to specific tacties (functions) and premises in sequence to prove a theorem. In addition, the dataset includes a premise corpus, serving as a library of facts and definitions.
3.3 PROGRESSIVE TRAINING OF THE RETRIEVER
LeanAgent then progressively trains its retriever on the newly generated dataset. This strategy al- lows LeanAgent to continuously adapt to new mathematical knowledge from the premises in new datasets while preserving previously learned information, crucial for lifelong learning in theorem proving. Progressive training achieves this by incrementally incorporating new knowledge from each repository.
Although LeanAgent works with any LLM, we provide specific implementation here. We start with ReProver's retriever, a fine-tuned version of the ByT3 encoder (Xue et al. 2022), leveraging its general pre-trained knowledge from mathl 144. We train LeanAgent the dataset for additional epoch. This limited exposure helps prevent overfitting to the new data while allowing LeanAgent to learn essential new information. LeanAgent's retriever, and therefore the embeddings it generates, are continuously updated during progressive training. Thus, at the end of the current progressive training run, we precompute embeddings for all premises the corpus generated by LeanAgent's current state to ensure that we properly evaluate LeanAgent's 's validation performance. To understand how LeanAgent balances stability and plasticity, we save the model iteration with the highest validation recall for the top ten retrieved premises (R @ 10). This is a raw plasticity value: it can be used to compute other metrics that describe LeanAgent's ability to adapt to and handle new types of mathematics in the latest repository (details in Sec. 4). Then, compute the average test R@ 10 over all previous datasets the model has progressively trained on, a raw stability value.
As mentioned previously, we repeat this procedure for each dataset we generate from the database, hence the progressive nature of this training. Progressive training adds new premises to the premise embeddings and increases the space of possible proof states. This allows LeanAgent explore more diverse paths to prove theorems, discovering new proofs that couldn't produce with its original knowledge base
3.4 sorry THEOREM PROVING
For each sorry theorem, LeanAgent generates a proof with a best-first tree search by generating tactic candidates each step, in line with prior work (Yang et al., 2023). Using the embeddings from the entire corpus of premises we previously collected, LeanAgent retrieves relevant premises from the premise corpus based on their similarity to the current proof state, represented embedding. Then, it filters the results using a corpus dependency graph to ensure that we only consider premises accessible from the current file. We add these retrieved premises to the current state and generate tactic candidates using beam search. Then, we run each tactic candidate through Lean to obtain potential next states. Each successful tactic application adds a new edge the proof search tree. We choose the tactic with the maximum cumulative log probability of the tactics leading it. If the search reaches a dead-end, we backtrack and explore alternative paths. We repeat the above steps until the search finds a proof, exhausts all possibilities, or reaches the time limit of 10 minutes.
context
If LeanAgent finds proof, it adds it to the dynamic database. The newly added premises from this proof will included future premise corpus involving the current repository. Moreover, LeanAgent can learn from the new proof during progressive training in the future, aiding further improvements.
4 EXPERIMENTS
4.1 EXPERIMENTAL SETUP
We devote this section to describing two types of experiments: (1) sorry Theorem Proving: We compare sorry theorem proving performance between LeanAgent and ReProver. We also examine the progression of LeanAgent's proven sorry theorems during lifelong learning the end of life-
5

---

Published as a conference paper at ICLR 2025
Table Selected repository descriptions
Repository
Description
PFR
Polynomial Freiman-Ruzsa Conjecture
Hairy Ball Theorem
Algebraic topology result
Coxeter
Coxeter groups
Mathematics in Lean Source
Lean files for the texthook
Formal Book
Proofs from THE BOOK
MiniF2F
Math olympiad-style problem solving
SciLean
Scientific computing
Carleson
Carleson's 's Theorem
Lean4 PDL
Propositional Dynamic Logic
Table 2: Accuracy in proving sorry theorems across repositories. Accuracy is calculated as (proven theorems / total sorry theorems). "LA" denotes LeanAgent and "ReProver+" denotes the setting where we update ReProver on all 23 repositories at once. "During" shows accuracy during lifelong learning, "Add. After" shows additional accuracy after lifelong learning, and "Total" shows the combined accuracy. "MIL" stands for Mathematics in Lean Source and "Hairy Ball" refers to the Hairy Ball Theorem repository. Repositories with no sorry theorems or no proven ones are not shown. The best accuracy for each repository is in bold. As noted previously, we progressively train on MiniF2F after the initial curriculum to demonstrate the use case formalizing in a new repository after learning curriculum. As such, we don't It evaluate LeanAgent after lifelong learning on MiniF2F.
Repository
#sorrys
LA Accuracy (%)
ReProver Accuracy ( (%)
ReProver+
Total
During
Add. After
Accuracy (%
MIL
29
72.4
48.3
24.1
48.3
55.2
MiniF2F
406
24.4
24.4
20.9
20.9
Formal Book
29
10.3
6.9
3.4
6.9
10.3
SciLean
294
9.2
7.5
1.7
8.2
8.5
Hairy Ball
14
7.1
0.0
7.1
0,0
7.1
Coxeter
15
6.7
6.7
0.0
0.0
6.7
Carleson
24
4,2
4.2
0.0
4.2
4.2
Lean4 PDL
30
3.3
3.3
0.0
3.3
3.3
PER
37
2.7
2.7
0.0
0.0
0.0
long learning. This shows LeanAgent's continuous generalizability and improvement, (2) Lifelong Learning Analysis: We conduct an ablation study with lifelong learning metrics to explain Lean- Agent's superiority in sorry theorem proving. Morcover, these results explain LeanAgent's superior handling of the stability tradeoff. Please see Appendix A.2 for experiment implementation details. We release LeanAgent
Repositories. We evaluate our approach on a diverse set of 23 Lean repositories to assess its gener-
alizability across different mathematical domains (Skrivan 2024
Kontorovich 2024| Avigad
2024
Tao et al. 2024 |Rnnhaww 2024; |Fermat's 's Last Theorem 2024
DeepMind [202]]
[ Carneiro
2024
Wieser 2024
Mizuno, 2024 Murphy 2024 Formal Logic 2024 Con-nf) 2024 Gadgil 2024
Yang, 2024 Zeta 3 Irrational 2024 Firsehing. Moritz, 2024 Monnerjahn [2024] van Doorn 2024
Dillies 2024 Hairy Ball Theorem, 2024] Coxeter CoxetCr 2024 Gattinger] 2024). Details of key reposito-
ries are in Table I] Further details of these repositories, including commits and how we chose the
initial curriculum and the nub-curriculum (described in Sec. 4.2p, are in Appeediix A.3
4.2 sorry THEOREM PROVING
We compare the number of sorry theorems LeanAgent prove, both during and after lifelong learning, to the ReProver baseline. We use ReProver as the baseline because we use its retriever as LeanAgent's 's initial retriever in experiments.
In addition, a use case of LeanAgent is proving new repository after learning a curriculum; progressively train MiniF2F to demonstrate this. Note that choose the Lean4 version

---

Published as a conference paper at ICLR 2025
MiniF2F
PFR
theoren Drluction_12dvdHexeee 4*(n-1) by
Rl swnoRhooof_ttanstaer transtateee (A 5 Typex) IMeasureSpace (Y
Lerna condRho_od
Finset (s:G)
noгi
condRho (fun
condRho by
induction" with hn simp onego
simp only [condKha, the translate)
SciLean
theoren amc12a_28022_6 (n : N)
theoren re_. flont (a Flost) exact SeLixe.re_eo_seML..o le_rfl
by
(he 0 < n)]
(n
lift cases' n with
using
Coxeter
exact (.. LE add of BOS right
Lema invmap.ot_co (S:Set G) ICoxeterSysten S] invmap s by
simp)
simp [oxxteeSystenn.ee wwweeesyyytten.eeeeeeee Presentation invirgg]
Formal Book
unfold CuxeterSys ten, toffa
apply CoxeterSys wwwpssyyteee.nnoooo. wtt..
theoren wedderburn Pintype R): IsField
:= by
apply Fietd. toIsField
Figure 2: Case studies of LeanAgent's new proofs. LeanAgent shows an ability work with these repositories, often able to retrieve the necessary premises (highlighted). For example, LeanAgent proves sorry theorem from PFR, condRho.of.trans. showing its proving ability on the PFR repository. In addition, LeanAgent could prove re se_float from SciLean during lifelong learning, while ReProver could not. Moreover, its MiniF2F proofs demonstrate its ability to generate relatively longer and more complex proofs for complex mathe- matics. LeanAgent's proof of invmap. ___eq and wedderbourn represents theorem proving capabilities with abstract algebra premises.
by simply expanding definitions,
of the Mi repository (Yang 2024) and disregard its separation into validation and test splits (reasoning in Appendix A.5) LeanAgent's success rate on the Lean4 version of the MiniF2F test Morcover, a mathematician could use LeanAgent for (1) an initial curriculum A, and later (2) sub-curriclum B. LeanAgent can then help the mathematician prove the repositories curriculum A + B. To demonstrate this scenario, we continue LeanAgent on a sub-curriculum B of repositories.
set is also in Appendix A.5
Results are in Table 2] with case studies in Figure 2 Appendix A.5 provides a more thorough discussion, including ablation study, and contains the complete theorems and proofs relevant to this section.
LeanAgent demonstrates continuous generalizability and improvement in theorem-proving capabil- ities across multiple repositories. LeanAgent's 's proofs are a superset of the sorry theorems proved by ReProver most cases. Moreover, isolate the effect of curriculum learning, we compare LeanA- gent against ReProver+, the ReProver model updated on all 23 repositories at once, and notice that LeanAgent outperforms it on several repositories, emphasizing the importance of curriculum learn- ing. Overall, LeanAgent progresses from basic concepts (arithmetic, simple algebra) to advanced topics (abstract algebra, topology).
PFR. LeanAgent can prove sorry theorem from this repository, while ReProver cannot. It also generalizes to different commit (not included in progressive training), uncovering system ex- ploits. LeanAgent proves two theorems with just the rfl tactic, one of which ReProver cannot, and proves sorry theorems with a 0 = 1 placeholder theorem statement.
SciLean. During lifelong learning, LeanAgent proves theorems related to fundamental algebraic structures, linear and affine maps, and measure theory basics. By the end of lifelong learning, proves concepts in advanced function spaces, sophisticated bijections, and abstract algebraic struc- tures.
Mathematics in Lean Source. During lifelong learning, LeanAgent proves theorems about basic algebraic structures and fundamental arithmetic properties. By the end lifelong learning, it proves more complex theorems involving quantifier manipulation, set theory, and relations.
MiniF2F. ReProver demonstrates proficiency in basic arithmetic, elementary algebra, and simple calculus. However, by the end of lifelong learning, LeanAgent handles theorems with advanced

---

Published as a conference paper at ICLR 2025
number theory, sophisticated algebra, complex calculus and analysis, abstract algebra, and complex induction.
Sub-curriculum. In the Formal Book repository, LeanAgent progresses from proving basic real analysis and number theory theorems to more advanced abstract algebra, exemplified by its proof of Wedderbum's Little Theorem. For the Coxeter repository, LeanAgent proves a complex lemma about Coxeter systems, showcasing its increased understanding of group theory. the Hairy Ball Theorem repository. LeanAgent proves a key step of the theorem, demonstrating improved perfor- mance in algebraic topology. Only LeanAgent can prove these theorems, demonstrating that it has much more advanced scoorempprvingg capabilities than ReProver.
4.3 LIFELONG LEARNING ANALYSIS
To our knowledge, other lifelong learning frameworks for theorem proving exist in the literature. As such, we conduct an ablation study with six lifelong learning metrics to showcase Leantgent's superior handling of the stability-plastiitty tradeoff. These results help explain LeanAgent's superi- ority in sorry theorem proving performance. We compute these metrics for the original curriculum of 14 repositories.
Specifically, the ablation study consists of seven additional setups constructed from combination of learning and dataset options. Options for learning setups are progressive training with or without EWC. Dataset setups involve dataset order and construction. Options for dataset orders involve Single Repository Merge All, where each dataset consists of all previous repositories and the new one. Given the most popular repositories on GitHub by star count, options for dataset construc- tion include popularity order or curriculum order. Appendix shows these orders and additional repository details.
Metrics. We use six lifelong learning metrics: Windowed-Forgetting (WF5), Forgetting Mea- sure (FM), Catastrophic Forgetting Resilience (CFR), Expanded Backward Transfer (EBWT), Windowed- Windowed-Pllsticity Plasticity (WP5), and Incremental Plasticity (IP). A description of these metrics is in Table 3 (De Lange et al., 2023 Wang al. 2024b Diaz-Rodrigue et al. 2018). Our reasoning for considering these metrics detailed in Appendix A.4
Table 3: Description of lifelong learning metries.
Metric
Description
Target
Type
WF5
Measures forgetting over 5-task window
Lower
Existing
FM
Average performance drop old tasks
Lower
Existing
CFR
Ratio of min to max average test R@ 10
Higher
Proposed
EBWT
Average improvement on old tasks after learning new ones
Higher
Existing
WP5
Max average test R @ 10 increase over a 5-task window
Higher
Existing
IP
Rate of validation @ 10 change per task
Higher
Proposed
We describe why we introduce two new metrics to address specific aspects of lifelong learning in theorem proving:
Catastrophic Forgetting Resilience (CFR), This metric captures LeanAgent's ability to maintain performance on its weakest task relative to its best performance, crucial in the presence of diverse mathematical domains.
Incremental Plasticity (IP). IP provides a more granular view of plasticity than aggregate mea- sures and is sensitive to the order of tasks, particularly relevant in lifelong learning for theorem proving.
In addition, these metrics the Merge All strategy measure cumulative knowledge refinement rather than isolated task performance (details in Appendix A.4). Due to these interpretational differences, we analyze Single Repository and Merge All setups separately. We consider an improvement of at least 3% be significant.
Single Repository Analysis. We first analyze the Single Repository results from Table 4 LeanA-
gent demonstrates superior stability across multiple metrics. The WF5 metric is 75.34% lower for
8

---

Published as a conference paper at ICLR 2025
Table Comparison of lifelong learning metrics across setups. The best scores for each metric are in bold.
Single Repository
Merge All
Metric
LeanAgent
Setup
Setup 2
Setup 3
Setup 4
Setup 5
Setup
Setup 7
WF5 (1)
0.18
7.60
7.17
0.73
15.83
2.23
13.34
5.82
FM (L)
0.85
6,53
4.04
2.11
10.50
4.06
11.44
3.80
CFR ())
0.88
0.87
0.88
0.85
0.76
0.94
0.75
0.90
EBWT (T)
1.21
0.51
1.04
0.76
-0.20
0.73
-1.34
-0.39
WP5 (t)
2.47
0.89
1.47
3,42
0.00
0.09
0.00
0.11
(P)
1.02
0.36
0.26
1.06
-1.50
-0.64
-1.71
-0.89
Legend
Single Repository:
Merge All:
Setup 1: No EWC, Popularity Order
Setup 4: No EWC, Popularity Order
Setup 2: EWC, Popularity Order
Setup 5: No EWC, Curriculum Learning
Sctup 3: EWC, Curriculum Learning
Setup 6: EWC, Popularity Order
Setup 7: EWC, Curriculum Learning
LeanAgent than the next best setup, suggesting it maintains performance over window more effee- tively. Its FM score is 59.97% lower than Setup 3's, showcasing its resilience against catastrophic forgetting. Furthermore, LeanAgent, Setup 1, and Setup 2 demonstrate high and consistent resilience against catastrophic forgetting, with CFR values above 0.87 and minimal (+0.01) differences. This underscores LeanAgent' ability to continuously generalize over time. In addition, LeanAgent has 16.25% higher EBWT, indicating its ability to continuously improve over time.
In contrast, Setup 3 exhibits characteristics of higher plasticity. It shows 38.26% higher WP5 over LeanAgent, indicating greater ability to rapidly adapt to new tasks in window. This is complemented by 3.98% higher IP over LeanAgent, suggesting more pronounced improvement on new tasks over time. However, these plasticity gains come at significant cost: Setup 3 suffers from more severe catastrophic forgetting, as evidenced by its significantly worse stability metrics compared to LeanAgent. This excessive plasticity in Setup 3 stems from EWC's inability to adapt parameter importance as theorem complexity increases. EWC preserves parameters important for simpler theorems, which may not be crucial for more complex ones. Consequently, these preserved parameters resist change while other parameters change rapidly for complex theorems. This forces the model to become more plastic overall, relying heavily on non- non-preserved parameters for new, complex theorems.
LeanAgent's favorable stability and EBWT scores make it the most suitable for lifelong learning in the Single Repository setting.
Merge All Analysis. Next, analyze the Merge All setups from Table 4 Setup 5's WF5 metric is 61.68% lower than the next best setup (Setup 7), suggesting Setup 5 balances and retains knowledge expanding dataset most effectively. Furthermore, Setup 5's CFR score is 3.77% higher than that of Setup 7, again demonstrating high and consistent resilience in the face of an expanding, potentially more complex dataset. However, Setup has 6.44% lower FM score than Setup 5's, showcasing its ability to maintain performance on earlier data points. Moreover, Setup 5 is the only setup with positive EBWT, indicating that learning new tasks improves performance on the entire historical dataset. The other setups have negative EBWT, indicating performance degradation on earlier tasks after learning new ones.
Only Setups 5 and 7 have non-zero WP5, suggesting the ability to adapt to the growing complexity of the combined dataset. The zero values for Setups 4 and 6 indicate that popularity order struggles to show improvement when dealing with merged data. However, although Setup has the highest IP score with a 27.75% improvement over Setup 7, all 4 setups have negative values. This indicates a decrease in validation @@ 10 over time, suggesting that the Merge All strategy struggles to maintain performance.
Experiment 5's favorable stability and EBWT scores suggest it is the best at balancing the retention of earlier knowledge with the adaptation to new data in a combined dataset. However, its negative IP value indicates fundamental issue with its approach.

---

Published as a conference paper at ICLR 2025
Comparative Analysis and Insights. Although the metrics have different interpretations in the Sin- gle Repository and Merge All settings, we can still draw some meaningful comparisons by focusing on overall trends and relative performance. We must consider that the negative IP values in Merge All setups indicate a significant issue. This drawback outweighs the potential benefits seen in other metrics like WP5, it indicates fundamental inability maintain and improve performance in a continuously growing dataset. In contrast, LeanAgent demonstrates a positive IP, indicating its ability incorporate new knowledge. This, combined with its superior stability and EBWT metrics relative to other Single Repository methods, suggests that LeanAgent is better suited than Setup 5 for continuous generalizability and improvement.
Consistency with sorry Theorem Proving Performance. This lifelong learning analysis is con- sistent with LeanAgent's sorry theorem proving performance. I LeanAgent's superior stability met- rics (WF5, FM, and CFR) explain its ability to maintain performance across diverse mathematical domains, as evidenced by its success in proving theorems from various repositories like SciL Mathematics in Lean Source, and PFR. Its high EBWT score aligns with its progression from basic concepts to advanced topics in theorem proving. While LeanAgent shows slightly lower plasticity (WP5 and IP) compared to some setups. this trade-off results in better overall performance, flected in its ability to prove a superset of sorry theorems compared to ReProver in most cases. This analysis demonstrates LeanAgent's overall superiority in lifelong learning for theorem proving.
CONCLUSION
We have presented LeanAgent, a lifelong learning framework for theorem proving that achieves continuous generalizability and improvement across diverse mathematical domains. Key compo- nents include a curriculum learning strategy, progressive training approach, and custom dynamic database infrastructure. LeanAgent successfully generates formal proofs for 155 theorems where formal proofs were previously missing and uncovers 7 exploits across 23 Lean repositories, includ- ing from challenging mathematics. This highlights its potential to assist in formalizing complex proofs across multiple domains and identifying system exploits. For example, LeanAgent success- fully proves challenging theorems abstract algebra and algebraic topology. ReProver baseline in proving new sorry theorems, progressively learning from basic to complex mathematical concepts. Moreover, LeanAgent shows significant performance in forgetting measures and backward transfer, explaining its continuous generalizability and continuous improvement.
outperforms the
Future work could explore integration with Lean Copilot, providing real-time assistance with math- ematician's repositories. In addition, a limitation of LeanAgent is its inability to prove certain theo- rems due to a lack of data on specific topics, such as odeSolve arg X semiAd rule in LeiLLen about ODEs. To solve this problem, future work could use reinforcement learning for synthetic data generation during curriculum construction. Moreover, future work could use LeanA- gent with additional math LLMs and search strategies.
ACKNOWLEDGMENTT
Adarsh Kumarappan supported by the Summer Undergraduate Research Fellowships (SURF) pro- gram at Caltech. Anima Anandkumar is supported by the Bren named chair professorship, Schmidt AI 2050 senior fellowship, and ONR (MURI grant N00014-18-12624) We thank Terence Tao for detailed discussions and feedback that significantly improved this paper. We thank Zulip chat mem- bers for engaging in clarifying conversations that were incorporated into the paper.
REFERENCES
Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivisivadze, and Josef Urban. Premise Selec- tion for Mathematics by Corpus Analysis and Kernel Methods. Journal of Automated Reasoning, 12(2)1191-213, February 2014. ISSN 0168-7433, 1573-0670. doi: (0.10077s108117003-99
Andrew Arana and Will Stafford. On the difficulty of discovering mathematical proofs. Synthese, 202(2):1-29, 2023. doi: 10.10077/11222--022-411833
Jeremy Avigad, Avigad/mathematics in lean source, August 2024.
10

---

Published as a conference paper at ICLR 2025
Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Al- bert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An Open Language Model For Mathematics, March 2024.
Yoshua Bengio, Jérôme Louradour, Ronan Collobert, and Jason Weston. Curriculum learning. In Proceedings of the 26th Annual International Conference on Machine Learning, pp. 41-48, Montreal Quebec Canada, June 2009, ACM. ISBN 978-1-60558-511 doi: 10.1145/1553374. 1553380.
Sebastian Borgeaud, Arthur Mensch, Jordan Hoffmann, Trevor Cai, Eliza Rutherford, Katie Mil- lican, George van den Driessche, Sean-Baptiste Lespiau, Bogdan Damoc, Aidan Clark, Diego de Las Casas, Aurelia Guy, Jacob Menick, Roman Ring, Tom Hennigan, Saffron Huang, Loren Maggiore, Chris Jones, Albin Cassirer, Andy Brock, Michela Paganini, Geoffrey Irving, Oriol Vinyals, Simon Osindero, Karen Simonyan, Jack W. Rac, Erich Elsen, and Laurent Sifre. Im- proving language models by retrieving from trillions tokens, February 2022.
Mario Carneiro. Digama0/lean4lean, September 2024.
Ernie Chang, Hui-Syuan Yeh, and Vera Demberg. Does the Order of Training Samples Matter? Im- proving Neural Data-to-Texs Text Generation with Curriculum Learning. In Paola Merlo, Jorg Tiede-
mann, and Reut Tsarfaty (eds.), Proceedings of the 16th Conference of the European Chapter of the Association for Computational Linguistics; Main Volume, pp. 727-733, Online, April 2021. Association for Computational Linguistics. doi: 10.18653/v1/022 wttp:///2221eelemmaaaaaaaa eacl-main.61.
Arslan Chaudhry, Marc' Aurelio Ranzato, Marcus Rohrbach, and Mohamed Elhoseiny, Efficient Lifelong Learning with A- A-GEM, January 2019.
Jiefeng Chen, Timothy Nguyen, Dilan Gorur, and Arslan Chaudhry. Is forgetting less good induc- tive bias for forward transfer?, March 2023.
Yupeng Chen, Senmiao Wang, Zhihang Lin, Zeyu Qin, Yushun Zhang, Tian Ding, and Ruoyu Sun. MoFO: Momentum-Filtered Optimizer for Mitigating Forgetting in LLM Fine- Sine-Tuning. 2024. doi: 10.4850/ARXX1.2407.0099
Volkan Cirik, Eduard Hovy, and Louis- Philsppil Morency. Visualizing and Understanding Curricu- lum Learning for Long Short- Term Memory Networks, November 2016.
Claude Team. Introducing claude 3.5 sonnet, June 2024. URL http:::://www.aaahrpp.....
com/ ccom///eerr/cladde--------oeee
Lean Community. Lemprover-communt//ccr-iiiiiii htw.:://iie..eeeooo.ooooooooooeo September 2024a.
Lean Community. Leupooercommmmiyyy/carrrrroooooo leanprover-communig wtt.:/acccccpp.p....eeeeooooommo August
2024b.
Con-nf. Leapprver-oommuniyy/on..tt formal consistency proof of Quine's set theory New Foundations. htwp:///hhiiooommaaareecooooooet 2024.
Coxeter. NUSSMMath-Formnlizzttoooooooos at htt.s//ees.........oooeoooooooos
2024. http:///...ooooooommmmm/mm/tttte
Matthias De Lange. Gido van de Ven, and Tinne Tuytelaars. Continual evaluation for lifelong
learning: Identifying the stability gap, March 2023.
Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob Von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp (eds.), Au- tomated Deduction CADE-25, volume 9195, pp. 378-388, Cham, 2015. Springer International doi: 10. 00.1007/978-3-31--24440
Publishing. ISBN 978-3-3199211400-9 908
Google DeepMind. Google-deepmin//debattt Google DeepMind, August 2024.
Natalia Diaz-Rodríguez, Vincenzo Lomonaco, David Filliat, and Davide Maltoni. Don't forget, there is more than forgetting: New metrics for Continual Learning, October 2018.

---

Published as a conference paper at ICLR 2025
Yael Dillies. YuclDillies/LeemAAPP. September 2024.
Shibhansh Dohare, Fernando Hernandez- Garcia, Qingfeng Lan, Parash Rahman, A. Rupam Mah- mood, and Richard S. Sutton. Loss of plasticity in deep continual learning. Nature, 632(8026): 768-774, August 2024. ISSN 0028-0836, 1476-4687. doi: 10. (003664418-002-07777111
Fermat's Last Theorem. ImperialCColegeeLnnddooff Imperial College London, September 2024.
Firsching, Moritz. Mo271/FormalBook: Formalizing "Proofs from THE BOOK", 2024.
Formalized Formal Logic. commaliredoormalllogiccfooooddd FormalizedFFrmallloggi Septem- ber 2024.
Siddhartha Gadgil. Siddiartna-gadgiiSSaumn Experiments with SAT solvers with proof's in Lean 4. 2024.
Malvin Gattinger. M4lvin/lean4-pdl, September 2024.
Septembeerr
Hairy Ball Theorem.
Corent I http://aaiiiy-aalllhhhheereeee http:///ggiuuub.ooooooeeettt 2234/mar1///2/////e hhtprrrteeeeeeeee7//dd////ee/eee
at
2024.
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Een, Francois Chollet, and Josef Urban. Deep.att Deep Sequence Models for Premise Selection. Advances in Neural Infor- mation Processing Systems, volume 29, Curran Associates, Inc., 2016.
Albert Q Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóždž, Piotr Miloš, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. 2022. doi: (0.4855//ARXIV.2255..0
Gangwei Jiang, Caigao Jiang, Zhaoyi Li, Siqiao Xue, Jun Zhou, Lingi Song, Defu Lian, and Ying Wei. Interpretable Catastrophic Forgetting of Large Language Model Fine-tuning via Instruction Vector. 2024. doi: 10.48550/ARXIV.244 12227.
Kevin Buzzard. The Future of Mathematics? Professor Kevin Buzzard 30 May 2019, June 2019.
Seungyeon Kim, Ankit Singh Rawat, Manzil Zaheer, Sadeep Jayasumana, Veeranjaneyulu Sad- hanala, Wittawat Jitkrittum, Aditya Krishna Menon, Rob Fergus, and Sanjiv Kumar. EmbedDis- till: A Geometric Knowledge Distillation for Information Retrieval. 2023. doi: 10.48550/ARXIV. 2301.
James Kirkpatrick, Razvan Pascanu, Neil Rabinowitz, Joel Veness, Guillaume Desjardins, Andrei A. Rusu, Kieran Milan, John Quan, Tiago Ramalho, Agnieszka abis, Claudia Clopath, Dharshan Kumaran, and Raia Hadsell. Overcoming catastrophic forgetting in neural networks. Proceedings of the National Academy of Sciences, (14(13):3521-33 -3526, March 2017. ISSN 0027-8424, (091-6490. doi: 10.1003/pnas. 161 1835114.
Demis Hass-
Alex Kontorovich. AlcKKmntorochhPPiineNnnnnbTTTTTe Thw.remmnddd....ndn...... August 2024.
Guillaume Lample, Marie-Anne Lachaux. Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. HyperTree Proof Search for Neural Theorem Proving.
Conglong Li. Zhewei Yao, Xiaoxia Wu, Minjia Zhang, Connor Holmes, Cheng Li, and Yuxiong He. DeepSpeed Data Efficiency: Improving Deep Learning Model Quality and Training Efficiency via Efficient Data Sampling and Routing. Proceedings of the AAAI Conference on Artificial Intelligence, 38(16):18490-1848 18490-18498. March 2024. ISSN 2364-3468. 2159-5399. doi: 10.1609/ aaai.v38116.29810
Zhizhong Li and Derek Hoiem. Learning without Forgetting, February 2017.
Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-STaR: Learning to Interleave Thinking and Proving, August 2024.
12

---

Published as a conference paper at ICLR 2025
Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, and Qun Liu. FIMO: Challenge For- mal Dataset for Automated Theorem Proving, December 2023.
David Lopez-Paz and Marc' Aurelio Ranzato. Gradient Episodic Memory for Continual Learning. In Advances in Neural Information Processing Systems, volume 30. Curran Associates, Inc., 2017.
I. Loshchilov and F. Hutter. Decoupled Weight Decay Regularization. In International Conference on Learning Representations, November 2017.
Minghai Lu, Benjamin Delaware, and Tianyi Zhang. Proof Automation with Large Language Mod- cls, September 2024.
Shuai Lu. Nan Duan, Hojae Han, Daya Guo, Seung-won Hwang, and Alexey Svyatkovskiy, ReACC: A Detrieval-Augmennt Code Completion Framework. In Smaranda Muresan, Preslav Nakov, and Aline Villavicencio (eds.), Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume I: Long Papers), pp. Association for Computational Linguistics. doi: 10.18653/1/22222.aal4/o
Dublin, Ireland, May 2022.
The mathlib4 Community. Leappove--ommmiityyaablbb leanprover-community September 2024.
Jorge A Mendez and Eric Eaton. Lifelong Learning of Compositional Structures. 2021.
Maciej Mikula, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Lukasz Kuciński. Piotr Milos, and Yuhuai Wu. Magnusham- mer: A Transformer-Baut Approach to Premise Selection, March 2024.
Yuma Mizuno. Yuma- hama--mzzuoollan-maaan worth-oorkhhop. https//github.com/yumas www.:/omommymmammiuiiimuullolaaa mww.no//eaannnaeaeeeee maath workshop, 2024.
Ludwig Monnerjahn. wuu.gl/.Cccc/mmmmmaaoooooooooooa September 2024.
Logan Murphy. LeganiinurphyyLeenEuuidd September 2024.
OpenAI. OpenAl ol System Card, September 2024.
Bartosz Piotrowski, Ramon Fernández Mir, and Edward Ayers. Machine- Premise Selec- tion for Lean. In Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings, pp. 175-186, Berlin, Heidelberg, September 2023. Springer-Verlag. ISBN 978-3- 031-43512-6. doi: 111100/97788--3--3351-33
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and
I. Sutskever. Formal Mathematics Statement Curriculum Learning ArXiv, February 2022.
David Renshaw. Dwrenssha/comptties: Catalog Of Math Problems Formalized In Lean. http://giiubb.cmm//weesss////o/p
September 2024.
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models, April 2024.
Hanul Shin, Jung Kwon Lee, Jaehong Kim, and Jiwon Kim. Continual Learning with Deep Gener-
ative Replay, December 2017.
Tomáš
Lecopivo/Scil.ean: http://gitbbboooomccccppi////sat
Skfivan.
Scientific computing in Lean 4.
September 2024.
Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots
for theorem proving lean, 2024. URLptttp. ://arxiv.. wwtpxivvorr///booo /20../4//244.222..
Valentin Spitkovsky, Hiyan Alshawi and Daniel Jurafsky. Baby Steps: How "Less is More" in Unsupervised Dependency Parsing.
13

---

Published as a conference paper at ICLR 2025
Sandeep Subramanian, Sai Rajeswar, Francis Dutil, Chris Pal, and Aaron Courville. Adversar- ial Generation Natural Language. In Phil Blunsom, Antoine Bordes, Kyunghyun Cho, Shay Cohen, Chris Dyer, Edward Grefenstette. Karl Moritz Hermann, Laura Rimell, Jason Weston, and Scott Yih (eds.), Proceedings of the 2nd Workshop on Representation Learning for NLP, pp. 241-2511 Vancouver, Canada, August 2017. Association for Computational Linguistics. doi: 10.11865/11//11--62222
Terence Tao. Teorth/asymptotic.
Terence Tao. Teorth/newton, June 2024a.
Terence Tao. Teortblyymmtttccpprjeee,, July 2024b.
Terence Tao, Pietro Monticone, Lorenzo Luccioli, and Rémy Degenne. Teorth/pfi, August 2024.
Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An In- Context Learning Agent for Formal Theorem-Proving. August 2024.
Szymon Tworkowski, Maciej Mikula, Tomasz Odrzygozdz, Konrad Czechowski, Szymon Antoniak, Albert Q Jiang. Christian Szegedy, Lukasz Kucinski, Piotr Milos, and Yuhuai Wu. Formal Premise Selection With Language Models.
Gido M. van de Ven, Nicholas Soures, and Dhireesha Kudithipudi. Continual Learning and Catas- trophic Forgetting, March 2024.
Floris van Doom. Epvandoorm/carlesson, September 2024.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, E ukasz Kaiser, and Illia Polosukhin. Attention is All you Need. In Advances in Neural In- formation Processing Systems, volume 30. Curran Associates, Inc., 2017.
Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, and Xiaodan Liang. DT-Solver: Automated Theorem Proving with Dynamic-Tie Tree Sampling Guided by Proof-level Value Function. In Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki (eds.), Proceedings of the 61st Annual Meeting of the Association for Compulational Linguistics (Volume 1: Long Papers), pp. 12632-12646, Toronto, Canada, July 2023. Association for Computational Linguistics. doi: 10.11653/v1/2023 aa..022...lllooggg.. 706.
Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang. Jing Tang, Jian Yin, Zhenguo Li, and Xiaodan Liang. Proving Theorems Recursively, May 2024a.
Liyuan Wang, Xingxing Zhang, Hang Su, and Jun Zhu. A Comprehensive Survey of Continual Learning: Theory, Method and Application. JEEE Transactions Pattern Analysis and Machine Intelligence, 46(8):5362-5388 August 2024b. ISSN 0162-8828, 2160-9292, 1939-3539. doi: 0..109/TPAAMI..224333773
Mingzhe Wang and Jia Deng. Learning to Prove Theorems by Learning to Generate Theorems. ArXiv, February 2020.
Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theo- remLlama: Transforming General-Purpose LLMs into Lean4 Experts, October 2024c.
Eric Wieser. orii- prover. https://gihubbbcom//eriwwwssssss cot.eeaooomaaicccooooooooooooooo 2024.
The matrix cookbook, proved in the Lean theorem
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Preoee: Advancing Theorem Proving in LLMs through Large- Scale Synthetic Data, May 2024a.
Huajian Xin, Z. Z. Ren, Junxiao Song. Zhihong Shao, Wanjia Zhao Haocheng Wang. Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang. Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. DeepSeck-Prover V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search, August 2024b.
14

---

Published as a conference paper at ICLR 2025
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-Bye Models. Transactions of the Association for Computational Linguistics, 10:291-306, 2022. doi:
10.1162/tacl a 00461.
Kaiyu Yang. Fangky1I/mini22F-eeann http://gghha..ocomyyyyyyyy/////2 2024.
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. 2023. doi: 10448550ARXXV:2306.6555 15666.
Wojciech Zaremba and Ilya Sutskever. Learning to Execute, February 2015.
irratiii Zeta 3 Irrational. Ahhwuhu/zeta.3 irrational at 01666644000444404447777777771110
2024.
Jiawei Zhao, Zhenyu Zhang, Beidi Chen, Zhangyang Wang, Anima Anandkumar, and Yuandong
Tian. GaLore: Memory-Efficient LLM Training by Gradient Low-Rank Projection. [RLhttp:
Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q. Weinberger, and Yuhuai Wu. Don't Trust: Verify Grounding LLM Quantitative Reasoning with Autoformalization, March 2024.
Shuyan Zhou, Uri Alon, Frank F. Xu, Zhiruo Wang, Zhengbao Jiang, and Graham Neubig. DocPrompting: Generating Code by Retrieving the Docs, February 2023.
Zsolt Zombori, Adrian Csiszarik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban. Curricu- lum Learning and Theorem Proving. 2019.
A APPENDIX
A.1 FURTHER METHODOLOGY DETAILS
Repository Scanning and Data Extraction. We use the GitHub API to query for Lean repositorics based sorting parameters (e.g., by repository
most recently updated repositories). We maintain a list of known repositories to avoid; the list can be updated to allow LeanAgent to re- analyze the same repository on new commit Lean version.
We clone each identified repository locally using the Git version control system. To ensure compati- bility with compare it with the supported versions of our system. If the required version is incompatible, we skip the repository and move on to the next one. Otherwise, LeanAgent switches its Lean version to match the repository's 's version. This version checking is performed by parsing the repository's configuration files and extracting the specified Lean version.
tieerrm--rrving pipeline, check the Lean version required by each repository and
Dynamic Database Management. This database contains many key features that are useful in our setting. For example, it can add new repositories, update existing ones, and generate merged datasets from multiple repositories with customizable splitting strategies. In addition, it can query specific theorems or premises across repositories, track the progress proof attempts (including the proof status of sorry theorems), and analyze the structure and content of Lean proofs, including tactic sequences and proof states.
The database keeps track of various details: Repository metadata; theorems categorized already proven, sorry theorems that are proven, or sorry theorems that are unproven; premise files with their imports and individual premises; traced files for tracking which files have been processed; detailed theorem information, including file path, start/end positions, and full statements; and traced tactics with annotated versions, including the proof state before and after application.
15

---

Published as a conference paper at ICLR 2025
If we encounter duplicate theorems between repositories while merging repositories, we the theorem from the repository most recently added to the database. We deduplicate premise files and traced files by choosing the first one encountered while merging the repositories. We also generate metadata containing details of all the repositories used to generate the dataset and statistics regarding the theorems, premise files, and traced files in the dataset, such the total number of theorems.
We provide the user with many options to generate a dataset. To generate the set of theorems and proofs, the default option is simply use the theorems, proofs, premise files, and traced files from the current curriculum repository in the database. Specifically, we use the random split from LeanDojo create training, validation, and testing sets. We refrain from using the novel split from LeanDojo, as we would like LeanAgent to learn as much as possible from a repository to perform well on its hardest theorems. The data in the splits include details about the proofs of theorems, including the URI. and commit of the source repository, the file path of the theorem, the full name of the theorem, the theorem statement, the start and end positions in the source file, and a list of traced tactics with annotations. The validation and test split each contain 2% of the total theorem and proofs, following the methodology from LeanDojo. Moreover, the database uses a topologiaal sort over the traced files in the repository to generate the premise corpus. This corpus is a JSON Lines file, where each line is a JSON object consisting of a path to a Lean source file, the file's imports, and the file's premise statements and definitions.
Progressive Training of the Retriever. We describe some additional steps for progressive training. single forward pass with batch processing to serialize and
To precompute the embeddings, tokenize premises from the entire corpus. Then, we use the retriever's encoder to process the batches and generate embeddings.
sorry Theorem Proving. We start by processing the premise corpus to use it more efficiently during premise retrieval. This involves initializing directed dependency graph to represent each file path in the corpus, adding files as nodes and imports as edges, and creating transitive closure of this graph. We also track all premises encountered during this process, building a comprehensive knowledge base.
Crucially, we limit retrieval to subset of all available premises aid the effectiveness of the re- sults. Specifically, we choose the top 25% of accessible and relevant premises, following ReProver's method.
Proof Integration and Pull Request Generation. We integrate the generated proofs into the origi- nal Lean files and create pull requests to propose the changes to the repository owners. This aids the development of these repositories and functions as more training data for future research.
To achieve this, in a temporary Git branch, we iterate over the Lean files and locate the sorry key- words corresponding the generated proofs. We then replace these sorry keywords with the actual proof text, working from the bottom of each file upward to preserve the position of theorems. Af- ter integrating the proofs, commit our changes, push them, and create pull request for the repository on GitHub.
A.2 EXPERIMENT IMPLEMENTATION DETAILS
We use ReProver's retriever trained on the random split from LeanDojo. We use four NVIDIA A100 GPUs with 80GB of memory each for progressive training. LeanAgent uses a distributed architecture leveraging PyTorch Lightning and Ray for parallel processing. We use bfloat16 mixed precision and optimize with Adam W (Loshchilov & Hutter 2017) with an effective batch size of 16 (achieved through a batch size of 4 with gradient accumulation over steps). In the first 1, 1,000 steps, the learning rate warms up linearly from 0 to the maximum value of 10-3 Then it decays to 0 using a cosine schedule. In addition, we apply gradient clipping with a value of 1.0. Just as ReProver does during training, sample 3 negative premises per example, including I in-file negative premise. The maximum sequence length for the retriever is set to 1024 tokens. The maximum sequence length for the generator is set to 512 tokens for input and 128 tokens for output.
The prover uses a best-first search strategy with no limit on the maximum number of expansions of the search tree. It generates 64 tactic candidates and retrieves 100 premises for each proof state. LeanAgent uses ReProver's 's tactic generator for the experiments. We generate tactics with a beam search of size 5. We used 4 CPU workers, per GPU. Due to the wide variety of repositories and
16

---

Published as a conference paper at ICLR 2025
experimental setups that we tested, the time for each experiment widely varied. For example, the experiments in Table 10 took from to 9 days to complete.
Furthermore, we do not compare LeanAgent with any existing 4LM-based prover besides ReProver because LeanAgent is a framework, not a model. As mentioned previously, can be used with any LLM. As such, comparison would be impractical for reasons including differences in data, pre- training, and fine-tuning. We only compare with ReProver because we use ReProver's 's retriever as the starting one in LeanAgent, allowing for more faithful comparison.
Moreover, we do not compare with Aesop because is not an ML model. We aim to improve upon MI research for theorem proving, such ReProver. Moreover, Aesop is framework, but ReProver was included as the starting point of the LeanAgent framework, which is why we compare LeanAgent to ReProver. Rather than comparing against existing tools, we aim understand how lifelong learning can work in theorem proving.
Furthermore, although LeanAgent can work with other LLMs such as Llemma (Azerbayev et al, 2024) and SrepSeek-Prover (Xin et al. (024a), using these LLMs in our work would require ar- chitectural modifications that go beyond the scope of our current work. For example, the 7B model DeepSeek-Prover as well as the 7B and 34B Llemma models are not retrieval-basee -based. As such, rather than progressively training retriever, we would progressively train the entire model. This may be feasible with methods such as Gradient Low-Rank Projection (Zhao et al.), but this would lead to fundamentally different usage than we currently demonstrate. Specifically, rather than using a best- first tree search approach need to generate the entire proof at once. This setup is quite dissimilar from our current evaluation, and these results may be dissimilar from our current evaluation framework.
do with ReProver's 's retriever and tactic generator, we may instead
In addition, we would like to note that because Leant does not claim to contribute a new search algorithm, it can be used with other search strategies such Hypertree Proof Search (Lample) iet al.). However, the source code for Hypertree Proof Search was only recently released on GitHub, explaining why we did not use thus far.
Moreover, the objective function for Elastic Weight Consolidation (EWC) is given by:
L(0)= = LB
Σ F. 10:0--0400 -A..))
where (0) is the loss for the current task B, is the label for each parameter, θA, are the pa- rameters from the previous task A, F; is the Fisher information matrix, and À is hyperparameter that controls the strength of the EWC penalty. For the setups that use EWC, we performed grid search over À values in {0.01, 0.1, 1, 10, 100). For each value, we ran Setup on separate testing repositories. We found 0.1 to yield the best overall stability and plasticity scores.
A.3 REPOSITORY DETAILS
Table 5: Additional repository descriptions
Repository
Description
Prime Number Theorem And
Prime Number Theorem proof
Compfiles
Catalog of Olympiad-style math problems
FLT
Fermat's ' Last Theorem proof
Debate
Stochastic double-cfficient debate protocol Implementation of Lean4 kernel in Lean4
Lean4Lean
Matrix Cookbook
The Matrix Cookbook lemmas
Math Workshop
Detailed Lean tutorial
LeanEuclid
Euclidean Geometry
Foundation
Formal logic results
Con-nf
Consistency of Quine's New Foundations
Saturn
SAT solver-prover implementation
Zeta 3 Irrational
Proof of ((3) irrationality
Formalization of Constructable Numbers
Ancient construction problems
LeanAPAP
Kelley-Meka bound on Roth numbers
17

---

Published as a conference paper at ICLR 2025
Table 6: Repository commits. Formalization of Const. Numbers denotes Formalization of Con-
structable Numbers.
Repository
Commit
PFR
Hairy Ball Theorem
Coxeter
Mathematics in Lean Source
Formal Book
MiniF2F
04445555555070044444444444444453
SciLean
Carleson
Lean4 PDL
Prime Number Theorem And
Compfiles
FLT
Debate
Lean4Lean
Matrix Cookbook
Math Workshop
LeanEuclid
Foundation
Con-nf
Saturn
Zeta 3 Irrational
Formalization of Const, Numbers
LeanAPAP
Table 7: Repository orders (initial curriculum). Note that Popularity Order is by star count on
August 20, 2024.
Curriculum Order
Popularity Order
Compfiles
SciLean
2
Mathematics in Lean Source
FLT
Prime Number Theorem And
PFR
4
Math Workshop
Prime Number Theorem And
FLT
Compfiles
PFR
Debate
SciLean
Mathematics in Lean Source
Debate
Lean4Lean
Matrix Cookbook
Matrix Cookbook
10
Con-nf
Math Workshop
11
Foundation
LeanEuclid
12
Saturn
Foundation
13
LeanEuclid
Con-nf
Lean4Lean
Saturn
Table 8: Curriculum order (sub-curriculum)
#
Curriculum Order
1
Zeta 3 Irrational
2
Formal Book
3
Formalization of Constructable Numbers
4
Carleson
5
LeanAPAP
6
Hairy Ball Theorem
7
Coxeter
8
Lean4 PDL
18

---

Published as a conference paper at ICLR 2025
Table 9: Repository theorem and premise counts
Repository
Total Theorems
Total Premises
PFR
74306
109855
Hairy Ball Theorem
73026
131217
Coxeter
71273
127608
Mathematics Lean Source
78886
117699
Formal Book
74654
112458
MiniF2F
71313
127202
SciLean
72244
129711
Carleson
73851
109334
Lean4 PDL
20599
46400
Prime Number Theorem And
79147
1 115751
Compfiles
121391
178108
FLT
75082
1 114830
Debate
68853
103684
Lean4Lean
2559
22689
Matrix Cookbook
67585
102294
Math Workshop
76942
115458
LeanEuclid
15423
40555
Foundation
25047
57964
Con-nf
29489
64177
Saturn
10982
34497
7eta 3 Irrational
120174
176332
Formalization of Const. Numbers LeanAPAP
74050
109645
71090
109477
Repository Statistics and Information. Additional repository descriptions are in Table The commits we used for experiments in Table 6 Moreover, the repository orders are detailed in Ta- ble and 8 Furthermore, the total number theorems and premises per repository (including dependencies) in Table
Repository Selection Process. Many repositories have issues such as incompatibilities with Le- anDojo, unsupported Lean versions, and build failures. As such, our process for choosing the 14 repositories in the first curriculum was simply using LeanAgent to extract information from the most popular repositories on GitHub. We disregard incompatible and inapplicable ones, such as those with no theorems. We performed this process on August 20, 2024. We performed a similar process for the eight repositories in the second curriculum with two differences: (1) We checked that the number of sorry theorems visible from GitHub was at least 10. This narrowed down the available repositories significantly. (2) We included some more recently updated repositories to provide some variety in the age of the repositories in our curriculum. We performed this process on September 14, 2024. However, many of the repositories that passed this test had fewer than 10 sorry theorems when processed by LeanDojo; this is mainly due to the functionalities of LeanDojo.
A.4 LIFELONG LEARNING METRIC DETAILS
Prior work has noted that lifelong learning methods generally lack standard evaluation metrics (De Lange et al. 2023 Diaz-Rodríguez et al. 2018). As such, our selection primarily focused on metrics that emphasized a change over time, aligning with our problem setup. In addition, we moved metrics that were redundant. For example, prior work suggests that evaluating lifelong learn- ing frameworks only after each task, rather than over time, leads to substantial forgetting (De Lange et al. 2023). As such, we adopt WF and WP in our analysis of LeanAgent. We use window size of for WF and WP as this represents a relatively medium-term understanding, given that we have 14 repositories. This would provide balanced interpretation of forgetting and plasticity. Furthermore, we use the EBWT metric, in line with previous work, to evaluate LeanAgent throughout its lifetime chose not to include the Forward Transfer metric as prior work has shown that a lower FM leads to better forward transfer (Chen al. 2023). As such, only check FM. We also chose not include lifelong learning met-
rather than simply at the end Diaz- Rodriguez et al. 2018). Moreover,
19

---

Published as a conference paper at ICLR 2025
rics for overall performance, such as Time Weighted Cumulative Performance (TWCP), Area Under the Learning Curve (AULC), and Average Accuracy (AA), as these would lead to redundancy in our analysis. Specifically, the metrics we chose were all computed using validation R@ 10 and the average test @ 10, which are already measures of I LeanAgent's performance.
We provide some additional details on the metrics we used. Windowed- Windowed-Forgettingg 5 (WF5) quan- tifies model stability by measuring the maximum performance decrease in average test R@ 10 over stiding window of evaluations. Following prior work, we define WF for given window size and then average it over all evaluation tasks to provide a single measure of stability, Moreover, Catastrophic Forgetting Resilience (CFR) is a key indicator of the subilittyplastiiciis trade-off. Fur- thermore, the Forgetting Measure (FM) measures the negative influence that learning task has on the test @@ 10 of all old tasks. It is the average forgetting of all old tasks, where forgetting of a task is the difference between its highest and current performance. Furthermore, BWT measures the positive influence of learning a new task on the test R @ 10 of old tasks. EBWT improves upon this metric by considering the average of the BWT computed after each task. Mandowedd-laattciie 5 (WP5) measures the ability to learn new information by quantifying the maximum average test R @ 10 increase over sliding window of 5 evaluations. Incremental Plasticity (IP) tracks changes in validation @@ 10 for each task over time.
However, it is important to note that our lifelong learning metrics have different interpretations in the Merge All dataset construction strategy, which differs from the traditional rask-incremental setup. To knowledge, interpretation of these metrics in this setting has not been thoroughly conducted. As such, we propose that metrics should be interpreted with an understanding that they may reflect an adaptation gradual shifts in data distribution rather than abrupt task changes. Specifically, WF5 may reflect not just forgetting old tasks but also the ability to balance and retain knowledge across an expanding dataset. WP5 could indicate how well the model adapts to the growing complexity of the combined dataset rather than purely learning new, isolated tasks. FM, in this context, may represent the ability to maintain performance on earlier data points as the dataset grows. EBWT might reflect the capacity to leverage newly added data to improve performance on the entire historical dataset. CFR becomes a measure of stability in the face of an expanding, potentially more complex dataset. IP may represent how quickly the model adapts to the evolving nature of the combined dataset rather than discrete new tasks. These metrics in the Merge All case measure the ability to accumulate and refine knowledge over time rather than strictly measuring performance
isolated tasks.
is worth analyzing the effect of EWC. Our results in Sec. 4.3 suggest that the effect of EWC is not uniform across different task-ordering strategies. In aurriculum-based ordering. EWC seems to improve plasticity (WP5 and IP) at the cost of stability and continuous improvement (WF5, FM, EBWT, and CFR). An exception is Setup 7, which improves WP5 and FM. This suggests that the Merge All strategy creates a more nuanced balance between stability and plasticity. EWC generally improves stability and plasticity metrics, except IP, in the popularity order for the Single Repository strategy. This may be because this ordering is less optimized for learning, and EWC helps to mitigate ordering,
some of its shortcomings. However, when used with more effective curriculum- EWC interferes with the carefully structured learning process, leading to mixed results. Moreover, in the Merge All scenario, EWC offers benefits only for the curriculum learning setups, suggesting that its effectiveness might be limited in more complex, merged datasets. This can be explained by the fact that the Merge All strategy is a memory-basee approach to lifelong learning. As such, using both EWC and the Merge All strategy may lead to excessive stability. This analysis further explains why LeanAgent's setup is superior.
A.5 FURTHER sorry THEOREM PROVING DISCUSSION
We provide some additional discussion on the results in Table
First, we note that comparing LeanAgent to ReProvert, the fine-tuning baseline, is not a direct comparison. Specifically, we note how mathematicians often formalize across multiple domains and projects simultaneously or cyclically. We use this as motivation for connecting mathematical knowledge between domains. Moreover, a key use case is formalizing new repositories without retraining the entire dataset each time. When mathematician creates some new repositories and adds them to a curriculum, they can simply progressively train LeanAgent on the new repositories while maintaining performance on previous ones, shown in experiments with both the initial
20

---

Published as a conference paper at ICLR 2025
Table 10: Accuracy comparison across setups. Accuracy is calculated (proven theorems total sorry theorems). MIL denotes the Mathematics in Lean Source repository, LA denotes LeanAgent, and SX denotes Setup X (e.g.. is Setup 1). The best accuracy for each repository is in bold.
Repository
#sorrys
Accuracy
LA
S1
S2
S3
S4
55
S6
S7
MIL
72.4
55.2
41.4
55.2
55.2
48.3
58.6
48.3
SciLean
294
9.2
8.5
7.5
6.8
8.5
8.5
8.8
7.8
PFR
37
2.7
0.0
0.0
0.0
0.0
0.0
0.0
0.0
curriculum and sub-currieulum. This is much more practical than retraining on the entire dataset, which would be expensive in terms of compute and time, especially as the number of repositories grows.
Moreover, data scarcity is a major problem in theorem proving. As such, having enough high- quality data for effective pre-training on all repositories may not feasible. Training on all data, an approach similar to existing work, could prevent the model from generalizing to new repositories. However, LeanAgent does not have this restraint as it continuously generalizes to and improves on ever-expanding mathematical knowledge without forgetting previously learned knowledge.
In addition, the results Table 4 show that our lifelong learning setup leads to effective backward transfer. This is a strong advantage that pre-training does not provide and is also reason why LeanAgent demonstrates progressive learning, starting with basic concepts and advancing to more complex ones. Also, although not a direct comparison to the pre-training approach, the "Merge All" strategy indicates decreased performance over time. This dataset strategy can be interpreted being closer to pre-training than the "Single Repository" strategy, suggesting lower than desired pre-training performance when training on all data.
Second, we note that LeanAgent improves over the direct fine-tuning baseline on various reposito- ries, including MiniF2F, Scilean, and PFR. We find that these repositories contain a range of math- ematical concepts that require progressively the effectiveness of our lifelong learning approach in continuously generalizing to and improving on expanding mathematical knowledge without catastrophic forgetting.
advanced reasoning capabilities. This highlights
In addition to comparing LeanAgent and ReProver, we conduct an ablation study between LeanA- gent and the seven variants discussed in Sec. 4.3 regarding the original curriculum. The detailed sorry theorem proving comparison, which focuses on some of the repositories compared in [Sec.] 4.2 is in Table 10, Note that when using the Merge All strategy, only sorry theorems from the new repository are proven during each iteration of lifelong learning. We devote the rest of this section to the detailed comparison sorry theorems that these setups can prove.
Mathematics in Lean Source. We notice progression in LeanAgent's proving ability in the Math- ematics Lean Source repository. During lifelong learning, LeanAgent demonstrates a grasp of fundamental algebraic structures and basic mathematical operations:
a) Group and Ring Theory: LeanAgent proves theorems about basic algebraic structures. For in- stance, MyGroup hhuu-right_lle shows that multiplying an element by its inverse yields the identity and MyRing. add right cancel demonstrates the cancellation property in ring addi- tion.
21

---

Published as a conference paper at ICLR 2025
theorem mul_right,_ inv G) a- := by simp
theorem add r right_cancel {a c Ry a b) simpa us ing h
b) Elementary Number Theory: LeanAgent handles fundamental arithmetic properties, in- cluding MyRing, zero.mul, which proves that zero multiplied by any number is zero, and MyRing which shows that the negative of a negative number the original number.
thearem mul R)
by
Fw [MulZeroClass.2 peroeeerrrmmma ]_ml]]
theorem neg_neg (a -a by simp
c) Order Theory: LeanAgent grasps order theory, as evidenced by absorbl, which proves that infimum of and the supremum of and y is always equal to and absorb2, which demonstrates that the supremum and the infimum x and y is always equal to x.
theorem absorbl
(x U y) = x by
imp
theorem absorb2 s imp
U n y := by
d) Rudimentary Real Analysis: LeanAgent demonstrates early capability to handle properties lated to real numbers and absolute values, as shown by c03s05. MyAbs abs add, which proves the triangle inequality for real numbers.
22

---

Published as a conference paper at ICLR 2025
theorem abs_add (x y R) : |x s |x| + lyl := by
apply abs _dd le
10/14 of these proven sorry theorems from Mathematics in Lean Source during the lifelong learning process are from the exercise file for proving identities about algebraic structures. This indicates that LeanAgent starts its grasp of mathematical concepts from the basics.
Crucially, by the end of the lifelong learning process, LeanAgent exhibits significant growth in its mathematical reasoning abilities:
a) Quantifier Manipulation: LeanAgent exhibits more advanced logical reasoning by managing mul- tiple quantifiers and implications, evidenced by C03501 mym_mllmmmmt mny_lemma3. which proves com- plex statement involving bounds and absolute values with multiple quantifiers and conditions, and C03S05 MyAbs abs.lt, which establishes that the absolute value being less than y equiv- y.
alent to yy < x A x
theorem my my_ 1enma3 {x R}, <
[X] M lyl <E- |x <
apply 003501. my lemma
theorem abs It
- <xXxy< by
cases
exact abs_lt
b) Set Theory and Relations: LeanAgent handles abstract set-theoretic concepts, as shown by c03501 Subset. trans, which proves that subset relations are transitive.
theorem Subset. trans exact Set. Subset. traset trans
by
23

---

Published as a conference paper at ICLR 2025
Now, only 2/7 sorry theorems from Mathematics in Lean Source from the exercise file for prov- ing identities about algebraic structures. This suggests that lifelong learning allowed LeanAgent to transition to gaining stronger ability to work with premises for more complicated proofs.
We gain some insights from comparing the performance LeanAgent over time on Mathematics in Lean Source to other setups. For example, the fact that ReProver handle harder theorems out of the box, such as CC3501 my mny_leeman _1mma,, , but fewer theorems overall suggests that it has a broader knowledge base initially but loses performance from lack of adaptability, Furthermore, Setup proves the same sorry theorems as LeanAgent does during lifelong learning. This suggests that pure curriculum learning without EWC the Merge All strategy emphasizes grasping easier concepts earlier. This mimics the insights gained from the lifelong learning analysis. However, Setups 3 and (curriculum with EWC and/or Merge All) demonstrate some knowledge plasticity, proving harder theorems during lifelong learning, such C03501 Subset. trans in Setup 3. However, this comes the cost of proving basic theorems, showing catastrophic forgetting. For example, Setups and could not prove the trivial theorems MyGroup mul - rightiiiii and MyRing vero_mule respectively, during lifelong learning, whereas LeanAgent could. This again aligns with the insights from the lifelong learning scores from previous analysis.
By the end of lifelong learning, the sorry theorems that LeanAgent prove from Mathematics in Lean Source long learning setup provides continuously improving capabilities to reason about more advanced premises and proofs than other setups. For example, LeanAgent is the only system, except for Setup 6, which can prove theorem CC3S05 MyAbs abs_lt. LeanAgent achieved this by using the available premises, such abs_lt with statement similar C03505 MyAAs. abs_lt.
superset of those that the other setups prove. This shows that LeanAgent's life-
An interesting case study can be found in the dichotomy between the theorems C03S05 MyAbs weg. and C03$05 c03s05.MyAbs le_abs.self. LeanAgent can prove CC3S05, 903505.MyAbs neg_le_abs_sell by referencing C03805 MyAbs, le le_abs-self, which is still unproven that point:
theorem neg_ lc_abs_____________________e self (x R) - |x| := by sippa using ce3s05. MyAbs. abs_self (-x)
At the end of lifelong learning, LeanAgent can prove C03505. MyAbs. .e abs sel. f:
theorem le_abs jelf (x B) |x] := by
FW [le_abs abs]
5 Limp
24

---

Published as a conference paper at ICLR 2025
It achieves this through its of the le_abs premise, which provides conditions for when element is less than or equal to the absolute value of another. This suggests that LeanAgent begins by using existing knowledge where possible before trying to realizing why existing facts are reasonable.
SciLean. We examine the sorry theorems from SciLean that LeanAgent proved to gain some further key insights about its performance. During the lifelong learning process, LeanAgent demonstrated stronger understanding relative to ReProver in a wide range of mathematical concepts from SciLeen. These theorems primarily focus on:
a) Fundamental Algebraic Structures: LeanAgent proves basic algebraic operations and properties, such Sci Scin. scal aarllladdvviiiii which proves that dividing any number by yields the same number, Scilean. scwlar.min.zeroooo...o tween 0 and 1 is and Function con invFinnuu un. id rule, which proves that the inverse of the identity function is the identity function itself.
which demonstrates the minimum value be-
theorem scalar_div_on (x R) == by simmp
theorem scalar Baolar_min_____ _ero_one min (0 R) (1 RJ := by rw [min_comm] simp
theorem rule : LnvFun (fun (x X) x) fun => := by
apply Function. comp exact Function. injective id
b) Linear and Affine Maps: LeanAgent handles basic properties of linear and affine maps effectively,
recognizing their structure in IsLinea www.pp.ssiinnaaaaa..... which proves the linearity of function applications, and IsAffineMap. IsAf IsAffineMap.appi which demonstrates the affine property of function applications.
theoren isLinearMap_appe (1 1) IsLinearHap (fun (1 1) 1) :- by all_goals
theoren LnAMaLn apply (1 1) ineMap (fun (1 1) := by constructor
constructor
simp
stmp
Measure Theory Basics: LeanAgent starts grasping theory concepts, exem- plified by SciLean. ite pull measureOf, which handles conditional measure selec- tion between measures based proposition, Lean Meiieee.. Mew.uMe. prod volume,
25

---

Published as a conference paper at ICLR 2025
which proves that the product of two volume measures is the volume measure itself, and SciLean. Stte.pull.enneea..ooeee tended non-negative real and converting it to real is equivalent to converting the individual com- ponents first.
which proves that conditionally pulling out an ex-
theorem Lte putl, neasureef (X) [Measurablespp]
Prop) [Dec Idable
(u Measure X) (A Set x)
(if then else v) A
(if then A else A) : by split_ifs <;> rfl
theorem Measure. volune (X Y} [MeasureSpace [MeasureSpace Y1
(Neasure. prod (volume Measure X) (volume Measure Y) volume :- by
rfl
theorem ennreal toReal Prop) [Decidable ENNReal)
then else y). toReal
(if then toReal else toReal by spl(t_ rfl
d) Floating-Pou Point Operations: LeanAgent demonstrates early grasp of floating- point representa- tions and their correspondence to real numbers, shown by SciLean. re float, proving that floating-point number's real-like part is itself.
theorem re. float (a Float) ) : RCLike. re := by
exact RCLike, sel_e____l.____eeee of le le_rfl
The proofs during this phase are characteristically concise, often using basic tactics like simp, rfl, aesop that do not premises. This suggests that LeanAgent recognizes these theorems straightforward enough to prove without the complex retrieval of premises.
Crucially, by the end of the lifelong learning process, LeanAgent exhibits significant growth in its mathematical reasoning abilities on SciLean, just as it did with Mathematics in Lean Source:
Advanced Function Spaces: LeanAgent understands concepts in advanced function spaces, such as Cont CDi IMapPD at which demonstrates the eta reduction property for contin- uously differentiable maps finite dimensions.
26

---

Published as a conference paper at ICLR 2025
theorem CD eta -FD[K,n] (fun -FD[K,n] x) by
simp only [DFunL wit.tieeeettt.. ext_[ff)
aesop
b) Sophisticated Bijections:
LeanAgent grows work with product spaces and bijections, proving theorems such as wewa..k..rg....r.e.o arq.fst www.eettiee.erle..iii..........e Function. BijnBBijeciiiee.. Prod. mk
ability to
which proves the bijectivity of function that swaps elements in product space and Function. Bijectivve Equivv invFun. arg a0. N0.Bijective rule, which proves that the composition of bijection and its inverse remains bijective. Crucially, these theorems might seem simple, but they demonstrate LeanAgent's capability to handle abstract algebraic thinking.
att_arssssssdddd. ftt.sddddddddd f.s.ssd.Bieeetiiie site_sinple"
arg.
BLjective ('fn xy X=Y (xy.2, xy.1l)
: by
constructor <;> intro h ggoals aesop
theoren Equtv. LnvFun. .ar..arg.... a8. M..Bjecctive rute (f Y Z) (g X 2) (ht Bijective
BE Biject Lve (un => f. invFun (g x]] == by convert
stop [hf] exact F.symm. b Dijective coc.cooco hf
c) Abstract Algebraic Structures: LeanAgent proves further abstract algebraic properties, including Sci Lean, CDi fferentialle. id rule, which proves that the identity function is continu- ously differentiable.
thearem CDifferentiable id_rule (Differentiable K (fun X => x) := by
intro x unfold SciLean. CD CDifferent tableAt tauto
d) Data Structures in Mathematics: LeanAgent navigates proofs involving array types in mathe- matical context, proving theorems such as SciLeam ArrayType. Acrayyn..r ext, which proves that two arrays are equal if their elements equal at all indices.
27

---

Published as a conference paper at ICLR 2025
theorem ext [x y Cont) : (A i, x[i] y(i]) = := by
intra
apply SciLean. www.eean.Arraayppe..ooo get gett-geee_iijeeiveeee
simp only [h]
Aeant proved this theorem about traditionally computer-scienne-orintee data structure from a mathematical lens, which some other setups could not do.
The proofs this stage more sophisticated, involving multiple steps and combining various mathematical concepts. This indicates a deeper ability to connect different areas of mathematics.
The progression from basic algebraic structures advanced function spaces and data structures (like array types) shows that LeanAgent is bridging the gap between pure mathematical concepts and their applications in computational mathematics. Furthermore, the progression from basic inte- gral manipulations to advanced function spaces indicates that LeanAgent is improving its premise selection over time. learns to identify and apply more sophisticated mathematical structures and theorems premises.
By the end of lifelong learning, the sorry theorems that LeanAgent proves from SciLean are almost entirely a superset of those that the other setups prove. This corroborates our previous assertion from our analysis of the sorry theorems from Mathematics in Lean Source that LeanAgent's 's lifelong learning setup provides it with continuously improving capabilities to reason about premises and proofs that outperform other setups.
Crucially, LeanAgent could prove re re-float during lifelong learning while other setup could. This indicates that LeanAgent's more measured and stable approach allowed it to grasp floating- point representations and their relation to reals. At the same time, other setups prioritized this less with their reduced stability. This may also suggest that continuous improvement allowed LeanAgent process new and unique concepts from new repositories.
We gain some interesting insights from comparing the performance of LeanAgent over time on SciLean other setups. For example, the fact that ReProver could prove the trivial theorem SciLean. wtt.puul.eennerall....... oReal while LeanAgent could, even during lifelong learning, suggests that this baseline cannot handle foundational concepts. LeanAgent has better grasp of these concepts from lifelong learning. This is due to the increased stability of LeanAgent and im- provement from learning a new task, as shown in the lifelong learning metric analysis in Sec. 4.3
intriguing observation is that Setup 3 could prove Function. Bijectiveeeeeeeeeeeee Prod. mx fst.ss..dddd. Bi jejeeciveeerie soectiverrule rule. www.errrreessseeeeeeeeeeeeeeeeee simple' lifelong learning. However, as mentioned above, LeanAgent could only prove this theorem at the end of lifelong learning. This suggests that Setup is more plastic during lifelong learning, while LeanAgent remains more stable. This corroborates the analysis from the lifelong learning metrics. However, this again comes at the cost of grasping basic theorems. For example, Setup cannot prove the trivial measure theory theorem SciLean. ..Maaurree.... proddvoll lme, whereas LeanAgent could during lifelong learning, again suggesting that favors plasticity over stability.
Furthermore,
during
An interesting case is that LeanAgent prove Gein www.:oosscaaaac.. during lifelong learn ing but not SciLean. norm2 s scalar. Conversely, Setup proved SciLean. norm2 scalar but not S Lean, norm2 scals scalar.
28

---

Published as a conference paper at ICLR 2025
thcorem scalar {R) [RealScalar RJ
[[]]|[[R] Scalar.abs by
[SciLean. scalar (clleannscalar_nommm)
theorem norm2 scalar (R) [RealScalar R] (x
||x||= [R] = x i= by
symm
stmp [sq]
congr
s tmmp
Setup 2 uses the sq premise from ma tatthhb444 which states that the square of an element the same multiplying that element by itself, while LeanAgent used the Sei Lean ocalar... m_norrm premise from SciLean, which states that the 2-norm of a real scalar is equal to the absolute value of that scalar. This suggests that LeanAgent prefers use new premises if possible rather than simplistic pre- trained ones. This also makes sense since Setup 2 uses popularity order, which generally provides poor stability and plasticity.
PFR. Crucially, LeanAgent is the only setup to prove sorry theorem from PFR. We can prove condRho o ww..raansla... ate, which states form of translation invariance property of randomness measures.
lemna condRho of translate (o Type*) [MeasureSpace 0] (X 0 5) (A Finset G) (s:G) condãho (fun a 5) Y A condRho X A by simp only [condRho, rho_of of__tranlaatee
LeanAgent suggests that the proof is straightforward after expanding definitions of condRho and considering how rho, the randomness measure, behaves under translation (as captured by the tho.of.translee lemma). The fact that LeanAgent could trivially identify such short proof using existing premises while the maintainers of the PFR repository did not suggests the power of our approach. This suggests that by learning the foundations of the PFR lemmas using its improved stability, LeanAgent was able grasp some basic definitions.
However, LeanAgent and other setups could not prove any PFR theorems after lifelong learning. This suggests that LeanAgent requires more training time or data to further strengthen its knowledge in this new area of mathematics.
We also analyze whether LeanAgent can general- ize to different commit of a repository in the curriculum. We choose commit (5516906488244477706666222222222
Alternate PFR Commit.
because PFR/RhoFFnntionall.enn from which proved condRho ww..rrassaattttt...... in the newer commit, did not exist in the old commit. This allowed the sorry theorems the old commit to be more distinct. proved two theorems, including the theorem multiDist.com copying random variables across different measure spaces that ReProver could not. LeanAgent achieved this with just the tactic rfl. However, these statements were about mu t tiDis sts another
the file
about the equality of distributions when
29

---

Published as a conference paper at ICLR 2025
sorry theorem. Since any two instances of sorry automatically equal by rfl, LeanAgent exploits this technicality to prove the two theorems.
lerma mult coultiiistcoppp {m:h) {o Type*} Fin Type*}
Fin MeasureSpace ())
(hQ": Fun MeasureSpace (0' ()) (X Fin (0 ()
(X' Fun (Q' G)
(hident: y i, IdentDistrib (X (x' () (hQ 1) volune (ha' i vo volume)
D[X hū] D[X' ha'l by
rfl
Lemma multiDist of perm (m:N) {o: Fin m Type*}
(hQ (i : Fin m) - MeasureSpace (a U)
(X : (t Fin m) (o 1) G) (9 Equiv.Pern (Fin m))
D[X ha] fun i (o 1); fun ha (9 1)]:= == by
This commit also provides another interesting example. The PFR maintainers used as a placeholder for some sorry theorems, five of which are multifau min exists, multiTau mi sus.umu... le, sub multiDistance le, sub condMult snndMultibistance le, sub_condMule miiiiiitaan sissnncneeee lee.. Interestingly, LeanAgent finds unintended constructs and proves these theorems with this proof:
Lenma [Tau multiTTaumin_extss min_exists by nontriviality s imp
apply @zero_ ne_ me_one
exact bultidist_eq_zer
combines the known fact that 0 / 1 with the placeholder theorem www.mmmiiii.t..e.ee....... which states 0 = 1. As such, it proves False, allowing it to derive anything, including 0 =
MiniF2F. This repository consists of validation and test split. Prior work evaluated performance as the number of sorry theorems proved and a Pass k metric on the test split (Yang et al., 2023). However, given that LeanAgent is framework, not model, quantitatively comparing with exist- ing methods using @ass@k k metric is misleading. In line with our existing setups, we do not treat MiniF2F as a benchmark. Instead, we disregard its existing splits and compare LeanAgent's proven sorry theorems with those of ReProver.
LeanAgent can prove 99 theorems, while ReProver can only prove 85. As mentioned in Sec. 4.2 append MiniF2F to the initial curriculum to demonstrate the use case of formalizing new repository in parallel with the ones the starting curriculum. As such, interesting observations can be made by comparing ReProver (starting point) with LeanAgent (ending point). The types of sorry theorems LeanAgent can prove demonstrate its increasing understanding relative to ReProver in complex mathematical concepts due lifelong learning.
30

---

Published as a conference paper at ICLR 2025
ReProver initially demonstrated proficiency in range of foundational mathematical areas MiniF2F:
a) Basic Arithmetic and Number Theory: ReProver could handle simple arithmetic and modu- lar arithmetic problems, such as mathd numbertheory 254, a theorem about modular arith- metic and basic addition, mathd www.nnmmmeeettt a theorem about simple exponentiation. These proofs only rely on the no crmnnum tactic, which evaluates arithmetic expressions. This suggests less sophisticated prov- ing ability of mathematics at the start of lifelong learning.
-32, theorem about basic divisibility, and
theorem heardd_nmmbeetherry..o 254 (239 + 174 83) % nora_num
:= by
theorem wethddnnmberrhhory_BBe 54 % 6 = 0 := by nora
theorem mathd www.aallggbaaaa. 3004 91^2 8281 by nora_num
b) Elementary Algebra: ReProver could solve basic algebraic equations and perform straightfor- ward manipulations, such mathd.algebra.14] which proves statement about quadratic expressions, mathd algebra 329, which shows grasp of systems of linear equations, and mathd agebrr 547, which proves basic algebraic manipulation with roots.
31

---

Published as a conference paper at ICLR 2025
thearem mathd aa algebra__le 141
(a b R.)
(h: (a b)=180)
(ha : 2 (a b)=54) :
(a^2 + b*2) = 369 := by
nlinarith
theorem mathd algebra__aaa 329
(x R.)
y = x)
(hx : 2 x + 5 y = 11) :
X + y = 4 := by
linarith
theorem
(x R.)
(he x 5)
(ha y = 2)
Real.sort (x
y) = 11 := by
simp [ho, h1, sq]
rv [Real.sort_egs _q__tt___________ iff __f__q_______________f sq_eqs <i>
norm num
num
c) Basic Calculus and Analysis: ReProver showed early capabilities in dealing with logarithms and exponentials, including mat mathhaalgebaa4433 a theorem involving dividing logarithmic expres- sions.
theorem ma matthd alggerra_a44. 484 Real. log Field_simg
Real. log
rw [- Real. log rpow] all_goals norm_num
Notably, the proofs at this stage were characteristically concise, often using basic tactics like norm_num, linarith, and field_simp. This suggests that ReProver recognized these theo- rems as straightforward enough to prove without complex retrieval of premises, similar to its behav- ior with previous repositories.
However, by the end of the lifelong learning process, LeanAgent exhibited significant growth in its mathematical reasoning abilities MiniF2F:
a) Advanced Number Theory: LeanAgent showed a more advanced grasp of number theory, prov- complex theorem about divisibility involving
ing theorems like mat complex expression and mathd numbertheory 233, a theorem dealing with modular arithmetic in ZMod 11
32

---

Published as a conference paper at ICLR 2025
theorem mathd_ haahhdd_uubberhhory...o
(n R)
(ho 9)
(h: 11/20 100 + n 7)
n = == by
omega
theorem mathd www.neeteeerrr.ee...
(b ZMod (11~2))
(he 24-
b 116 by
exact he
b) Sophisticated Algebra: LeanAgent showed better grasp of more complex algebraic manipula- tions. Theorems include mathd algebra 148, which involves function definitions and solving for unknown coefficients, and amc 2a_201 6_p3, involving special case function.
theorem mathd_algebra 148
(c (.)
{f R R))
the V x, x
x 9
(hr f 2 = 9)
c 3 := by
[ho
p3
-BI
(he
(_ 8), 1x - Int. (x yI)
f (3 (-12 5)) 40) by
norm_num [h+]
Field_simp
norm_cast
LeanAgent demonstrated improved capabilities in handling more complex analytical problems, including mat hd algebra 270, a theorem involving function composition and rational expressions.
Advanced Calculus and Analysis:
33

---

Published as a conference paper at ICLR 2025
theorem mathd algebra_22 (f - 3)
(he : x, x = -2 -> x (x 2))
(f 1) 3/7 :- by
set set_opt ion lon tactic. wwwpppsssiidndnnaaannnnne false in norm_num [ho]]
d) Complex Induction: LeanAgent became adept at more advanced induction proofs. An example is inductionn Induction.12dee ioductioon12ddd4xxxxxpp p20, a theorem about divisibility that requires an induction proof.
theorem induction httpuciionn/dvvddeeppppp.... (n : N) 12 4*(n+1) 20 := by
norm_num
Lnduction' with n hn
s imp
omega
e) Complex Quantifiers and Incqualities: LeanAgent increased its ability to prove more complex logical statements, such as amc 2a 2002 p6, theorem involving multiple existential quantifiers and inequalities.
theorem 2002 p6 lift Nr using cases' n with exact (_, Lt_ _f__oo__________________________ right. zero zero_lt_one one, 1, by simp?
n,
pJ by
The proofs at this later stage are more sophisticated, usually involving multiple steps and com- bining various mathematical concepts or indicating better ability connect different areas of mathematics, mirroring the progression observed in Mathematics in Lean Source and Scil ean. For example, as shown above, LeanAgent provides a one-line proof to the relatively advanced theorem mathd_numbertheo. 233. The proof means the hypothesis directly proves the goal. This sug- gests that LeanAgent grasps modular arithmetic and recognizes when a given hypothesis is sufficient prove the goal without additional steps.
Furthermore, as shown above, LeanAgent uses four tactics to prove the induction.12dvd4eee
theorem. This demonstrates its ability to handle more complex number theory proofs and use advanced tactics. This again shows that LeanAgent can recognize when does not require complex premise retrieval.
34

---

Published as a conference paper at ICLR 2025
LeanAgent demonstrates similar grasp of the theorem amc12a.20022 the simple premises ot.add..f.pos.r' ight, which describes how an element is less than that element added with positive one, and zero 1t one, which states that 0 is less than 1, with more advanced tactics like 1 lift, cases, and exact with complex term construction. This demon- strates its ability to reuse foundational concepts for more complex proofs of abstract mathematical concepts, showing its stability.
Notably, it combines
Importantly, LeanAgent's performance on MiniF2F showcases its ability to adapt and improve across different mathematical domains. We see this in the progression from ReProver's basic arith- metic and algebra LeanAgent's more advanced number theory, calculus, and abstract algebra. This aligns with the observations from Mathematics in Lean Source and SciLean, further support- ing the effectiveness of Leanttent's lifelong learning approach theorem proving across various mathematical repositories.
Furthermore, early proofs from ReProver dealt with concrete numbers and simple equations. Later proofs from LeanAgent involved more abstract concepts like equivalence relations and function properties. LeanAgent gained the capability to handle more complex number theory problems involving divisibility under constraints. Moreover, LeanAgent shifted from solving basic linear and quadratic equations to analyzing functions and their compositions. Also, early proofs often used norm num for straightforward computations. Later proofs employed more varied tactics and premises, suggesting a more sophisticated approach to proof construction. This all crucially suggests that while existing methods, like ReProver, may be more tailored to simpler computation problems, LeanAgent is superior on complex and analytical problems. These are precisely the types of prob- lems present in advanced mathematics. This also corroborates LeanAgent's performance on the repositories mentioned previously.
In addition, we evaluate LeanAgent on the Lean4 version of the MiniF2F test set using the same experimental setup from prior experiments, taking care not to progressively train on Test and only proving sorry theorems from it. The results are as follows:
LeanAgent: Pass@ 1 of 38.1% % (93 / 244 theorems)
ReProver (our run on Lean4): @ass@ of 34.0% (83 / 244 theorems)
ReProver was only tested on the Lean3 test set in the LeanDojo paper, so we ran ReProver on the Lean4 test set for a fairer comparison. TheoremLlama (Wang et al. 2024c reports 33.61% % cumulative accuracy on the Lean4 test set, but this makes direct comparison with the Pass@ rates of LeanAgent and ReProver infeasible. Moreover, PrepSeek-Proved V1.5 (Xin et al., 2024b) reports a state-of-the-arr result of 63.5% on the Lean4 test set.
However, LeanAgent a lifelong learning framework, not model. The performance of LeanAgent is dependent on the retriever used as the starting point ReProver's retriever in our case. As such, the metrics for other methods besides ReProver cannot be directly compared with LeanAgent. Such comparison would be impractical for reasons including differences in data, pretraining, and fine- tuning. Again, we only compare with ReProver because we use ReProver's s retriever as the starting one in Lean LeanAgent, allowing for more faithful comparison. We use ReProver because past work has shown that retrieval leads to improved generalizability.
Moreover, design LeanAgent to continuously generalize to and improve ever-expanding math- ematical knowledge without forgetting previously learned knowledge. Our goal is not to beat the MiniF2F benchmark; instead, we aim perform well in proving sorry theorems across a range of diverse repositories. The other approaches mentioned focus on different objectives and don't address the lifelong learning aspect that is central our work.
Formal Book. We first examine the sorry theorems from Formal Book that LeanAgent proved during lifelong learning. These theorems centered around:
a) Real Analysis and Inequalities: LeanAgent demonstrates a better understanding relative ReProver in real number properties and can handle basic inequality reasoning. proving book. irratiton ional. lm aux i ii, which involves real analysis and incqualities.
35

---

Published as a conference paper at ICLR 2025
Lemma Lem (x (h x) (h
(0 f_aux x) (f_aux R) n. n.factorial) by
constructor <;> linarith
b) Number Theory: LeanAgent shows capabilities in fundamental number theory concepts, proving book. quadratiic.recipproee quudratt....ciipoaatttt.... a key result in quadratic reciprocity.
theorem quadratic_reciproctiee rer___rrccrpr___22 (p : N) (hp P 2) (hq q 2)
[Fact (Nat.Pr p}] [Fact (Nat.Prime qi]
[llegnndre_s Legendre syn -1 ((p-1)
17
exact book. quakaquad rec reciprocity wwrrocity.quddratee quadratic recipracity p hp
Notably, the proof of the first theorem premises, and the proof of the second uses simple statement of quadratic reciprocity. However, by the end of the lifelong learning process, LeanAgent exhibits growth in its proving abilities in this repository:
a) Advanced Abstract Algebra: LeanAgent shows advancement in proving key result in abstract algebra, wedderbura (Wedderburn's Little Theorem), which is erucial result in abstract algebra, stating that every finite division ring is field.
theorem wedderburn (h: Fintype R): IsField R :- by apply Field. toIsField
LeanAgent's proof of the wedderburn theorem represents the ability handle algebraic struc- tures. By using the Field. toTsFiel eld premise, LeanAgent shows that it has grasped how to use the knowledge of what makes ring field. This requires an understanding of ring theory and field properties.
Coxeter. LeanAgent could not prove sorry theorems from the Coxeter repository during lifelong learning. However, by the end of lifelong learning, LeanAgent demonstrates growing under- standing of more complex algebraic structures, proving the lemma invmap. of_eg about Coxeter systems, again showing the ability to work with advanced concepts in group theory and abstract algebra. This corroborates the handling of abstract algebra necessary to prove the wedderburn theorem.
36

---

Published as a conference paper at ICLR 2025
Lenma 'nvmmap of_ (S:Set G} [CoxeterSysten G 5] (s :5) : invmap 5 im by
simp [CoxeterSysten. teaetersysten.Preseenatttu
invmap]
unfold CoxeterSystem. toNatrix
apply CoxeterSysten. mono idL ift.tttt. mapl. ift.of
LeanAgent's proof of invaap. of eq involves unfolding definitions and applying specific proper- ties of Coxeter systems. This demonstrates LeanAgent's growing understanding relative to ReProver abstract algebra specific to the new repository has learned from.
Hairy Ball Theorem. Moreover, LeanAgent could not prove sorry theorems from the Hairy Ball Theorem repository during lifelong learning. However, the end lifelong learning, LeanAgent again demonstrates stronger understanding relative ReProver in algebraic topology. It proves HairyBal ByBialiiff,,, which states a key step in the Hairy Ball Theorem, demonstrating a grasp of vector spaces, norms, and their connections topological concepts.
theorem HairyBallDiff use FW [- norm_eq_zerre zero]
FW [vUnit, norn_ norn_zero]
Crucially, only LeanAgent could prove invmap of_eq, wedde rburn, and HairyBallDifg demonstrating that has developed much more advanced theorem theorem-proving capabilities than other setups. These proofs show that LeanAgent work with highly abstract concepts and apply them to specific mathematical objects.
A.6 CURRICULUM LEARNING ANALYSIS
In this section, aim number of proof steps) as its complexity metric? (2) Why does curriculum learning work in theo- rem proving? (3) Why does LeanAgent use curriculum learning instead of other lifelong learning methods?
the following questions: (1) Why does LeanAgent e (S
Complexity Measure. There is universal measure proof complexity in Lean or other formal systems. One approach, the congth-based measure, involves examining the proof length (number of steps or lines) and the size of the proof term in formal system. While these can indicate verification complexity, they may not fully capture the complexity of discovering proof (Arana & Stafford, 2023]. Moreover, within the NL.P literature, many works have related input length complexity
Zaremba & Sutskever] 2015 Cirik et al.) 2016 Spitkovsky et al. (Sbrramnnian et al. [2077] Chang ct al. 2021), Starting with shorter sequences and gradually increasing length improves model quality (Li 2024).
These works demonstrate the gains from basing the complexity measure on input length. As such, consider the equivalent of length in theorem proving to be the number of proof steps. However, we consider a linear scaling of length naive for theorem proving: it doesn't 't consider the combina- torial explosion of possible proof paths as the length of the proof increases. As such, choose
37

---

Published as a conference paper at ICLR 2025
exponential scaling. Notably, key strength of this choice is it is easy to compute and requires additional hyperparameters to tune.
We now discuss some alternative complexity metrics and why we chose not to use them in Lean- Agent. One option is e where B represents the number of different proof paths that could be explored at each step. Formally, B is defined as the average number of child nodes for each non-leaf node in the proof tree. This is sometimes called the branching factor. We refrain from using this com- plexity metrie as computing this becomes computationally expensive for complex proofs. Moreover, another option is to consider the complexity of the theorem statement to determine complexity. For example, this could be measured by the number of unique symbols, the depth of nested expressions, or the number of quantifiers. However, developing reliable metric for statement complexity that works across various mathematical domains could he challenging. Moreover, LeanAgent focuses on improving proof generation, so using a metric directly related to the proof process (number of steps) aligns better with this goal than statement complexity. Dependency-bai we order theorems based on their dependency structure within the mathematical library, wasn't I used for multiple reasons. Namely, a theorem might depend on many simple results but still be relatively easy prove, it might depend on few results but be very challenging. Furthermore, a topic- based curriculum would be unsuitable because LeanAgent aims to be a general-purpose framework. A topic-based approach might bias it towards certain mathematical domains. Moreover, a topic- based approach does not account for theorems spanning multiple mathematical concepts. Another option is a form of premise-based complexity measure. However, analyzing premise occurrence frequencies across repositories could be computationally expensive, especially for large repositories like SciLean.
complexity, where
Curriculum Learning. Prior work suggests that curriculum learning guides the learner towards better local minima in non-convex optimization problems (Bengio et al. 2009). Crucially, theorem proving involves navigating a highly non-convex optimization landscape, especially for complex mathematical statements. The space of possible proofs is vast and complex, with many potential dead ends and suboptimal solutions to parts of proof. This makes theorem proving an ideal can- didate for benefitting from curriculum learning. Moreover, curriculum learning has been shown to have effect similar to unsupervised pre-training, acting as a form of regularization (Bengio et al. 2009). For theorem proving, curriculum learning allows LeanAgent to build a foundational knowledge base of mathematics before attempting more complex theorems, naturally leading to continuous improvement. This avoids suboptimal proof strategies early in training. Furthermore, this leads to more robust and generalizable proof techniques that work across broader range of theorems, explaining LeanAgent's sorry theorem proving performance. Moreover, the ability to act as a regularizer means curriculum learning prevents the model from overfitting to specific types of proofs or mathematical domains. This allows for continuous generalizability, explaining LeanA- gent's 's superior lifelong learning metric scores.
Moreover, other works from the literature show that curriculum learning biases models towards building constructive internal representations (Cirik et al.) 2016). Specifically, it allows the model to use the knowledge from earlier steps in later predictions. In theorem proving, this allows Lean- Agent to learn basic proof skills, which then become building blocks for more complex proofs later on. This corroborates our analysis of LeanAgent's 's progression of proof complexity. Moreover, mul- tiple past works agree that curriculum learning provides larger gains when training data is limited (Zaremba & Sutskever] 2015 Cirik et al., 2016 SSpikkossyy et al.). This is the case in formal theorem proving, where the number of formalized theorems and proots is limited. These past works also state that curriculum learning leads to better generalization, supporting the observations of LeanAgent's superior lifelong learning metrics.
This context supports LeanAgent's sorry theorem proving performance and superiority on lifelong learning metrics.
Comparison with Other Lifelong Learning Methods. Many other lifelong learning methods ist, such as those mentioned in Sec. 2 However, we chose curriculum learning for the following reasons. Regularization methods, like EWC, slow down learning on important parameters. How- ever, the importance of parameters can change as the theorem complexity increases. This helps explain the lower sorry theorem proving performance of EWC methods and their performance on lifelong learning metrics. Moreover, memory- based techniques store examples from previous tasks to prevent forgetting. However, this can greatly affect these methods balance of stability and plas-
38

---

Published as a conference paper at ICLR 2025
ticity. This can be seen in the lifelong learning metrics of Merge All setups, including the negative IP values. Knowledge distillation requires a separate teacher model, but curriculum learning is more efficient as it provides the path to knowledge accumulation in a single model. Since LeanAgent is framework, not a model, we refrain from using dynamic architecture adjustment to keep LeanAgent general many LLM architectures. Moreover, recent work selectively updates parameters with the largest momentum magnitudes and uses selective reinitialization to maintain plasticity. How- ever, these methods often focus on balancing performance across distinct tasks. In theorem proving, where tasks form spectrum of increasing complexity, curriculum learning provides a more struc- tured approach to knowledge accumulation.
A.7 THEOREM PROVING PERFORMANCE SCORE (TPPS) ANALYSIS
In this work, we directly compared the number of proven theorems with ReProver. However, the field of theorem proving, especially in lifelong learning context, currently lacks standardized per- formance metrics. To address this concern, this section discusses possible alternative metric while acknowledging its limitations.
Theorem proving difficulty is inherently non-linear in nature. For example, LeanAgent's significantly improved performance over the baseline across multiple repositories allows to prove progressively harder theorems. Furthermore, sorry theorems lack ground truth proofs, so proving one is valuable. To address these nuances, one could propose the Theorem Proving Performance Score (TPPS) to emphasize newly proven sorry theorems. Specifically, could be stated that LeanAgent TPPS = (# ReProver Theorems Proved) + (# New Theorems Proved X) + 1, where X represents the importance of proving new theo- rem, and ReProver TPPS = (# ReProver Theorems Proved) + 1. Then, Improvement Factor = (LeanAgent TPPS)/
TPPS).
The core idea behind TPPS is to assign higher reward for newly proven theorems, aligning with lifelong learning objectives. However, it is important to recognize its preliminary nature and po- tential shortcomings. First, choosing the parameter X is challenging. One approach is to choose static value, such as = 10, to standardize comparisons between LeanAgent and ReProver across diverse repositories. However, this may lead to inflated or deflated metrics on such repositories. Alternatively, could be chosen adaptively based on the difficulty of a repository, but this may similarly result in unrealistic metric scores. Overall, the TPPS metric focuses quantity and faces challenges in ensuring comparisons across diverse repositories.
Moreover, the TPPS metric can be susceptible to artifacts that artificially inflate performance. For instance, several theorems in the PFR repository were proven on a technicality due to placeholder statements of "0 1", which could then be used prove other "sorry" theorems through the principle of ex falso quodlibet. Examples such as this are due to the weakness of the current state of repositories rather than a fundamental shortcoming of our ML approach, underscoring the need for more robust and well-tested benchmarks.
Furthermore, TPPS does not account for the difficulty of the theorems being proved. While we ini- tially considered using proof length as proxy for difficulty (c.g., e where S is the number of proof steps), we found this approach problematic during proving evaluation. LeanAgent sometimes gen- crates shorter proof's for difficult theorems, making proof length an unreliable indicator of theorem difficulty.
These issues expose broader challenges in evaluating axcorem-proving systems. The field lacks standardized benchmarks, necessitating carefully curated sets of theorems with varying difficulties across different mathematical domains. Developing reliable metrics to assess theorem difficulty beyond simple measures like proof length or statement complexity is crucial. Future benchmarks should prevent the cxploitation of technicalities. Moreover, metrics should consider the mathemat- ical significance of proven thcorems, not just their quantity. Finally, ensuring that performance metrics are meaningful and comparable across different mathematical repositories is essential for consistent evaluation.
In light of these considerations, we acknowledge that TPPS, while step towards quantifying theorem-provine performance in a lifelong learning setting, has many limitations. Future work should focus on developing more sophisticated and robust evaluation frameworks that address these
39

---

Published as a conference paper at ICLR 2025
challenges. For example, plan to investigate more sophisticated measures that reward not only newly proved theorems but also difficult ones. By highlighting these issues, we hope to contribute to the ongoing discussion how best to evaluate and compare setorem-proving systems, particularly in the context of lifelong learning. The development standardized, reliable metrics will be crucial for measuring progress and guiding future research in this field.
40


Reviews:
[{"review_id": "rDV09KpQvZ", "reviewer": "Reviewer_SgJW", "summary": "The paper presents LeanAgent, a framework that aims to improve automated theorem proving through lifelong learning across multiple mathematical domains. The key contributions include a curriculum learning strategy, progressive training of retrieval models, and management of evolving mathematical knowledge. The paper claims significant improvements over baselines, particularly in proving \"sorry\" theorems previously unproved by humans.", "questions": "1. Could you provide separate statistics for theorems proved during vs after lifelong learning?\n2. Why not update both retriever and tactic generator during training?\n3. Have you compared to simple pre-training on all available data?\n4. How do you ensure reported improvements aren't just from running multiple model checkpoints?\n5. What are the key computational requirements for practical deployment?", "limitations": "", "rating": 6, "confidence": 2, "soundness": 2, "presentation": 2, "contribution": 2, "strengths": "- LeanAgent introduces an interesting approach to adapting theorem provers across evolving repositories. And it uses curriculum learning strategy provides a systematic way to handle increasing mathematical complexity and demonstrates potential for improving retrieval models through continuous training\n- This paper provides a framework that could be practically useful for filling in \"sorry\" theorems and it demonstrates ability to work across diverse mathematical repositories, shows promise for developing maintainable theorem provers that can adapt to changes-\n- This paper has detailed ablation studies examining different components", "weaknesses": "# Evaluation Methodology Concerns\n- TPPS metric (with 10x multiplier) may artificially inflate improvements over baseline\n- Unclear separation between \"during\" vs \"after\" lifelong learning results\n- Combined statistics from multiple 10-minute runs may give unfair advantage over baselines\n# Results Reproducibility Issues\n- Some reported baseline numbers appear inconsistent with other evaluations (ReProver's results)\n- Need clearer accounting of which theorems are proved and how\n# Technical Limitations\n- Only updates retriever model, not tactic generator\n- Unclear why curriculum learning is necessary vs training on all data\n- Long training times (4-9 days) may limit practical applicability", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "ojWDJK6BjW", "reviewer": "Reviewer_5WDb", "summary": "This paper proposes LeanAgent, a lifelong learning framework for formal theorem proving in Lean. LeanAgent alleviates the catastrophic forgetting issue in life-long learning of formal language provers via retrieval-augmented generation, with progressive training on the retriever.\n\nFour main techniques are adopted to reduce the difficulty of training or proof search, including\n  * **Curriculum learning** based on quantifiable complexity measured by the number of reasoning steps, allowing the model to learn from easy to difficult repositories\n  * **Dynamic database management** that manages existing proofs and incorporates new proof steps generated by LeanAgent\n  * **Progressive training** which limits the number of epochs to 1 to improve stability for mitigating forgetting, and choose the iteration with the highest validation recall on top-10 retrieved premises to improve the plasticity of absorbing new information.\n  * **_sorry_ Theorem proving** via best-first search, similar to Dijkstra's algorithm in the graph, where each node/state is an incomplete proof, each edge is a proof step, and the path length is measured by the negative log-likelihood.\n\nExperiments are conducted on two aspects, 1) comparing the quantity and quality of newly discovered proofs, and 2) ablation over different setups to further strike a balance between stability and plasticity. The main result shows that LeanAgent significantly outperforms ReProver and discovers 162 new theorems across 23 Lean repositories.", "questions": "* I am wondering if the code will be released, and when it is expected to be released.\n* I am wondering if it is possible to report the miniF2F success rate of the proposed method, given this is the conventional benchmark for Lean-based methods.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 4, "strengths": "The main strength of the paper is its significance, especially for the Math community. A method capable of automatically discovering new theorems/proofs can lead to powerful tools to accelerate the development of mathematics and expedite relevant scientific fields such as physics and machine learning.\n\nAlthough each proposed technique alone is not novel, showing the effectiveness of the combined systems is non-trivial, demonstrating the novelty of the proposed methods.", "weaknesses": "The main concern centers around its quality. The provided demos are impressive and great, but the code availability and adopted benchmarks are questionable, specifically,\n\n  * **Code availability**: for LeanAgent to be truly accessible for mathematicians, the code and corresponding inference pipeline are necessary. I am wondering if the authors intend to release the code soon.\n  * **Adopted benchmarks**: a standard metric for evaluating Lean-based systems is the success rate on the miniF2F test set. I am wondering if the authors can provide the number, along with comparisons to baselines other than retrieval-based methods. Just including the reported success rates in the previous literature would be fine, e.g. [1][2][3][4][5].\n\nOther detailed comments are listed as follows,\n  - [Clarity] lines 262-263, typo: \"We sorry theorem theorem proving performance between...\" -> \"We compare sorry theorem proving performance between...\"\n  - [Clarity] lines 373-374: terms like \"masters\" may not be sufficiently rigorous and objective. It would be recommended to provide some numbers to improve the objectivity of the statement.\n  - [Clarity] lines 366-387: Better provide redirections to the corresponding section in the Appendix, e.g. line 2050 of HairyBallDiff. This improves the objectivity of the paper.\n  - [Clarity] line 437, Table 4: it is recommended to add up/down arrows in metrics to indicate whether the lower or higher values are better\n  - [Clarity] Appendix section A.5: the figures for different theorems can be rescaled to make the fonts similar in size.\n  - [Quality] lines 316, 430-431: several metrics adopted in the paper are computed based on heuristics, where further justification is encouraged to be added. For example, under the proposed metrics, the rank order of modern LLMs, o_1 > GPT-4o> ChatGPT, would provide evidence that the chosen coefficient is proper.\n\nI am considering raising my score if those concerns can be properly addressed in the rebuttal.\n\n### Reference\n\n[1]: Jiang, Albert Qiaochu, et al. \"Thor: Wielding hammers to integrate language models and automated theorem provers.\" Advances in Neural Information Processing Systems 35 (2022): 8360-8373.\n\n[2]: Jiang, Albert Q., et al. \"Draft, sketch, and prove: Guiding formal theorem provers with informal proofs.\" arXiv preprint arXiv:2210.12283 (2022).\n\n[3]: Zhao, Xueliang, Wenda Li, and Lingpeng Kong. \"Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving.\" arXiv preprint arXiv:2305.16366 (2023).\n\n[4]: Wang, Ruida, et al. \"Theoremllama: Transforming general-purpose llms into lean4 experts.\" arXiv preprint arXiv:2407.03203 (2024).\n\n[5]: Xin, Huajian, et al. \"DeepSeek-Prover-V1. 5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search.\" arXiv preprint arXiv:2408.08152 (2024).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "2Z5CGvRUnm", "reviewer": "Reviewer_563Q", "summary": "The paper introduces LeanAgent, a framework that augments LLM-guided formal theorem proving with lifelong learning and retrieval from a dynamic database. Evaluations on several real-world Lean GitHub repos and miniF2F demonstrate the advantage of the framework over a baseline with only retrieval from a static database (ReProver).", "questions": "(Questions 1-3 are about typos and wording issues)\n1. Line 262: Missing word in “We sorry theorem proving performance…”?\n2. Lines 227-228: “Before validation, we precompute embeddings for all premises in the corpus to ensure these embeddings are consistent with LeanAgent’s current state.” What does this mean?\n3. Lines 318-324: Not sure what “formalize” means here, since if I understood the paper correctly, LeanAgent doesn’t do auto-formalization and MiniF2F is not an auto-formalization benchmark. It is also unclear to me what “in parallel” in line 323 means.\n4. It would help the reader to show some basic statistics about each repo, namely, the number of sorry theorems in each repo, the number/percentage proven by LeanAgent, and the number/percentage proven by ReProver. Some statistics regarding the dynamic database would also help, such as the number of theorems/premises from each repo and their breakdown into difficulty categories.\n5. (Related to the TPPS metric) It would be helpful to see a more informative metric than the TPPS metric (see criticisms above). For example, it would be ideal to have difficulty estimates for all the “sorry” theorems (based on e.g. ground truth proof length), and then for each repo, show (with e.g. a histogram) for each difficulty category, how many “sorry” theorems there are, how many were proven by ReProver, and how many by LeanAgent.\n6. How is it ensured that the proofs do not involve circular reasoning? In other words, how did you make sure you’re not proving a sorry theorem A using another sorry theorem B while using sorry theorem A in the proof of sorry theorem B? (The Alternate PFR Commit case study on pages 30-31 seem to suggest that circular reasoning did occur, using 0 = 1 placeholder theorems to prove other 0 = 1 placeholder theorems.)\n7. The coefficients in the definition of the Composite Score obtained (lines 429-431) seem arbitrary – how were they determined? How sensitive are the results to these coefficients?", "limitations": "", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "1. Demonstrates the utility of curriculum learning with retrieval from a dynamic database in the application of neural-guided formal theorem proving.\n2. Evaluation on real-world repos shows real-world applicability of the framework (although this also has caveats – see Weakness 5 below).", "weaknesses": "1. The way the abstract describes the results is very misleading. For example, “LeanAgent successfully proves 162 theorems previously unproved by humans” is understood to mean that LeanAgent solved 162 unsolved problems in math, whereas in reality many of these just happened to not have their proofs filled in because the authors of the repositories hadn’t gotten to them yet, or the proofs are intentionally left blank because they are exercises from Lean tutorials/textbooks. For example, there are 0 = 1 placeholder theorems and theorems that simply involve expanding definitions (thus proven by just “refl”). The main metric of comparison with the baseline is also misleading, where the “11x” improvement actually refers to 3 repos where ReProver proved nothing and LeanAgent proved 1 theorem – see my next point.\n2. The metric of comparison with the baseline (“TPPS”) appears to be designed to inflate the result of LeanAgent. The metric’s definition depends on the model/framework – already not a good sign. For LeanAgent it is (# ReProver Theorems Proved) + 10 * (# New Theorems Proved) + 1, and for the baseline ReProver it is (# ReProver Theorems Proved) + 1. Notably, the metric for LeanAgent is defined as the metric for the baseline plus a non-negative number, so by the very definition of the metric it is impossible for LeanAgent to perform worse than the baseline. Furthermore, the extra factor of 10 in the definition of the metric for LeanAgent (that doesn’t appear in the definition of the metric for the baseline) appears arbitrary and requires more justification than just saying it is “relatively modest considering the large difficulty gap between basic arithmetic and abstract algebra”.\n3. The paper only showed results of the LeanAgent framework with the ReProver retriever and tactic generator. The paper would be stronger if it also showed consistent improvements from LeanAgent applied on top of well-known math LLMs such as Llemma and DeepSeek-Prover and/or other search strategies such as Hypertree Proof Search.\n4. While the paper frequently emphasizes its curriculum learning strategy, it does not appear to make a technical contribution in this regard (simple rule of training for 1 epoch on each successive repository) and its application to formal math has already been explored (see, e.g., https://arxiv.org/abs/2202.01344).\n5. The evaluation datasets (with the exception of miniF2F) appear to be various Lean GitHub repos with no guarantee of cleanliness. Indeed, the authors point out themselves that one of the repos has several “0 = 1” placeholder “sorry” theorems. Even among actual “sorry” theorems, there’s significant variation in difficulty, e.g., there are some proven by just “refl” and others that are more involved. This makes it more difficult to contextualize and interpret the results. (See also question 5 below for a suggestion to possibly improve this.)\n6. In terms of presentation, there’s a decent amount of repetition (e.g. curriculum learning was explained an excessive number of times)", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "YGNaxAQpW9", "reviewer": "Reviewer_W5az", "summary": "This paper studies the topic of automated theorem proving in Lean language. It primarily builds on the method proposed by LeanDojo and considers the problem that a trained LLM may consider catastrophic forgetting when it is fine tuned on a new dataset. To address this issue, it suggests that LLMs should be trained for lifelong learning, where they learn new material after being fine-tuned without forgetting what they had learned before. It then considers several Lean repositories and tries to prove the unsolved theorems in those repositories. It reports vaguely some successes in solving some of the theorems.", "questions": "Please see weaknesses.", "limitations": "", "rating": 6, "confidence": 5, "soundness": 2, "presentation": 2, "contribution": 2, "strengths": "The topic is very interesting and the experiments are on a diverse set of problems and repositories.\n\nLiterature review considers both the ML literature and math literature.", "weaknesses": "I found the presentation of results very disorganized and rather unusual in the context of the ML literature. Overall, the presentation seems to be a stream of consciousness.\n\nI try to view the contribution from different perspectives, and I explain the shortcomings from each perspective.\n\n1. The task of automated theorem proving: \n\n    1.a. I tried for some time to find out what is the achieved accuracy of the proposed system on the miniF2F validation and test sets. I was shocked to see in the main body of the paper, in Tables 1 and 2, the paper provides the number of theorems in the datasets that it has proved without giving the total number of theorems nor the accuracy. I was expecting these tables to provide the accuracy of the proposed model on each of the datasets. I was only able to find somewhere deep in the appendix that the paper has been able to prove 99 theorems from the miniF2F dataset (not clear whether it is for the test set or valid set) which translates to accuracy of about 40%. It is as if the paper is trying to hide the accuracy on the known benchmark miniF2F.\n\n    1.b. The accuracy of 40% on miniF2F does not appear to be an improvement in the recent literature. For example, the accuracy of Hypertree Proof Search from 2022 is 41% on the miniF2F.\n\n    1.c. Table 2 does not show how many sorry theorems exists in each repository. For the Coxeter, I believe there are hundreds of sorrys, but paper only indicates the numbers 1 and 11, the number of sorry's it has been able to address without mentioning how many sorry have remained unproved. Table 2 has large margins of empty space, so I don't see why those numbers are not provided.\n\n    1.d. Paper does not mention how many of those sorrys can be proved using native methods in Lean such as apply?, hint, or exact?. \n\n     1.e. Many of the statements in the paper seem imprecise and perhaps trying to exaggerate the contributions of the paper. For example, the paper claims: “For the Coxeter repository, LeanAgent proves a complex lemma about Coxeter systems, showcasing its proficiency in group theory.” While the paper claims “proficiency” of its model in group theory, it is useful to note that its proof only has three lines of code, and the model fails to prove all other theorems in that repository. So the claim of “proficiency in group theory” seems overblown and unjustified.\n\n2. Lifelong learning: \n    \n    2.a. The paper does not establish how its LLM suffers from the issue of forgetting when it comes to ATP. It seems that the paper has struggled with this, and has tried to find the best setting for training the LLM on multiple datasets in sequence, but it is not clear what the baseline was, what kind of accuracy was obtained, how the LLM was suffering from forgetting, and how the issue can be addressed. \n\n    2.b. The paper keeps talking about the trade-offs between the stability and plasticity, but these two terms remain undefined and unquantified.\n\n    2.c. It seems that, ultimately, paper has just performed trials and errors to eventually find the setting that yields the highest accuracy. Is that the case? I hope authors can clarify this, and explain their exact contribution. Is the contribution a method on how to train LLMs on multiple datasets while avoiding the issue of catastrophic forgetting, or is their contribution just an improvement on the task of ATP? If the former is the case, it would make sense to formalize the method, perform ablation studies, and demonstrate the generalization ability of the method. By ablation study, I mean reporting the accuracies in each configuration of lifelong learning and on each of the datasets. By accuracy for each dataset, I mean the number of proved theorems divided by the total number of theorems in a dataset.\n\n\nSome other comments\n\nThe discussion about lifelong learning, and the claims about how mathematicians work seems like an incoherent opinion piece without much evidence, and not even necessary for the experiments of the paper.\n\nThe claim that “mathematicians often formalize across multiple domains and projects simultaneously or cyclically”, and giving Terry Tao as an example, seems a bit out of context. Terry Tao is famous for his unusual ability to work on multiple domains. Overall, I think the paper makes claims that are not even necessary. Paper can simply review the list of problems in miniF2F that it has failed to prove, perhaps showcase one of the more easier problems that it has not been able to prove, and be more grounded in reality when claiming “proficiency” in topics such as group theory.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)