# LeanAgent: Lifelong Learning for Formal Theorem Proving
**Authors**:
- Chaowei Xiao, Anima Anandkumar (California Institute of Technology, Stanford University, University of Wisconsin, Madison)
> Equal contribution.
## 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.
## 1 Introduction
Mathematics can be expressed in informal and formal languages. Informal mathematics utilizes natural language and intuitive reasoning, whereas formal mathematics employs symbolic logic to construct machine-verifiable proofs (Kevin Buzzard, 2019). State-of-the-art large language models (LLMs), such as o1 (OpenAI, 2024) and Claude (Claude Team, 2024), produce incorrect informal proofs (Zhou et al., 2024). This highlights the importance of formal mathematics in ensuring proof correctness and reliability. Interactive theorem provers (ITPs), such as Lean (De Moura et al., 2015), have emerged as tools for formalizing and verifying mathematical proofs. However, constructing formal proofs using ITPs is complex and time-consuming; it requires extremely detailed proof steps and involves working with extensive mathematical libraries.
Recent research has explored using LLMs to generate proof steps or complete proofs. For example, LeanDojo (Yang et al., 2023) introduced the first open-source framework to spur such research. Existing approaches typically involve training or fine-tuning LLMs on a specific dataset (Jiang et al., 2022). However, data scarcity in formal theorem proving (Polu et al., 2022) hinders the generalizability of these approaches (Liu et al., 2023). For example, ReProver, the retrieval-augmented LLM from the LeanDojo family, uses a retriever fine-tuned on Lean’s math library, mathlib4 (mathlib4 Community, 2024). Although mathlib4 contains over 100,000 formalized mathematical 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 (Tao et al., 2024).
<details>
<summary>extracted/6256159/Final2.png Details</summary>
### Visual Description
## System Architecture Diagram: LeanAgent - Automated Theorem Proving Pipeline
### Overview
This image is a technical system architecture diagram illustrating a multi-stage pipeline for automated theorem proving, specifically within the Lean formal proof assistant ecosystem. The diagram is divided into three primary, nested functional blocks that describe a continuous learning and data processing loop. The overall flow depicts how data is extracted from repositories, processed through curriculum learning and progressive training, and used to prove previously unproven ("sorry") theorems, with the results feeding back into a dynamic database.
### Components/Axes
The diagram is structured into three main rounded rectangular containers, each representing a major subsystem or process:
1. **Top Container (LeanAgent Core Loop):**
* **Input:** "GitHub Repositories" (represented by a folder icon).
* **Process Flow:** "Extract Data Per Repository" → A data box containing "theorem + proof" entries (in blue text) → "LeanAgent" → "Curriculum Learning" → "Dynamic Database" (represented by a cylinder icon).
* **Feedback Loop:** A large arrow labeled "Repeat For Each Repository" encloses a secondary process: A repository icon → "Premise Corpus" and "Theorems + Proofs" → "Progressive Training" → "*sorry* Theorem Proving" → which feeds back into the "Dynamic Database".
2. **Middle Container (Curriculum Learning Subsystem):**
* **Input Graph:** A small line graph with Y-axis "Complexity" and X-axis "# Proof Steps", showing a positive correlation.
* **Process Flow:** "Theorem Complexities" → A data box with example values: "complexity: 2.7", "complexity: 7.4" (in blue text) → A bell curve distribution labeled "Easy Medium Hard" on its X-axis → A set of three stacked, colored blocks (green, yellow, red) with an arrow pointing to the label "Descending # Easy Theorems".
3. **Bottom Container (Progressive Training & Proving Subsystems):**
* **Progressive Training Sub-block:**
* "Latest Retriever" (represented by a small rectangle) → "Limited Exposure" with a box labeled "1 epoch" → "Balanced Training" (represented by a bar chart icon comparing "Stability" and "Plasticity") → "New Retriever".
* **sorry Theorem Proving Sub-block:**
* "*sorry* Theorems" → "Retrieved Premises w/ Updated Retriever" (a data box containing "theorem", "lemma" in blue text) + "Generated Tactics" (a data box containing "apply premise" in blue text) + "Best-First Tree Search" (represented by a tree search icon) → "New Proofs".
### Detailed Analysis
* **Data Flow & Iteration:** The system is fundamentally iterative. It processes one GitHub repository at a time ("Repeat For Each Repository"), extracting formal mathematical theorems and their proofs. This data is used to train and update the system, which then attempts to prove new theorems. The results ("New Proofs") are stored in a "Dynamic Database," which presumably informs future training cycles.
* **Curriculum Learning Mechanism:** This component organizes training data by difficulty. Theorems are assigned a complexity score (e.g., 2.7, 7.4) likely based on the number of proof steps. They are then categorized into a distribution (Easy, Medium, Hard). The training strategy involves presenting theorems in "Descending # Easy Theorems," suggesting a schedule that starts with many easy problems and gradually introduces harder ones.
* **Progressive Training Mechanism:** This focuses on updating a "Retriver" model (likely a component that finds relevant premises/lemmas). It uses "Limited Exposure" (1 epoch) to prevent catastrophic forgetting, followed by "Balanced Training" to manage the trade-off between "Stability" (retaining old knowledge) and "Plasticity" (learning new information).
* **Theorem Proving Engine:** The "*sorry* Theorem Proving" module takes theorems that are incomplete (marked with `sorry` in Lean). It uses the updated retriever to find relevant premises, generates potential proof tactics (e.g., `apply premise`), and employs a "Best-First Tree Search" algorithm to explore the proof space and generate "New Proofs."
### Key Observations
* **Closed-Loop System:** The architecture is a closed feedback loop where outputs (new proofs) become inputs for future learning, enabling continuous improvement.
* **Explicit Handling of Complexity:** The system doesn't treat all theorems equally. It explicitly measures complexity and structures learning accordingly (Curriculum Learning).
* **Focus on Incremental Updates:** The "Progressive Training" block highlights a concern for efficiently updating the AI model without retraining from scratch, emphasizing stability-plasticity balance.
* **Integration of Symbolic and Neural Methods:** The pipeline combines neural/retrieval components ("Retriever," "Generated Tactics") with classical symbolic AI search ("Best-First Tree Search").
### Interpretation
This diagram outlines a sophisticated, autonomous AI system designed to advance the state of automated mathematical reasoning. The core innovation appears to be the integration of three key machine learning paradigms into a single, continuous pipeline:
1. **Self-Improvement via Data Flywheel:** By mining public code repositories (GitHub), the system bootstraps its own training data, creating a virtuous cycle where more data leads to better proving, which in turn generates more data (new proofs).
2. **Pedagogically-Structured Learning:** The "Curriculum Learning" module mimics human education, suggesting that organizing training data from simple to complex is crucial for efficient learning in formal domains. This likely helps the model build foundational knowledge before tackling advanced concepts.
3. **Efficient Lifelong Learning:** The "Progressive Training" module addresses a key challenge in AI: updating a model with new information without forgetting old knowledge. This is essential for a system that must continuously learn from an ever-growing database of theorems.
The ultimate goal is to reduce the need for human-written proofs (the `sorry` placeholders) by having the AI agent autonomously discover and formalize proofs. This has significant implications for formal verification, mathematical research, and the development of more reliable software systems. The architecture suggests a move away from static, one-time trained models towards dynamic, self-improving agents that operate continuously on live data sources.
</details>
Figure 1: LeanAgent overview. LeanAgent searches for Lean repositories and uses LeanDojo to extract theorems and proofs. It uses curriculum learning, computing theorem complexity as $e^{S}$ ( $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 a retrieval-based framework, LeanAgent generates a dataset (premise corpus and a collection of theorems and proofs) for each repository in the curriculum and progressively trains its retriever. Progressive training happens over one epoch to prevent forgetting old knowledge. Then, LeanAgent uses the updated retriever in a search-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.
The dynamic nature of mathematical research exacerbates this generalizability issue. Mathematicians often formalize across multiple domains and projects simultaneously or cyclically. For example, Terence Tao has worked on various projects in parallel, including formalizations of the PFR Conjecture, symmetric mean of real numbers, classical Newton inequality, and asymptotic analysis (Tao, ; Tao, 2024a; Tao et 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-proving 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 learning, i.e. learning multiple tasks without forgetting (Wang et al., 2024b). A significant challenge is catastrophic forgetting: when adaptation to new distributions leads to a loss of understanding of old ones (Jiang et al., 2024). The core challenge is balancing plasticity (the ability to learn and adapt) with stability (the ability to retain existing knowledge) (Wang et al., 2024b). Increasing plasticity to learn new tasks efficiently can lead to overwriting previously learned information. However, enhancing stability to preserve old knowledge may impair the model’s ability to acquire new skills (van de Ven et al., 2024). Achieving the right balance is key to continuous generalizability in theorem proving.
LeanAgent. We present LeanAgent, a novel lifelong learning framework for theorem proving. As shown in Figure 1, LeanAgent’s workflow consists of (1) deriving complexity measures of theorems to compute a 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 LLM; we implement it with retrieval for improved generalizability (Yang et al., 2023).
We employ a simple progressive training method to avoid catastrophic forgetting. Progressive training allows LeanAgent to continuously adapt to new mathematical knowledge while preserving previously learned information. This process involves incrementally 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, gradually expanding LeanAgent’s knowledge base. This approach increases the space of possible proof states (where a 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., 2017), which uses the Fisher Information Matrix to constrain important weights for previous tasks, result in excessive plasticity. The uncontrolled plasticity 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 7 theorems using exploits found within Lean’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 continuous generalizability to new repositories. Backward transfer (BWT), where learning new tasks improves performance on 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 simple components of curriculum learning and progressive training improve stability and BWT scores substantially, emphasizing its continuous generalizability and improvement and explaining its superior sorry theorem proving performance.
## 2 Preliminaries
Neural Theorem Proving. The current state-of-the-art of learning-based provers employs Transformer-based (Vaswani et al., 2017) LLMs that process expressions as plain text strings (Azerbayev et al., 2024; Xin et al., 2024b; Shao et al., 2024). In addition, researchers have explored complementary aspects like proof search algorithms (Lample et al., ; Wang et al., 2023). Moreover, other works break the theorem-proving 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 (Irving 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 as input to symbolic provers (Alama et al., 2014; Mikuła et al., 2024).
Retrieval-Augmented LLMs. While retrieval-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 new. However, relevant architectures have been researched in natural language processing (NLP) (Lu et al., 2024; Borgeaud et al., 2022; Thakur et al., 2024).
Lifelong Learning. Lifelong learning addresses catastrophic forgetting in sequential task learning (Chen et al., 2024). Approaches include regularization methods (Kirkpatrick et al., 2017), memory-based techniques (Lopez-Paz & Ranzato, 2017; Chaudhry et al., 2019; Shin et al., 2017), and knowledge distillation (Li & Hoiem, 2017; Kim et al., 2023). Other strategies involve dynamic architecture adjustment (Mendez & Eaton, 2021) and recent work on gradient manipulation and selective 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 a curriculum of statements of increasing difficulty (Polu et al., 2022). For reinforcement learning, an 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) 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.1 and a discussion of why curriculum learning works in theorem proving is available in Appendix 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 to 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-grained information about their theorems, proofs, and dependencies. Then, we calculate the complexity of each theorem using $e^{S}$ , where $S$ represents the number of 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 Appendix A.6.
We compute the 33rd and 67th percentiles of complexity across all theorems in all repositories. Using these percentiles, we 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 LeanAgent extracted. This way, we can keep track of and interact with the knowledge that LeanAgent is aware of and the proofs it 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 a future curriculum. Details of the database’s contents and features can be found in Appendix A.1.
For each repository in the curriculum, LeanAgent uses the dynamic database to generate a dataset by following the same procedure used to make LeanDojo Benchmark 4 (details in Appendix A.1). This dataset includes a 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 of a theorem’s hypotheses and the current progress in proving the theorem. As such, this pairing of theorems and proofs demonstrates how to use specific tactics (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 allows 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 a specific implementation here. We start with ReProver’s retriever, a fine-tuned version of the ByT5 encoder (Xue et al., 2022), leveraging its general pre-trained knowledge from mathlib4. We train LeanAgent on the new dataset for an 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 in the corpus generated by LeanAgent’s current state to ensure that we properly evaluate LeanAgent’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, we 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 to explore more diverse paths to prove theorems, discovering new proofs that it 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 at 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 as a context 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 to the proof search tree. We choose the tactic with the maximum cumulative log probability of the tactics leading to 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.
If LeanAgent finds a proof, it adds it to the dynamic database. The newly added premises from this proof will be included in a 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
Table 1: Selected repository descriptions
| PFR Hairy Ball Theorem Coxeter | Polynomial Freiman-Ruzsa Conjecture Algebraic topology result Coxeter groups |
| --- | --- |
| Mathematics in Lean Source | Lean files for the textbook |
| Formal Book | Proofs from THE BOOK |
| MiniF2F | Math olympiad-style problem solving |
| SciLean | Scientific computing |
| Carleson | Carleson’s Theorem |
| Lean4 PDL | Propositional Dynamic Logic |
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 to the end of lifelong learning. This shows LeanAgent’s continuous generalizability and improvement. (2) Lifelong Learning Analysis: We conduct an ablation study with six lifelong learning metrics to explain LeanAgent’s superiority in sorry theorem proving. Moreover, these results explain LeanAgent’s superior handling of the stability-plasticity tradeoff. Please see Appendix A.2 for experiment implementation details. We release LeanAgent at https://github.com/lean-dojo/LeanAgent.
Repositories. We evaluate our approach on a diverse set of 23 Lean repositories to assess its generalizability across different mathematical domains (Skřivan, 2024; Kontorovich, 2024; Avigad, 2024; Tao et al., 2024; Renshaw, 2024; Fermat’s Last Theorem, 2024; DeepMind, 2024; Carneiro, 2024; Wieser, 2024; Mizuno, 2024; Murphy, 2024; Formal Logic, 2024; Con-nf, 2024; Gadgil, 2024; Yang, 2024; Zeta 3 Irrational, 2024; Firsching, Moritz, 2024; Monnerjahn, 2024; van Doorn, 2024; Dillies, 2024; Hairy Ball Theorem, 2024; Coxeter, 2024; Gattinger, 2024). Details of key repositories are in Table 1. Further details of these repositories, including commits and how we chose the initial curriculum and the sub-curriculum (described in Sec. 4.2), are in Appendix A.3.
### 4.2 sorry Theorem Proving
We compare the number of sorry theorems LeanAgent can 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 initial retriever in our experiments.
<details>
<summary>extracted/6256159/newproof4.png Details</summary>
### Visual Description
## Mathematical Formalization Code Snippets: Project Examples
### Overview
The image displays five distinct code blocks, each representing a formal mathematical statement (lemma or theorem) and its proof, written in the Lean 4 proof assistant language. These snippets are sourced from different formalization projects or libraries, as indicated by their titles. The code is presented in a monospaced font with syntax highlighting (keywords in blue, definitions/tactics in green, types in brown). The layout is asymmetrical, with three blocks on the left and two on the right.
### Components/Axes
The image is organized into labeled sections, each containing a code block within a rounded rectangle. The labels are:
* **PFR** (Top-Left)
* **SciLean** (Middle-Left)
* **Coxeter** (Bottom-Left)
* **MiniF2F** (Top-Right)
* **Formal Book** (Bottom-Right)
There are no traditional chart axes, legends, or data points. The "data" consists of the textual code itself.
### Detailed Analysis / Content Details
#### **PFR (Top-Left)**
* **Label:** `PFR`
* **Code Transcription:**
```lean
lemma condRho_of_translate {Ω S : Type*} [MeasureSpace
Ω] (X : Ω → G) (Y : Ω → S) (A : Finset G) (s:G) :
condRho (fun ω ↦ X ω + s) Y A = condRho X Y A := by
simp only [condRho, rho_of_translate]
```
* **Content:** This is a lemma about a conditional expectation operator (`condRho`) in the context of measure theory. It states that translating the random variable `X` by a constant `s` does not change the value of `condRho`. The proof is completed by simplification (`simp`) using the definitions of `condRho` and `rho_of_translate`.
#### **SciLean (Middle-Left)**
* **Label:** `SciLean`
* **Code Transcription:**
```lean
theorem re_float (a : Float)
: RCLike.re a = a := by
exact RCLike.re_eq_self_of_le le_rfl
```
* **Content:** This theorem asserts that for a floating-point number `a` (treated as an element of a complex-like ring `RCLike`), its real part (`RCLike.re`) is equal to itself. The proof uses an exact application of a lemma `RCLike.re_eq_self_of_le` with a reflexivity proof (`le_rfl`).
#### **Coxeter (Bottom-Left)**
* **Label:** `Coxeter`
* **Code Transcription:**
```lean
lemma invmap.of_eq {S:Set G} [CoxeterSystem G S] {s :S}
: invmap S s = s := by
simp [CoxeterSystem.Presentation.invmap]
unfold CoxeterSystem.toMatrix
apply CoxeterSystem.monoidLift.mapLift.of
```
* **Content:** This lemma concerns Coxeter systems. It states that the inverse map (`invmap`) of a generator `s` from the set `S` is equal to `s` itself. The proof proceeds by simplifying the definition of `invmap`, unfolding the `toMatrix` definition, and then applying a property (`of`) from the monoid lift.
#### **MiniF2F (Top-Right)**
* **Label:** `MiniF2F`
* **Code Transcription (Theorem 1):**
```lean
theorem induction_12dvd4expnp1p20
(n : ℕ) :
12 | 4^(n+1) + 20 := by
norm_num
induction' n with n hn
simp
omega
```
* **Content:** This theorem from the MiniF2F benchmark states that for any natural number `n`, 12 divides `4^(n+1) + 20`. The proof uses numeric normalization (`norm_num`), induction on `n`, simplification (`simp`), and the omega tactic for linear arithmetic.
* **Code Transcription (Theorem 2):**
```lean
theorem amc12a_2002_p6
(n : ℕ)
(h₀ : 0 < n) :
∃ m, (m > n ∧ ∃ p, m * p ≤ m + p) := by
lift n to ℕ+ using h₀
cases' n with n
exact (_, lt_add_of_pos_right _ zero_lt_one, 1, by simp)
```
* **Content:** This theorem, sourced from the AMC 12A 2002 competition (problem 6), states that for any positive natural number `n`, there exists a natural number `m` greater than `n` such that there exists a `p` where `m * p ≤ m + p`. The proof lifts `n` to a positive natural number, performs case analysis, and provides a witness (`m = n+1`, `p = 1`).
#### **Formal Book (Bottom-Right)**
* **Label:** `Formal Book`
* **Code Transcription:**
```lean
theorem wedderburn (h: Fintype R): IsField R
:= by
apply Field.toIsField
```
* **Content:** This theorem states Wedderburn's little theorem: if a finite ring `R` (with a finite type `Fintype R`) is a division ring, then it is a field (`IsField R`). The proof applies the lemma `Field.toIsField`.
### Key Observations
1. **Diversity of Domains:** The snippets cover distinct areas of mathematics: measure theory (PFR), numerical analysis (SciLean), algebra/combinatorics (Coxeter), number theory and competition math (MiniF2F), and ring theory (Formal Book).
2. **Proof Techniques:** A variety of Lean 4 tactics are demonstrated, including `simp`, `exact`, `unfold`, `apply`, `norm_num`, `induction'`, `omega`, and `cases'`.
3. **Syntax Highlighting:** Keywords (`lemma`, `theorem`, `by`, `simp`, `exact`, etc.) are consistently highlighted in blue. Definitions, tactics, and specific constants (`condRho`, `rho_of_translate`, `RCLike.re_eq_self_of_le`, `CoxeterSystem.Presentation.invmap`, `lt_add_of_pos_right`, `Field.toIsField`) are highlighted in green. Type constructors and constants (`Type*`, `MeasureSpace`, `Finset`, `ℕ`, `Float`, `Set`, `CoxeterSystem`, `Fintype`) are in brown.
4. **Layout:** The code blocks are arranged in a non-grid, visually balanced manner. The `MiniF2F` block is the largest, containing two separate theorems.
### Interpretation
This image serves as a showcase or catalog of formalized mathematical results from various Lean 4 projects. It is not a data chart but a **technical document snippet**. The primary information is the code itself, which provides concrete examples of:
* **Formal Statement:** How mathematical concepts are precisely encoded in a dependently typed language.
* **Proof Sketch:** The high-level structure of the machine-checked proof, indicated by the tactic steps.
* **Project Scope:** The titles (`PFR`, `SciLean`, etc.) hint at the broader libraries or formalization efforts these snippets belong to, suggesting active work in formalizing diverse mathematical fields.
The value lies in the **precision and verifiability** of the content. Each snippet is a self-contained, machine-verifiable claim. For a researcher or developer in formal methods, this image provides quick reference examples of Lean 4 syntax and proof patterns across different domains. The highlighted green text likely draws attention to key definitions or lemmas that are central to each proof's strategy.
</details>
Figure 2: Case studies of LeanAgent’s new proofs. LeanAgent shows an ability to work with these repositories, often able to retrieve the necessary premises (highlighted). For example, LeanAgent proves a sorry theorem from PFR, condRho_of_translate, by simply expanding definitions, showing its proving ability on the PFR repository. In addition, LeanAgent could prove re_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 mathematics. LeanAgent’s proof of invmap.of_eq and wedderburn represents its theorem proving capabilities with abstract algebra premises.
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 of formalizing in a new repository after learning a curriculum. As such, we don’t evaluate LeanAgent after lifelong learning on MiniF2F.
| MIL MiniF2F Formal Book | 29 406 29 | 72.4 24.4 10.3 | 48.3 24.4 6.9 | 24.1 - 3.4 | 48.3 20.9 6.9 | 55.2 20.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 |
| PFR | 37 | 2.7 | 2.7 | 0.0 | 0.0 | 0.0 |
In addition, a use case of LeanAgent is proving in a new repository after learning a curriculum; we progressively train on MiniF2F to demonstrate this. Note that we choose the Lean4 version of the MiniF2F 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 set is also in Appendix A.5. Moreover, a mathematician could use LeanAgent for (1) an initial curriculum $A$ , and later (2) a sub-curriculum $B$ . LeanAgent can then help the mathematician prove in the repositories in curriculum $A+B$ . To demonstrate this scenario, we continue LeanAgent on a sub-curriculum $B$ of 8 repositories.
Results are in Table 2, with case studies in Figure 2. Appendix A.5 provides a more thorough discussion, including an ablation study, and contains the complete theorems and proofs relevant to this section.
LeanAgent demonstrates continuous generalizability and improvement in theorem-proving capabilities across multiple repositories. LeanAgent’s proofs are a superset of the sorry theorems proved by ReProver in most cases. Moreover, to isolate the effect of curriculum learning, we compare LeanAgent 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 learning. Overall, LeanAgent progresses from basic concepts (arithmetic, simple algebra) to advanced topics (abstract algebra, topology).
PFR. LeanAgent can prove a sorry theorem from this repository, while ReProver cannot. It also generalizes to a different commit (not included in progressive training), uncovering 7 system exploits. LeanAgent proves two theorems with just the rfl tactic, one of which ReProver cannot, and proves 5 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, it proves concepts in advanced function spaces, sophisticated bijections, and abstract algebraic structures.
Mathematics in Lean Source. During lifelong learning, LeanAgent proves theorems about basic algebraic structures and fundamental arithmetic properties. By the end of 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 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 Wedderburn’s Little Theorem. For the Coxeter repository, LeanAgent proves a complex lemma about Coxeter systems, showcasing its increased understanding of group theory. In the Hairy Ball Theorem repository, LeanAgent proves a key step of the theorem, demonstrating improved performance in algebraic topology. Only LeanAgent can prove these theorems, demonstrating that it has much more advanced theorem-proving capabilities than ReProver.
### 4.3 Lifelong Learning Analysis
To our knowledge, no 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 LeanAgent’s superior handling of the stability-plasticity tradeoff. These results help explain LeanAgent’s superiority 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 a combination of learning and dataset options. Options for learning setups are progressive training with or without EWC. Dataset setups involve a dataset order and construction. Options for dataset orders involve Single Repository or 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 construction include popularity order or curriculum order. Appendix A.3 shows these orders and additional repository details.
Metrics. We use six lifelong learning metrics: Windowed-Forgetting 5 (WF5), Forgetting Measure (FM), Catastrophic Forgetting Resilience (CFR), Expanded Backward Transfer (EBWT), Windowed-Plasticity 5 (WP5), and Incremental Plasticity (IP). A description of these metrics is in Table 3 (De Lange et al., 2023; Wang et al., 2024b; Díaz-Rodríguez et al., 2018). Our reasoning for considering these metrics is detailed in Appendix A.4.
Table 3: Description of lifelong learning metrics.
| WF5 | Measures forgetting over a 5-task window | Lower | Existing |
| --- | --- | --- | --- |
| FM | Average performance drop on 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 R@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 measures and is sensitive to the order of tasks, particularly relevant in lifelong learning for theorem proving.
In addition, these metrics in 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% to be significant.
Table 4: Comparison of lifelong learning metrics across setups. The best scores for each metric are in bold.
| WF5 ( $\downarrow$ ) FM ( $\downarrow$ ) CFR ( $\uparrow$ ) | 0.18 0.85 0.88 | 7.60 6.53 0.87 | 7.17 4.04 0.88 | 0.73 2.11 0.85 | 15.83 10.50 0.76 | 2.23 4.06 0.94 | 13.34 11.44 0.75 | 5.82 3.80 0.90 |
| --- | --- | --- | --- | --- | --- | --- | --- | --- |
| EBWT ( $\uparrow$ ) | 1.21 | 0.51 | 1.04 | 0.76 | -0.20 | 0.73 | -1.34 | -0.39 |
| WP5 ( $\uparrow$ ) | 2.47 | 0.89 | 1.47 | 3.42 | 0.00 | 0.09 | 0.00 | 0.11 |
| IP ( $\uparrow$ ) | 1.02 | 0.36 | 0.26 | 1.06 | -1.50 | -0.64 | -1.71 | -0.89 |
| 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 |
| Setup 3: EWC, Curriculum Learning | Setup 6: EWC, Popularity Order |
| Setup 7: EWC, Curriculum Learning | |
Single Repository Analysis. We first analyze the Single Repository results from Table 4. LeanAgent demonstrates superior stability across multiple metrics. The WF5 metric is 75.34% lower for LeanAgent than the next best setup, suggesting it maintains performance over a window more effectively. 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’s ability to continuously generalize over time. In addition, LeanAgent has a 16.25% higher EBWT, indicating its ability to continuously improve over time.
In contrast, Setup 3 exhibits characteristics of higher plasticity. It shows a 38.26% higher WP5 over LeanAgent, indicating a greater ability to rapidly adapt to new tasks in a window. This is complemented by its 3.98% higher IP over LeanAgent, suggesting a more pronounced improvement on new tasks over time. However, these plasticity gains come at a 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-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, we 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 across an 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 7 has a 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 a positive EBWT, indicating that learning new tasks improves performance on the entire historical dataset. The other setups have a negative EBWT, indicating performance degradation on earlier tasks after learning new ones.
Only Setups 5 and 7 have a 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 5 has the highest IP score with a 27.75% improvement over Setup 7, all 4 setups have negative IP values. This indicates a decrease in validation R@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 a fundamental issue with its approach.
Comparative Analysis and Insights. Although the metrics have different interpretations in the Single 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, as it indicates a fundamental inability to maintain and improve performance in a continuously growing dataset. In contrast, LeanAgent demonstrates a positive IP, indicating its ability to 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 consistent with LeanAgent’s sorry theorem proving performance. LeanAgent’s superior stability metrics (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 SciLean, 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, as reflected 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.
## 5 Conclusion
We have presented LeanAgent, a lifelong learning framework for theorem proving that achieves continuous generalizability and improvement across diverse mathematical domains. Key components 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, including from challenging mathematics. This highlights its potential to assist in formalizing complex proofs across multiple domains and identifying system exploits. For example, LeanAgent successfully proves challenging theorems in abstract algebra and algebraic topology. It outperforms the 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.
Future work could explore integration with Lean Copilot, providing real-time assistance with a mathematician’s repositories. In addition, a limitation of LeanAgent is its inability to prove certain theorems due to a lack of data on specific topics, such as odeSolve.arg_x 0.semiAdjoint_rule in SciLean about ODEs. To solve this problem, future work could use reinforcement learning for synthetic data generation during curriculum construction. Moreover, future work could use LeanAgent with additional math LLMs and search strategies.
#### Acknowledgments
Adarsh Kumarappan is supported by the Summer Undergraduate Research Fellowships (SURF) program 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 members for engaging in clarifying conversations that were incorporated into the paper.
## References
- Alama et al. (2014) Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. Journal of Automated Reasoning, 52(2):191–213, February 2014. ISSN 0168-7433, 1573-0670. doi: 10.1007/s10817-013-9286-5.
- Arana & Stafford (2023) Andrew Arana and Will Stafford. On the difficulty of discovering mathematical proofs. Synthese, 202(2):1–29, 2023. doi: 10.1007/s11229-023-04184-5.
- Avigad (2024) Jeremy Avigad. Avigad/mathematics_in_lean_source, August 2024.
- Azerbayev et al. (2024) Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An Open Language Model For Mathematics, March 2024.
- Bengio et al. (2009) 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-516-1. doi: 10.1145/1553374.1553380.
- Borgeaud et al. (2022) Sebastian Borgeaud, Arthur Mensch, Jordan Hoffmann, Trevor Cai, Eliza Rutherford, Katie Millican, George van den Driessche, Jean-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. Rae, Erich Elsen, and Laurent Sifre. Improving language models by retrieving from trillions of tokens, February 2022.
- Carneiro (2024) Mario Carneiro. Digama0/lean4lean, September 2024.
- Chang et al. (2021) Ernie Chang, Hui-Syuan Yeh, and Vera Demberg. Does the Order of Training Samples Matter? Improving Neural Data-to-Text Generation with Curriculum Learning. In Paola Merlo, Jorg Tiedemann, 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/2021.eacl-main.61.
- Chaudhry et al. (2019) Arslan Chaudhry, Marc’Aurelio Ranzato, Marcus Rohrbach, and Mohamed Elhoseiny. Efficient Lifelong Learning with A-GEM, January 2019.
- Chen et al. (2023) Jiefeng Chen, Timothy Nguyen, Dilan Gorur, and Arslan Chaudhry. Is forgetting less a good inductive bias for forward transfer?, March 2023.
- Chen et al. (2024) 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-Tuning. 2024. doi: 10.48550/ARXIV.2407.20999.
- Cirik et al. (2016) Volkan Cirik, Eduard Hovy, and Louis-Philippe Morency. Visualizing and Understanding Curriculum Learning for Long Short-Term Memory Networks, November 2016.
- Claude Team (2024) Claude Team. Introducing claude 3.5 sonnet, June 2024. URL https://www.anthropic.com/news/claude-3-5-sonnet.
- Community (2024a) Lean Community. Leanprover-community/lean-liquid. leanprover-community, September 2024a.
- Community (2024b) Lean Community. Leanprover-community/lean-perfectoid-spaces. leanprover-community, August 2024b.
- Con-nf (2024) Con-nf. Leanprover-community/con-nf: A formal consistency proof of Quine’s set theory New Foundations. https://github.com/leanprover-community/con-nf/tree/main, 2024.
- Coxeter (2024) Coxeter. NUS-Math-Formalization/coxeter at 96af8aee7943ca8685ed1b00cc83a559ea389a97. https://github.com/NUS-Math-Formalization/coxeter/tree/96af8aee7943ca8685ed1b00cc83a559ea389a97, 2024.
- De Lange et al. (2023) Matthias De Lange, Gido van de Ven, and Tinne Tuytelaars. Continual evaluation for lifelong learning: Identifying the stability gap, March 2023.
- De Moura et al. (2015) 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.), Automated Deduction - CADE-25, volume 9195, pp. 378–388, Cham, 2015. Springer International Publishing. ISBN 978-3-319-21400-9 978-3-319-21401-6. doi: 10.1007/978-3-319-21401-6˙26.
- DeepMind (2024) Google DeepMind. Google-deepmind/debate. Google DeepMind, August 2024.
- Díaz-Rodríguez et al. (2018) Natalia Díaz-Rodríguez, Vincenzo Lomonaco, David Filliat, and Davide Maltoni. Don’t forget, there is more than forgetting: New metrics for Continual Learning, October 2018.
- Dillies (2024) Yaël Dillies. YaelDillies/LeanAPAP, September 2024.
- Dohare et al. (2024) Shibhansh Dohare, J. Fernando Hernandez-Garcia, Qingfeng Lan, Parash Rahman, A. Rupam Mahmood, 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.1038/s41586-024-07711-7.
- Fermat’s Last Theorem (2024) Fermat’s Last Theorem. ImperialCollegeLondon/FLT. Imperial College London, September 2024.
- Firsching, Moritz (2024) Firsching, Moritz. Mo271/FormalBook: Formalizing ”Proofs from THE BOOK”, 2024.
- Formal Logic (2024) Formalized Formal Logic. FormalizedFormalLogic/Foundation. FormalizedFormalLogic, September 2024.
- Gadgil (2024) Siddhartha Gadgil. Siddhartha-gadgil/Saturn: Experiments with SAT solvers with proofs in Lean 4. https://github.com/siddhartha-gadgil/Saturn, 2024.
- Gattinger (2024) Malvin Gattinger. M4lvin/lean4-pdl, September 2024.
- Hairy Ball Theorem (2024) Hairy Ball Theorem. Corent1234/hairy-ball-theorem-lean at a778826d19c8a7ddf1d26beeea628c45450612e6. https://github.com/corent1234/hairy-ball-theorem-lean/tree/a778826d19c8a7ddf1d26beeea628c45450612e6, 2024.
- Irving et al. (2016) Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Een, Francois Chollet, and Josef Urban. DeepMath - Deep Sequence Models for Premise Selection. In Advances in Neural Information Processing Systems, volume 29. Curran Associates, Inc., 2016.
- Jiang et al. (2022) Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. 2022. doi: 10.48550/ARXIV.2205.10893.
- Jiang et al. (2024) Gangwei Jiang, Caigao Jiang, Zhaoyi Li, Siqiao Xue, Jun Zhou, Linqi Song, Defu Lian, and Ying Wei. Interpretable Catastrophic Forgetting of Large Language Model Fine-tuning via Instruction Vector. 2024. doi: 10.48550/ARXIV.2406.12227.
- Kevin Buzzard (2019) Kevin Buzzard. The Future of Mathematics? Professor Kevin Buzzard - 30 May 2019, June 2019.
- Kim et al. (2023) Seungyeon Kim, Ankit Singh Rawat, Manzil Zaheer, Sadeep Jayasumana, Veeranjaneyulu Sadhanala, Wittawat Jitkrittum, Aditya Krishna Menon, Rob Fergus, and Sanjiv Kumar. EmbedDistill: A Geometric Knowledge Distillation for Information Retrieval. 2023. doi: 10.48550/ARXIV.2301.12005.
- Kirkpatrick et al. (2017) James Kirkpatrick, Razvan Pascanu, Neil Rabinowitz, Joel Veness, Guillaume Desjardins, Andrei A. Rusu, Kieran Milan, John Quan, Tiago Ramalho, Agnieszka Grabska-Barwinska, Demis Hassabis, Claudia Clopath, Dharshan Kumaran, and Raia Hadsell. Overcoming catastrophic forgetting in neural networks. Proceedings of the National Academy of Sciences, 114(13):3521–3526, March 2017. ISSN 0027-8424, 1091-6490. doi: 10.1073/pnas.1611835114.
- Kontorovich (2024) Alex Kontorovich. AlexKontorovich/PrimeNumberTheoremAnd, August 2024.
- (37) 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.
- Li et al. (2024) 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–18498, March 2024. ISSN 2374-3468, 2159-5399. doi: 10.1609/aaai.v38i16.29810.
- Li & Hoiem (2017) Zhizhong Li and Derek Hoiem. Learning without Forgetting, February 2017.
- Lin et al. (2024) Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-STaR: Learning to Interleave Thinking and Proving, August 2024.
- Liu et al. (2023) 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: A Challenge Formal Dataset for Automated Theorem Proving, December 2023.
- Lopez-Paz & Ranzato (2017) 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.
- Loshchilov & Hutter (2017) I. Loshchilov and F. Hutter. Decoupled Weight Decay Regularization. In International Conference on Learning Representations, November 2017.
- Lu et al. (2024) Minghai Lu, Benjamin Delaware, and Tianyi Zhang. Proof Automation with Large Language Models, September 2024.
- Lu et al. (2022) Shuai Lu, Nan Duan, Hojae Han, Daya Guo, Seung-won Hwang, and Alexey Svyatkovskiy. ReACC: A Retrieval-Augmented 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 1: Long Papers), pp. 6227–6240, Dublin, Ireland, May 2022. Association for Computational Linguistics. doi: 10.18653/v1/2022.acl-long.431.
- mathlib4 Community (2024) The mathlib4 Community. Leanprover-community/mathlib4. leanprover-community, September 2024.
- Mendez & Eaton (2021) Jorge A Mendez and Eric Eaton. Lifelong Learning of Compositional Structures. 2021.
- Mikuła et al. (2024) Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. Magnushammer: A Transformer-Based Approach to Premise Selection, March 2024.
- Mizuno (2024) Yuma Mizuno. Yuma-mizuno/lean-math-workshop. https://github.com/yuma-mizuno/lean-math-workshop, 2024.
- Monnerjahn (2024) Ludwig Monnerjahn. Louis-Le-Grand/Formalisation-of-constructable-numbers, September 2024.
- Murphy (2024) Logan Murphy. Loganrjmurphy/LeanEuclid, September 2024.
- OpenAI (2024) OpenAI. OpenAI o1 System Card, September 2024.
- Piotrowski et al. (2023) Bartosz Piotrowski, Ramon Fernández Mir, and Edward Ayers. Machine-Learned Premise Selection 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: 10.1007/978-3-031-43513-3˙10.
- Polu et al. (2022) Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and I. Sutskever. Formal Mathematics Statement Curriculum Learning. ArXiv, February 2022.
- Renshaw (2024) David Renshaw. Dwrensha/compfiles: Catalog Of Math Problems Formalized In Lean. https://github.com/dwrensha/compfiles, September 2024.
- Shao et al. (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.
- Shin et al. (2017) Hanul Shin, Jung Kwon Lee, Jaehong Kim, and Jiwon Kim. Continual Learning with Deep Generative Replay, December 2017.
- Skřivan (2024) Tomáš Skřivan. Lecopivo/SciLean: Scientific computing in Lean 4. https://github.com/lecopivo/SciLean/tree/master, September 2024.
- Song et al. (2024) Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in lean, 2024. URL https://arxiv.org/abs/2404.12534.
- (60) Valentin I Spitkovsky, Hiyan Alshawi, and Daniel Jurafsky. Baby Steps: How “Less is More” in Unsupervised Dependency Parsing.
- Subramanian et al. (2017) Sandeep Subramanian, Sai Rajeswar, Francis Dutil, Chris Pal, and Aaron Courville. Adversarial Generation of 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–251, Vancouver, Canada, August 2017. Association for Computational Linguistics. doi: 10.18653/v1/W17-2629.
- (62) Terence Tao. Teorth/asymptotic.
- Tao (2024a) Terence Tao. Teorth/newton, June 2024a.
- Tao (2024b) Terence Tao. Teorth/symmetric_project, July 2024b.
- Tao et al. (2024) Terence Tao, Pietro Monticone, Lorenzo Luccioli, and Rémy Degenne. Teorth/pfr, August 2024.
- Thakur et al. (2024) Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An In-Context Learning Agent for Formal Theorem-Proving, August 2024.
- (67) 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.
- van de Ven et al. (2024) Gido M. van de Ven, Nicholas Soures, and Dhireesha Kudithipudi. Continual Learning and Catastrophic Forgetting, March 2024.
- van Doorn (2024) Floris van Doorn. Fpvandoorn/carleson, September 2024.
- Vaswani et al. (2017) Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Ł ukasz Kaiser, and Illia Polosukhin. Attention is All you Need. In Advances in Neural Information Processing Systems, volume 30. Curran Associates, Inc., 2017.
- Wang et al. (2023) Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, and Xiaodan Liang. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function. In Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki (eds.), Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 12632–12646, Toronto, Canada, July 2023. Association for Computational Linguistics. doi: 10.18653/v1/2023.acl-long.706.
- Wang et al. (2024a) 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.
- Wang et al. (2024b) Liyuan Wang, Xingxing Zhang, Hang Su, and Jun Zhu. A Comprehensive Survey of Continual Learning: Theory, Method and Application. IEEE Transactions on Pattern Analysis and Machine Intelligence, 46(8):5362–5383, August 2024b. ISSN 0162-8828, 2160-9292, 1939-3539. doi: 10.1109/TPAMI.2024.3367329.
- Wang & Deng (2020) Mingzhe Wang and Jia Deng. Learning to Prove Theorems by Learning to Generate Theorems. ArXiv, February 2020.
- Wang et al. (2024c) Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts, October 2024c.
- Wieser (2024) Eric Wieser. Eric-wieser/lean-matrix-cookbook: The matrix cookbook, proved in the Lean theorem prover. https://github.com/eric-wieser/lean-matrix-cookbook, 2024.
- Xin et al. (2024a) Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data, May 2024a.
- Xin et al. (2024b) Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search, August 2024b.
- Xue et al. (2022) Linting Xue, Aditya Barua, Noah Constant, Rami Al-Rfou, Sharan Narang, Mihir Kale, Adam Roberts, and Colin Raffel. ByT5: Towards a Token-Free Future with Pre-trained Byte-to-Byte Models. Transactions of the Association for Computational Linguistics, 10:291–306, 2022. doi: 10.1162/tacl˙a˙00461.
- Yang (2024) Kaiyu Yang. Yangky11/miniF2F-lean4. https://github.com/yangky11/miniF2F-lean4/tree/main, 2024.
- Yang et al. (2023) 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: 10.48550/ARXIV.2306.15626.
- Zaremba & Sutskever (2015) Wojciech Zaremba and Ilya Sutskever. Learning to Execute, February 2015.
- Zeta 3 Irrational (2024) Zeta 3 Irrational. Ahhwuhu/zeta_3_irrational at 3d68ddd90434a398c9a72f30d50c57f15a0118c7. https://github.com/ahhwuhu/zeta_3_irrational/tree/3d68ddd90434a398c9a72f30d50c57f15a0118c7, 2024.
- (84) Jiawei Zhao, Zhenyu Zhang, Beidi Chen, Zhangyang Wang, Anima Anandkumar, and Yuandong Tian. GaLore: Memory-Efficient LLM Training by Gradient Low-Rank Projection. URL http://arxiv.org/abs/2403.03507.
- Zhou et al. (2024) 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.
- Zhou et al. (2023) Shuyan Zhou, Uri Alon, Frank F. Xu, Zhiruo Wang, Zhengbao Jiang, and Graham Neubig. DocPrompting: Generating Code by Retrieving the Docs, February 2023.
- Zombori et al. (2019) Zsolt Zombori, Adrian Csiszarik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban. Curriculum Learning and Theorem Proving. 2019.
## Appendix A Appendix
### A.1 Further Methodology Details
Repository Scanning and Data Extraction. We use the GitHub API to query for Lean repositories based on sorting parameters (e.g., by repository stars or 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 a new commit or Lean version.
We clone each identified repository locally using the Git version control system. To ensure compatibility with our theorem-proving pipeline, we check the Lean version required by each repository and 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 version. This version checking is performed by parsing the repository’s configuration files and extracting the specified Lean version.
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 of 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 as 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.
If we encounter duplicate theorems between repositories while merging repositories, we use 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 as 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 to 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 to 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 URL 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 topological 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. To precompute the embeddings, we use a single forward pass with batch processing to serialize and 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 a directed dependency graph to represent each file path in the corpus, adding files as nodes and imports as edges, and creating a transitive closure of this graph. We also track all premises encountered during this process, building a comprehensive knowledge base.
Crucially, we limit retrieval to a subset of all available premises to aid the effectiveness of the results. 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 original 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 keywords corresponding to 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. After integrating the proofs, we commit our changes, push them, and create a 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 AdamW (Loshchilov & Hutter, 2017) with an effective batch size of 16 (achieved through a batch size of 4 with gradient accumulation over 4 steps). In the first 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, we sample 3 negative premises per example, including 1 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 tactic generator for the experiments. We generate tactics with a beam search of size 5. We used 4 CPU workers, 1 per GPU. Due to the wide variety of repositories and experimental setups that we tested, the time for each experiment widely varied. For example, the experiments in Table 10 took from 4 to 9 days to complete.
Furthermore, we do not compare LeanAgent with any existing LLM-based prover besides ReProver because LeanAgent is a framework, not a model. As mentioned previously, it can be used with any LLM. As such, a 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 retriever as the starting one in LeanAgent, allowing for a more faithful comparison.
Moreover, we do not compare with Aesop because it is not an ML model. We aim to improve upon ML research for theorem proving, such as ReProver. Moreover, Aesop is not a 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 to 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 DeepSeek-Prover (Xin et al., 2024a), using these LLMs in our work would require architectural 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-based. As such, rather than progressively training a 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 as we do with ReProver’s retriever and tactic generator, we may instead need to generate the entire proof at once. This setup is quite dissimilar from our current evaluation, and so these results may be too dissimilar from our current evaluation framework.
In addition, we would like to note that because LeanAgent does not claim to contribute a new search algorithm, it can be used with other search strategies such as Hypertree Proof Search (Lample et al., ). However, the source code for Hypertree Proof Search was only recently released on GitHub, explaining why we did not use it thus far.
Moreover, the objective function for Elastic Weight Consolidation (EWC) is given by:
$$
L(\theta)=L_{B}(\theta)+\frac{\lambda}{2}\sum_{i}F_{i}(\theta_{i}-\theta_{A,i}
)^{2}
$$
where $L_{B}(\theta)$ is the loss for the current task B, $i$ is the label for each parameter, $\theta_{A,i}$ are the parameters from the previous task A, $F_{i}$ is the Fisher information matrix, and $\lambda$ is a hyperparameter that controls the strength of the EWC penalty. For the setups that use EWC, we performed a grid search over $\lambda$ values in {0.01, 0.1, 1, 10, 100}. For each value, we ran Setup 2 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
Table 6: Repository commits. Formalization of Const. Numbers denotes Formalization of Constructable Numbers.
| PFR Hairy Ball Theorem Coxeter | fa398a5b853c7e94e3294c45e50c6aee013a2687 a778826d19c8a7ddf1d26beeea628c45450612e6 96af8aee7943ca8685ed1b00cc83a559ea389a97 |
| --- | --- |
| Mathematics in Lean Source | 5297e0fb051367c48c0a084411853a576389ecf5 |
| Formal Book | 6fbe8c2985008c0bfb30050750a71b90388ad3a3 |
| MiniF2F | 9e445f5435407f014b88b44a98436d50dd7abd00 |
| SciLean | 22d53b2f4e3db2a172e71da6eb9c916e62655744 |
| Carleson | bec7808b907190882fa1fa54ce749af297c6cf37 |
| Lean4 PDL | c7f649fe3c4891cf1a01c120e82ebc5f6199856e |
| Prime Number Theorem And | 29baddd685660b5fedd7bd67f9916ae24253d566 |
| Compfiles | f99bf6f2928d47dd1a445b414b3a723c2665f091 |
| FLT | b208a302cdcbfadce33d8165f0b054bfa17e2147 |
| Debate | 7fb39251b705797ee54e08c96177fabd29a5b5a3 |
| Lean4Lean | 05b1f4a68c5facea96a5ee51c6a56fef21276e0f |
| Matrix Cookbook | f15a149d321ac99ff9b9c024b58e7882f564669f |
| Math Workshop | 5acd4b933d47fd6c1032798a6046c1baf261445d |
| LeanEuclid | f1912c3090eb82820575758efc31e40b9db86bb8 |
| Foundation | d5fe5d057a90a0703a745cdc318a1b6621490c21 |
| Con-nf | 00bdc85ba7d486a9e544a0806a1018dd06fa3856 |
| Saturn | 3811a9dd46cdfd5fa0c0c1896720c28d2ec4a42a |
| Zeta 3 Irrational | 914712200e463cfc97fe37e929d518dd58806a38 |
| Formalization of Const. Numbers | 01ef1f22a04f2ba8081c5fb29413f515a0e52878 |
| LeanAPAP | 951c660a8d7ba8e39f906fdf657674a984effa8b |
Table 7: Repository orders (initial curriculum). Note that Popularity Order is by star count on August 20, 2024.
| 1 2 3 | Compfiles Mathematics in Lean Source Prime Number Theorem And | SciLean FLT PFR |
| --- | --- | --- |
| 4 | Math Workshop | Prime Number Theorem And |
| 5 | FLT | Compfiles |
| 6 | PFR | Debate |
| 7 | SciLean | Mathematics in Lean Source |
| 8 | Debate | Lean4Lean |
| 9 | Matrix Cookbook | Matrix Cookbook |
| 10 | Con-nf | Math Workshop |
| 11 | Foundation | LeanEuclid |
| 12 | Saturn | Foundation |
| 13 | LeanEuclid | Con-nf |
| 14 | Lean4Lean | Saturn |
Table 8: Curriculum order (sub-curriculum)
| 1 2 3 | Zeta 3 Irrational Formal Book Formalization of Constructable Numbers |
| --- | --- |
| 4 | Carleson |
| 5 | LeanAPAP |
| 6 | Hairy Ball Theorem |
| 7 | Coxeter |
| 8 | Lean4 PDL |
Table 9: Repository theorem and premise counts
| PFR Hairy Ball Theorem Coxeter | 74306 73026 71273 | 109855 131217 127608 |
| --- | --- | --- |
| Mathematics in 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 | 115751 |
| Compfiles | 121391 | 178108 |
| FLT | 75082 | 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 |
| Zeta 3 Irrational | 120174 | 176332 |
| Formalization of Const. Numbers | 74050 | 109645 |
| LeanAPAP | 71090 | 109477 |
Repository Statistics and Information. Additional repository descriptions are in Table 5. The commits we used for experiments are in Table 6. Moreover, the repository orders are detailed in Table 7 and Table 8. Furthermore, the total number of theorems and premises per repository (including dependencies) are in Table 9.
Repository Selection Process. Many repositories have issues such as incompatibilities with LeanDojo, 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; Díaz-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 removed metrics that were redundant. For example, prior work suggests that evaluating lifelong learning 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 a window size of 5 for WF and WP as this represents a relatively medium-term understanding, given that we have 14 repositories. This would provide a balanced interpretation of forgetting and plasticity. Furthermore, we use the EBWT metric, in line with previous work, to evaluate LeanAgent throughout its lifetime rather than simply at the end (Díaz-Rodríguez et al., 2018). Moreover, we chose not to include the Forward Transfer metric as prior work has shown that a lower FM leads to better forward transfer (Chen et al., 2023). As such, we only check FM. We also chose not to include lifelong learning metrics 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 R@10, which are already measures of LeanAgent’s performance.
We provide some additional details on the metrics we used. Windowed-Forgetting 5 (WF5) quantifies model stability by measuring the maximum performance decrease in average test R@10 over a sliding window of 5 evaluations. Following prior work, we define WF for a 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 stability-plasticity trade-off. Furthermore, the Forgetting Measure (FM) measures the negative influence that learning a task has on the test R@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. Windowed-Plasticity 5 (WP5) measures the ability to learn new information by quantifying the maximum average test R@10 increase over a sliding window of 5 evaluations. Incremental Plasticity (IP) tracks changes in validation R@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 task-incremental setup. To our knowledge, an 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 to 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 on isolated tasks.
It 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 curriculum-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 some of its shortcomings. However, when used with a more effective curriculum-based ordering, 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-based 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 2.
First, we note that comparing LeanAgent to ReProver+, 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 on the entire dataset each time. When a 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, as shown in our experiments with both the initial curriculum and sub-curriculum. 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 be 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 in 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 a 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 as 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 repositories, including MiniF2F, Scilean, and PFR. We find that these repositories contain a range of mathematical concepts that require progressively more advanced reasoning capabilities. This highlights the effectiveness of our lifelong learning approach in continuously generalizing to and improving on expanding mathematical knowledge without catastrophic forgetting.
Table 10: Accuracy comparison across setups. Accuracy is calculated as (proven theorems / total sorry theorems). MIL denotes the Mathematics in Lean Source repository, LA denotes LeanAgent, and SX denotes Setup X (e.g., S1 is Setup 1). The best accuracy for each repository is in bold.
| MIL SciLean PFR | 29 294 37 | 72.4 9.2 2.7 | 55.2 8.5 0.0 | 41.4 7.5 0.0 | 55.2 6.8 0.0 | 55.2 8.5 0.0 | 48.3 8.5 0.0 | 58.6 8.8 0.0 | 48.3 7.8 0.0 |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
In addition to comparing LeanAgent and ReProver, we conduct an ablation study between LeanAgent 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 of sorry theorems that these setups can prove.
Mathematics in Lean Source. We notice a progression in LeanAgent’s proving ability in the Mathematics in 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 instance, MyGroup.mul_right_inv shows that multiplying an element by its inverse yields the identity and MyRing.add_right_cancel demonstrates the cancellation property in ring addition.
<details>
<summary>extracted/6256159/carbon17.png Details</summary>
### Visual Description
## Code Snippet: Mathematical Theorems in a Proof Assistant
### Overview
The image displays a dark-themed code editor or terminal window containing two mathematical theorem statements and their proofs, written in a formal proof language (likely Lean or a similar system). The text is syntax-highlighted with distinct colors for keywords, theorem names, variables, and operators.
### Components/Axes
* **Window Frame:** A dark gray rectangular window with rounded corners, centered on a light gray background.
* **Window Controls:** Three colored circles (red, yellow, green) are positioned in the top-left corner of the window, typical of a macOS-style interface.
* **Content Area:** The main body of the window contains two separate theorem definitions, each spanning two lines.
### Detailed Analysis / Content Details
The content consists of two formal theorem statements.
**Theorem 1:**
* **Line 1:** `theorem mul_right_inv (a : G) : a * a⁻¹ = 1 := by`
* `theorem`: Keyword (pink).
* `mul_right_inv`: Theorem name (yellow).
* `(a : G)`: Parameter declaration. `a` is a variable of type `G` (likely a Group).
* `: a * a⁻¹ = 1`: The proposition being proved. It states that for an element `a` in group `G`, multiplying `a` by its inverse (`a⁻¹`) yields the identity element (`1`).
* `:= by`: Introduces the proof tactic.
* **Line 2:** ` simp`
* `simp`: The proof tactic (purple), short for "simplify." This is a common automated tactic in proof assistants.
**Theorem 2:**
* **Line 1:** `theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c := by`
* `theorem`: Keyword (pink).
* `add_right_cancel`: Theorem name (yellow).
* `{a b c : R}`: Implicit parameters. `a`, `b`, and `c` are elements of type `R` (likely a Ring or similar additive structure).
* `(h : a + b = c + b)`: A hypothesis named `h` stating that `a + b` equals `c + b`.
* `: a = c`: The proposition to be proved: `a` equals `c`.
* `:= by`: Introduces the proof tactic.
* **Line 2:** ` simpa using h`
* `simpa using h`: The proof tactic (purple). `simpa` is likely a variant of the simplify tactic that can use the hypothesis `h`.
### Key Observations
1. **Syntax Highlighting:** The code uses a consistent color scheme: pink for keywords (`theorem`), yellow for theorem names, light blue for types (`G`, `R`), white for variables and most symbols, and purple for proof tactics (`simp`, `simpa`).
2. **Mathematical Notation:** Standard mathematical symbols are used: `*` for multiplication, `⁻¹` for inverse, `=` for equality, `+` for addition.
3. **Proof Structure:** Both theorems follow the pattern: `theorem <name> <parameters> : <proposition> := by <tactic>`.
4. **Theorem Content:** The theorems represent fundamental algebraic properties:
* `mul_right_inv`: The right inverse property in a group.
* `add_right_cancel`: The right cancellation law for addition.
### Interpretation
This image is a screenshot of a formal verification environment. It demonstrates the process of stating and proving basic algebraic theorems using a computer-assisted proof system.
* **What the data suggests:** The code is not just mathematical notation but *executable specifications*. The `by` keyword signals to the proof assistant that an automated procedure (the tactic) will follow to convince the system of the theorem's truth.
* **How elements relate:** The first line of each theorem defines the logical statement. The indented second line contains the "recipe" (tactic script) for the proof. The hypothesis `h` in the second theorem is a crucial input for its `simpa` tactic.
* **Notable patterns/anomalies:** The use of `{}` for implicit parameters in the second theorem versus `()` for explicit parameters in the first is a syntactic detail indicating how these variables are introduced in the proof context. The tactics `simp` and `simpa` suggest these proofs are relatively straightforward and can be handled by the system's built-in simplification rules, especially when aided by a hypothesis (`using h`).
In essence, this snippet captures a moment of human-computer collaboration in mathematics, where a user declares a truth and delegates the rigorous verification to a machine.
</details>
b) Elementary Number Theory: LeanAgent handles fundamental arithmetic properties, including MyRing.zero_mul, which proves that zero multiplied by any number is zero, and MyRing.neg_neg, which shows that the negative of a negative number is the original number.
<details>
<summary>extracted/6256159/carbon19.png Details</summary>
### Visual Description
\n
## Code Snippet: Lean 4 Theorem Proofs
### Overview
The image displays a code snippet within a stylized window resembling a macOS terminal or code editor. The window has a dark charcoal gray background with rounded corners and a subtle drop shadow, set against a light gray-blue gradient background. The content consists of two formal theorem statements written in the Lean 4 programming language and proof assistant, featuring syntax highlighting.
### Components/Axes
* **Window Frame:** A dark gray (`#2d2d30` approximate) rounded rectangle.
* **Window Controls:** Three circular buttons in the top-left corner, from left to right: red, yellow, and green.
* **Code Area:** The main content area within the window frame.
* **Text & Syntax Highlighting:** The code uses a monospaced font. The syntax highlighting scheme is as follows:
* Keywords (`theorem`, `by`, `rw`, `simp`): Light pink/salmon.
* Theorem names (`zero_mul`, `neg_neg`): Light yellow/gold.
* Variables and types (`a`, `R`): Light blue/cyan.
* Operators and punctuation (`:`, `*`, `=`, `:=`, `[`, `]`, `.`): Light gray/white.
* Proof tactics and class names (`MulZeroClass.zero_mul`): Light pink/salmon for the tactic, with the class path in a lighter shade.
### Detailed Analysis
The code contains two distinct theorem proofs.
**1. Theorem `zero_mul`**
* **Statement:** `theorem zero_mul (a : R) : 0 * a = 0 := by`
* This declares a theorem named `zero_mul`.
* It takes one argument `a` of type `R` (where `R` is presumably a type representing a ring or similar algebraic structure).
* The proposition to be proven is `0 * a = 0` (multiplying any element `a` by zero yields zero).
* **Proof:** `rw [MulZeroClass.zero_mul]`
* The proof is a single tactic: `rw` (rewrite).
* It rewrites the goal using the lemma `MulZeroClass.zero_mul`, which is a standard lemma from Lean's mathlib stating that for any type with a multiplication and a zero element satisfying the `MulZeroClass` axioms, `0 * a = 0`. This indicates the proof is leveraging a pre-existing, more general result.
**2. Theorem `neg_neg`**
* **Statement:** `theorem neg_neg (a : R) : - -a = a := by`
* This declares a theorem named `neg_neg`.
* It takes one argument `a` of type `R`.
* The proposition is `- -a = a` (the negation of the negation of `a` equals `a`).
* **Proof:** `simp`
* The proof uses the `simp` tactic, which is a powerful automated tactic that simplifies expressions by applying a set of known simplification rules (lemmas). In this context, it would use rules defining the properties of negation in the structure `R`.
### Key Observations
* **Language:** The code is written in **Lean 4**, a functional programming language and interactive theorem prover.
* **Context:** The theorems are fundamental properties in abstract algebra. `zero_mul` is an axiom or property of a `MulZeroClass`, and `neg_neg` is a property of an additive inverse in a structure like a group or ring.
* **Proof Style:** The proofs are concise and rely on automation (`simp`) or referencing existing library lemmas (`rw`), which is idiomatic for Lean 4 and mathlib.
* **Visual Design:** The image is a mock-up or presentation graphic, not a raw screenshot. The syntax highlighting is aesthetic and consistent, and the window styling is minimalist and modern.
### Interpretation
This image serves as a visual example of formal mathematical verification in Lean 4. It demonstrates how basic algebraic properties are stated and proven within the system.
* **What it shows:** It captures the essence of "proof by authority" or "proof by definition" in a formal system. The first theorem (`zero_mul`) is proven by directly invoking a more fundamental lemma from a library, showing how complex mathematics is built from a hierarchy of definitions and theorems. The second (`neg_neg`) is proven by a general simplification tactic, showcasing the power of automation for routine algebraic manipulations.
* **Significance:** These theorems, while simple, are foundational. Their formal proof ensures absolute correctness within the logical framework of Lean. The image likely aims to illustrate the syntax, conciseness, and power of the Lean 4 language for formalizing mathematics.
* **Underlying Message:** The clean, highlighted code in a familiar editor window makes advanced formal verification appear accessible and integrated into a modern development workflow. It bridges the gap between abstract mathematical logic and practical software tooling.
</details>
c) Order Theory: LeanAgent grasps order theory, as evidenced by absorb1, which proves that the infimum of x and the supremum of x and y is always equal to x, and absorb2, which demonstrates that the supremum of x and the infimum of x and y is always equal to x.
<details>
<summary>extracted/6256159/carbon20.png Details</summary>
### Visual Description
\n
## Screenshot: Code Editor Window with Mathematical Theorems
### Overview
The image is a screenshot of a dark-themed code editor or terminal window displaying two lines of formal mathematical theorem statements written in a proof assistant language (likely Lean or a similar system). The window is centered against a neutral gray gradient background.
### Components/Axes
- **Window Frame**: A dark gray (`#2d2d2d` approx.) rounded rectangle with a subtle drop shadow, giving it a floating appearance.
- **Window Controls**: Three colored circles in the top-left corner of the window, from left to right: red, yellow, green. These are standard macOS-style window control buttons (close, minimize, maximize).
- **Text Content Area**: The main body of the window contains two lines of code, formatted with syntax highlighting. The text is in a monospaced font.
- **Background**: The area outside the window is a smooth, light-to-medium gray gradient.
### Detailed Analysis
The window contains two distinct theorem definitions. The text is transcribed below with its original formatting and symbols.
**Line 1 (Top Theorem):**
- **Text**: `theorem absorb1 : x ∩ (x ∪ y) = x := by simp`
- **Syntax Highlighting**:
- `theorem` and `by`: Displayed in a yellow/gold color.
- `absorb1`: Displayed in a light blue/cyan color.
- `x`, `y`: Displayed in a green color.
- `∩`, `∪`, `=`, `:`, `(`, `)`: Displayed in a light gray/white color.
- `simp`: Displayed in the same yellow/gold as `theorem` and `by`.
**Line 2 (Bottom Theorem):**
- **Text**: `theorem absorb2 : x ∪ x ∩ y = x := by simp`
- **Syntax Highlighting**: Follows the same pattern as the first line.
- `theorem` and `by`: Yellow/gold.
- `absorb2`: Light blue/cyan.
- `x`, `y`: Green.
- `∪`, `∩`, `=`, `:`: Light gray/white.
- `simp`: Yellow/gold.
**Mathematical Symbols Identified:**
- `∩`: Set intersection operator (Unicode: U+2229).
- `∪`: Set union operator (Unicode: U+222A).
### Key Observations
1. **Content**: The text presents two fundamental absorption laws from set theory or lattice theory.
2. **Structure**: Both theorems follow an identical syntactic structure: `theorem [name] : [mathematical identity] := by simp`.
3. **Proof Tactic**: The proof for both theorems is concluded with the tactic `simp`, which is short for "simplification." This indicates these are likely basic, foundational identities that a proof assistant can verify automatically.
4. **Visual Design**: The syntax highlighting is consistent and aids in parsing the code structure. The color scheme is a common dark theme variant.
### Interpretation
The image displays formal, machine-verifiable statements of two core algebraic properties.
- **Theorem `absorb1`**: `x ∩ (x ∪ y) = x`. This is the **first absorption law**. It states that the intersection of a set `x` with the union of `x` and any other set `y` is simply `x`. Intuitively, since `x` is already contained within `(x ∪ y)`, taking the intersection with `x` yields `x` itself.
- **Theorem `absorb2`**: `x ∪ x ∩ y = x`. This is the **second absorption law**. It states that the union of a set `x` with the intersection of `x` and any other set `y` is simply `x`. Intuitively, since `(x ∩ y)` is a subset of `x`, adding it to `x` via a union does not change `x`.
**Significance**: These laws are fundamental in Boolean algebra, set theory, and the theory of lattices. They demonstrate how one operation (intersection or union) can "absorb" a more complex expression involving the other operation, simplifying it to a single variable. The fact they are presented in a proof assistant context highlights their role as axiomatic or easily derivable truths within a formal system, serving as building blocks for more complex proofs. The use of `simp` confirms their status as canonical simplification rules.
</details>
d) Rudimentary Real Analysis: LeanAgent demonstrates an early capability to handle properties related to real numbers and absolute values, as shown by C03S05.MyAbs.abs_add, which proves the triangle inequality for real numbers.
<details>
<summary>extracted/6256159/carbon21.png Details</summary>
### Visual Description
## Code Snippet: Formal Theorem Statement in Lean 4
### Overview
The image displays a screenshot of a code editor or terminal window with a dark theme. It contains a single line of formal mathematical code, specifically a theorem statement and its proof in the Lean 4 theorem prover language. The theorem is the well-known "triangle inequality" for real numbers.
### Components/Visual Elements
* **Window Frame:** A dark gray, rounded rectangle window is centered against a lighter gray gradient background.
* **Window Controls:** In the top-left corner of the window, there are three circular buttons: red, yellow, and green, consistent with macOS window management controls.
* **Text Content:** A single line of monospaced text is displayed in the main body of the window. The text is a valid Lean 4 code statement.
### Content Details
**Primary Language:** The code syntax is **Lean 4**, a functional programming language and interactive theorem prover. The mathematical content is expressed in standard notation.
**Transcription of Text:**
```lean
theorem abs_add (x y : ℝ) : |x + y| ≤ |x| + |y| := by
apply abs_add_le
```
**Breakdown of the Statement:**
1. **`theorem abs_add`**: Declares a theorem named `abs_add`.
2. **`(x y : ℝ)`**: Specifies the theorem's parameters. `x` and `y` are variables of type `ℝ` (the set of real numbers).
3. **`: |x + y| ≤ |x| + |y|`**: States the proposition to be proven. This is the triangle inequality: the absolute value of a sum is less than or equal to the sum of the absolute values.
4. **`:= by`**: Introduces the proof block.
5. **`apply abs_add_le`**: The proof tactic. It instructs the system to prove the goal by applying a previously proven lemma or theorem named `abs_add_le`, which is presumably a more general or foundational version of this inequality.
### Key Observations
* **Formal Verification:** This is not a comment or documentation; it is executable, verifiable code within a proof assistant. The statement's truth is mechanically checked by the Lean compiler.
* **Conciseness:** The proof is extremely concise, relying on a single tactic (`apply`) that references an existing result (`abs_add_le`). This suggests `abs_add_le` is a core lemma in the mathematical library being used.
* **Syntax:** The code uses standard mathematical symbols (`ℝ`, `| |`, `≤`) integrated into the programming language's syntax.
### Interpretation
This image captures a moment of formal mathematical verification. The data presented is not numerical but logical and syntactic.
* **What it demonstrates:** It shows the formalization of a fundamental result from real analysis (the triangle inequality) in a computer-checked format. The theorem `abs_add` is proven by appealing to a more basic lemma, `abs_add_le`, illustrating the hierarchical structure of mathematical knowledge in such systems.
* **How elements relate:** The window and its controls are merely the container. The core information is the single line of code, which itself has a clear structure: name, parameters, statement, and proof method. The proof method (`apply abs_add_le`) directly links this specific theorem to a broader mathematical framework.
* **Notable aspects:** The primary "anomaly" for a general viewer is that this is a *proof*, not just a statement. The `:= by apply...` portion is the critical component that transforms a mathematical claim into a verified fact within the system. The image contains no charts, graphs, or data tables; its entire informational value is contained in the precise textual code snippet.
</details>
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 multiple quantifiers and implications, as evidenced by C03S01.my_lemma3, which proves a complex statement involving bounds and absolute values with multiple quantifiers and conditions, and C03S05.MyAbs.abs_lt, which establishes that the absolute value of x being less than y is equivalent to $-y<x\land x<y$ .
<details>
<summary>extracted/6256159/carbon23.png Details</summary>
### Visual Description
\n
## Screenshot: Formal Mathematical Theorems in a Code Editor
### Overview
The image is a screenshot of a dark-themed code editor or terminal window displaying two formal mathematical theorems and their proofs, written in a language consistent with a theorem prover like Lean. The window has a standard macOS-style title bar with three colored control buttons (red, yellow, green) in the top-left corner. The content consists of two distinct theorem statements, each followed by a brief proof script.
### Components/Axes
* **Window Frame:** A dark gray rectangular window with rounded corners, centered on a light gray gradient background.
* **Window Controls:** Three circular buttons in the top-left corner of the window. From left to right: red (close), yellow (minimize), green (maximize/zoom).
* **Code Content Area:** The main dark area containing the text. The text uses syntax highlighting:
* Keywords (`theorem`, `by`, `apply`, `cases`, `exact`) are in a salmon/pink color.
* Theorem names (`my_lemma3`, `abs_lt`) are in a light blue/cyan color.
* Mathematical symbols and variables are in white or light gray.
* Specific symbols like `ε` (epsilon) and `ℝ` (real numbers) are highlighted in orange and purple, respectively.
* Logical connectives (`→`, `↔`, `∧`) and operators (`<`, `*`) are in a teal color.
### Detailed Analysis
The image contains two complete theorem statements and their proofs.
**1. Theorem `my_lemma3`**
* **Statement:** `∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε`
* **Proof:** `:= by apply C03S01.my_lemma`
* **Transcription & Translation:** The statement is in formal mathematical logic. It reads: "For all real numbers x, y, and epsilon, if epsilon is greater than 0, and epsilon is less than or equal to 1, and the absolute value of x is less than epsilon, and the absolute value of y is less than epsilon, then the absolute value of the product of x and y is less than epsilon." The proof applies a previously established lemma named `my_lemma` from a module or context `C03S01`.
**2. Theorem `abs_lt`**
* **Statement:** `|x| < y ↔ -y < x ∧ x < y`
* **Proof:** `:= by cases x exact abs_lt`
* **Transcription & Translation:** This is a fundamental property of absolute value. It states: "The absolute value of x is less than y if and only if negative y is less than x AND x is less than y." The proof uses a case analysis on `x` (likely considering `x ≥ 0` and `x < 0`) and then applies a previously defined fact or theorem named `abs_lt`.
### Key Observations
* **Formal Verification Context:** The syntax (`theorem ... := by ...`, `apply`, `cases`, `exact`) is characteristic of interactive theorem provers used in formal mathematics and software verification.
* **Proof Structure:** Both proofs are very concise, relying on applying existing lemmas (`C03S01.my_lemma`, `abs_lt`) rather than building the proof from basic axioms step-by-step. This suggests a hierarchical development where complex theorems are built upon simpler, previously proven ones.
* **Mathematical Content:** The first theorem (`my_lemma3`) is a specific bound on the product of two small numbers, with the additional constraint that epsilon is at most 1. The second (`abs_lt`) is a standard, foundational equivalence used to remove absolute value signs in inequalities.
* **Visual Layout:** The theorems are presented as two separate, clearly delineated blocks of code, each with its name, statement, and proof method.
### Interpretation
This screenshot captures a moment in the process of formalizing mathematics using a computer-assisted proof system. The theorems are not just stated; they are *defined* in a language a machine can check for logical correctness.
* **What the data suggests:** It demonstrates the use of a modular approach to building a mathematical library. Theorem `my_lemma3` depends on a lemma from a specific location (`C03S01`), indicating an organized codebase. The proof of `abs_lt` being used as a tactic name in its own proof is a curious detail that might indicate a naming convention or a recursive definition within the proof environment.
* **How elements relate:** The two theorems are logically independent but thematically related, both dealing with inequalities and absolute values. They represent different levels of complexity: `abs_lt` is a basic tool, while `my_lemma3` is a more specific result that might be used in an analysis context (e.g., proving continuity or limits).
* **Notable patterns/anomalies:** The most notable aspect is the extreme conciseness of the proofs. In a traditional written proof, these would require several lines of explanation. Here, the heavy lifting is done by the underlying proof framework and previously established facts, showcasing the power of formal verification systems to manage complex logical dependencies. The use of the same identifier `abs_lt` for both a theorem and a proof tactic is a minor but interesting syntactic feature of the specific proof language being used.
</details>
b) Set Theory and Relations: LeanAgent handles abstract set-theoretic concepts, as shown by C03S01.Subset.trans, which proves that subset relations are transitive.
<details>
<summary>extracted/6256159/carbon24.png Details</summary>
### Visual Description
## Code Snippet: Lean 4 Theorem Proof
### Overview
The image is a screenshot of a code editor or terminal window displaying a single line of formal mathematics written in the Lean 4 programming language and theorem prover. The code defines a theorem about the transitivity of the subset relation and provides its proof.
### Components/Axes
The image consists of a single, dark-themed window pane centered on a light gray background.
* **Window Controls:** In the top-left corner of the dark pane are three circular window control buttons, colored (from left to right) red, yellow, and green.
* **Code Content:** The main content is a single line of code with syntax highlighting. The text is rendered in a monospaced font.
* **Language:** The code is written in **Lean 4**.
### Detailed Analysis
The code text is transcribed below. Colors are noted in brackets to describe the syntax highlighting.
**Full Code Transcription:**
```
theorem Subset.trans : r ⊆ s → s ⊆ t → r ⊆ t := by
exact Set.Subset.trans
```
**Color-Coded Breakdown:**
* `theorem` (purple keyword)
* `Subset.trans` (light blue for the theorem name)
* `:` (white colon)
* `r ⊆ s → s ⊆ t → r ⊆ t` (light blue for variables `r`, `s`, `t`; red for the subset symbol `⊆` and the implication arrow `→`)
* `:=` (white definition symbol)
* `by` (purple keyword)
* `exact` (purple keyword)
* `Set.Subset.trans` (light blue for the reference to an existing theorem in the `Set` library)
### Key Observations
1. **Syntax Highlighting:** The code uses a distinct color scheme to differentiate between keywords (purple), identifiers/names (light blue), and operators (red/white).
2. **Theorem Statement:** The theorem is named `Subset.trans`. Its type is `r ⊆ s → s ⊆ t → r ⊆ t`, which is a logical statement: "If `r` is a subset of `s` and `s` is a subset of `t`, then `r` is a subset of `t`."
3. **Proof Method:** The proof is given after `:= by`. It uses the `exact` tactic, which means the proof is simply a direct application of an existing, pre-proven theorem named `Set.Subset.trans` from Lean's standard library.
4. **Layout:** The proof line (`exact Set.Subset.trans`) is indented beneath the theorem statement, following standard formatting for Lean proofs.
### Interpretation
This image captures a fundamental moment in formal mathematics and software verification. It demonstrates the process of **defining a reusable mathematical property** (the transitivity of subsets) and **proving it by referencing established foundations**.
* **What it represents:** The code is not performing a calculation but is making a formal, machine-checkable assertion about set theory. The theorem `Subset.trans` encapsulates a basic logical truth.
* **How it works:** The proof is elegantly simple because it delegates the logical work to a more fundamental theorem (`Set.Subset.trans`) that is already part of the trusted code base (the standard library). This exemplifies the building-block nature of formal proofs.
* **Significance:** Snippets like this are the atoms of larger formal verification projects. By composing such small, proven theorems, developers and mathematicians can construct complex, unassailable proofs about software correctness, hardware design, or mathematical conjectures. The image is a visual representation of **rigorous, computer-assisted reasoning**.
</details>
Now, only 2/7 sorry theorems from Mathematics in Lean Source are from the exercise file for proving identities about algebraic structures. This suggests that lifelong learning allowed LeanAgent to transition to gaining a stronger ability to work with premises for more complicated proofs.
We gain some insights from comparing the performance of LeanAgent over time on Mathematics in Lean Source to other setups. For example, the fact that ReProver can handle harder theorems out of the box, such as C03S01.my_lemma3, but fewer theorems overall suggests that it has a broader knowledge base initially but loses performance from a lack of adaptability. Furthermore, Setup 5 proves the same sorry theorems as LeanAgent does during lifelong learning. This suggests that pure curriculum learning without EWC or the Merge All strategy emphasizes grasping easier concepts earlier. This mimics the insights gained from the lifelong learning analysis. However, Setups 3 and 7 (curriculum with EWC and/or Merge All) demonstrate some knowledge plasticity, proving harder theorems during lifelong learning, such as C03S01.Subset.trans in Setup 3. However, this comes at the cost of proving basic theorems, showing catastrophic forgetting. For example, Setups 3 and 7 could not prove the trivial theorems MyGroup.mul_right_inv and MyRing.zero_mul, respectively, during lifelong learning, whereas LeanAgent could. This again aligns with the insights from the lifelong learning scores from our previous analysis.
By the end of lifelong learning, the sorry theorems that LeanAgent prove from Mathematics in Lean Source are a superset of those that the other setups prove. This shows that LeanAgent’s lifelong 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 C03S05.MyAbs.abs_lt. LeanAgent achieved this by using the available premises, such as abs_lt with a statement similar to C03S05.MyAbs.abs_lt.
An interesting case study can be found in the dichotomy between the theorems C03S05.MyAbs.neg_le_abs_self and C03S05.MyAbs.le_abs_self. LeanAgent can prove C03S05.MyAbs.neg_le_abs_self by referencing C03S05.MyAbs.le_abs_self, which is still unproven at that point:
<details>
<summary>extracted/6256159/carbon27.png Details</summary>
### Visual Description
## Code Snippet: Mathematical Theorem Proof
### Overview
The image displays a screenshot of a code editor or terminal window containing a single line of formal mathematical proof written in a programming language (likely a proof assistant such as Lean). The theorem proves a basic property of the absolute value function for real numbers.
### Components/Axes
* **Window Frame:** A dark-themed rectangular window with rounded corners, centered on a light gray background. The top-left corner contains three circular window control buttons (red, yellow, green).
* **Text Content:** A single line of code with syntax highlighting. The text is centered within the window.
* **Language:** The primary language is English, with embedded mathematical notation (symbols for real numbers, inequality, and absolute value).
### Detailed Analysis
**Transcription of Text:**
```
theorem neg_le_abs_self (x : ℝ) : -x ≤ |x| := by
simpa using C03S05.MyAbs.le_abs_self (-x)
```
**Breakdown of Components:**
1. **Theorem Declaration:** `theorem neg_le_abs_self`
* `theorem`: Keyword indicating the start of a theorem definition.
* `neg_le_abs_self`: The name of the theorem. It describes the property: the negative (`neg`) is less than or equal to (`le`) the absolute value of itself (`abs_self`).
2. **Parameters:** `(x : ℝ)`
* Declares a variable `x` of type `ℝ`. The symbol `ℝ` represents the set of real numbers.
3. **Proposition:** `: -x ≤ |x|`
* The mathematical statement being proven.
* `-x`: The additive inverse (negative) of `x`.
* `≤`: The "less than or equal to" inequality symbol.
* `|x|`: The absolute value of `x`.
4. **Proof Term:** `:= by`
* `:=`: Indicates the start of the proof or definition body.
* `by`: A tactic mode indicator, showing the proof will be constructed using tactics.
5. **Proof Tactic:** `simpa using C03S05.MyAbs.le_abs_self (-x)`
* `simpa`: A tactic (likely "simplify with manual pre-processing") used to automate parts of the proof.
* `using ...`: Specifies a lemma or previously proven theorem to use.
* `C03S05.MyAbs.le_abs_self`: The fully qualified name of a lemma. It suggests a lemma named `le_abs_self` located in a module or namespace `C03S05.MyAbs`.
* `(-x)`: The argument passed to the lemma. The lemma `le_abs_self` likely states that for any real number `y`, `y ≤ |y|`. Here, it is applied with `y = -x`.
### Key Observations
* **Syntax Highlighting:** The code uses color for readability:
* Keywords (`theorem`, `by`, `using`) are in a pinkish-red.
* The theorem name and tactic (`neg_le_abs_self`, `simpa`) are in a light yellow/gold.
* The type (`ℝ`) and the lemma path (`C03S05.MyAbs.le_abs_self`) are in a light blue/cyan.
* The mathematical symbols (`-`, `≤`, `|`, `(`, `)`) and punctuation are in white or light gray.
* **Proof Structure:** The proof is concise. It does not build the argument from first principles but instead relies on applying a more general, previously established lemma (`le_abs_self`) to the specific case where the input is `-x`. The `simpa` tactic handles the simplification needed to make this application work.
### Interpretation
This image captures a moment in formal verification or interactive theorem proving. The content is not just a mathematical statement but a **machine-checkable proof** of that statement.
* **Mathematical Meaning:** The theorem `neg_le_abs_self` asserts a fundamental property of real numbers: for any real number `x`, its negative (`-x`) is always less than or equal to its absolute value (`|x|`). This is intuitively true because the absolute value is always non-negative, while `-x` can be negative, zero, or positive. The case where `-x` is positive (when `x` is negative) is the non-trivial part, showing that the magnitude of a negative number is captured by its absolute value.
* **Logical Relationship:** The proof demonstrates a common pattern in formal mathematics: **reduction to a previously proven lemma**. The complex goal (`-x ≤ |x|`) is solved by invoking a general rule (`y ≤ |y|` for any `y`) and instantiating it with `y = -x`. The `simpa` tactic likely performs the algebraic manipulation to align the goal with the lemma's conclusion.
* **Contextual Clues:** The lemma's path (`C03S05.MyAbs.le_abs_self`) suggests this is part of a structured curriculum or library. `C03S05` could denote "Chapter 3, Section 5," and `MyAbs` likely refers to a custom-defined absolute value function or module. This indicates the theorem is being proven within a specific pedagogical or developmental framework.
* **Significance:** While the property is elementary, its formal proof is a building block. In a proof assistant, such basic theorems are essential for constructing more complex proofs in analysis, algebra, and other fields. The image exemplifies how human mathematical insight (recognizing the applicable lemma) is combined with automated reasoning (the `simpa` tactic) to create a rigorous, verifiable argument.
</details>
At the end of lifelong learning, LeanAgent can prove C03S05.MyAbs.le_abs_self:
<details>
<summary>extracted/6256159/carbon28.png Details</summary>
### Visual Description
## Screenshot: Code Snippet in a Themed Editor Window
### Overview
The image is a screenshot of a dark-themed code editor or terminal window displaying a single line of formal mathematical theorem and its proof script. The window is centered against a neutral, gradient gray background. The content is a code snippet written in what appears to be a formal proof language (likely Lean or a similar theorem prover), demonstrating a proof that a real number is less than or equal to its absolute value.
### Components/Axes
* **Window Frame:** A dark gray, rectangular window with rounded corners and a subtle drop shadow, giving it a floating appearance.
* **Window Controls:** Three circular buttons are positioned in the top-left corner of the window. From left to right, their colors are: red, yellow, and green. These are standard macOS-style window control buttons for closing, minimizing, and maximizing/full-screening.
* **Code Area:** The main content area of the window has a dark charcoal background (`#2d2d2d` approximate). The code is displayed in a monospaced font with syntax highlighting.
* **Background:** The area outside the window is a smooth, vertical gradient from a lighter gray at the top to a slightly darker gray at the bottom.
### Detailed Analysis / Content Details
The code is transcribed below with its syntax highlighting colors noted in brackets. The language is English with mathematical notation.
**Line 1:**
`theorem le_abs_self (x : ℝ) : x ≤ |x| := by`
* `theorem` (pink/red)
* `le_abs_self` (yellow/gold)
* `(x : ℝ)` (light blue for `x`, white for `:`, pink/red for `ℝ`)
* `:` (white)
* `x ≤ |x|` (light blue for `x` and `|x|`, white for `≤`)
* `:=` (white)
* `by` (pink/red)
**Line 2 (indented):**
` rw [le_abs]`
* `rw` (pink/red)
* `[le_abs]` (light blue)
**Line 3 (indented):**
` simp`
* `simp` (pink/red)
**Transcription (Plain Text):**
```
theorem le_abs_self (x : ℝ) : x ≤ |x| := by
rw [le_abs]
simp
```
### Key Observations
1. **Syntax Highlighting:** The code uses a distinct color scheme: keywords (`theorem`, `by`, `rw`, `simp`) are pink/red; the theorem name (`le_abs_self`) is yellow/gold; the type `ℝ` (real numbers) is pink/red; variables (`x`) and identifiers within brackets (`le_abs`) are light blue; structural symbols (`:`, `≤`, `:=`, `[]`) are white.
2. **Structure:** The proof is concise, consisting of a theorem declaration followed by two tactics (`rw` for rewrite, `simp` for simplification) on indented lines.
3. **Mathematical Content:** The theorem states a fundamental property of real numbers: for any real number `x`, `x` is less than or equal to its absolute value `|x|`. The proof leverages a previously defined lemma or rule named `le_abs`.
### Interpretation
This image captures a moment of formal verification in mathematics or computer science. The code is not just an assertion but a machine-checkable proof.
* **What it demonstrates:** It shows the formalization of an intuitive mathematical truth. The property `x ≤ |x|` is obvious from the definition of absolute value (which returns `x` if `x ≥ 0` and `-x` if `x < 0`), but here it is proven rigorously within a logical framework.
* **How elements relate:** The `theorem` keyword declares the goal. The `by` keyword initiates a proof block. The `rw [le_abs]` tactic likely rewrites the goal using a previously established lemma about absolute values (perhaps a definition or a case-split property). The `simp` tactic then simplifies the resulting expression, presumably to a trivial truth, completing the proof.
* **Notable aspects:** The extreme brevity of the proof (two tactics) highlights the power of the underlying proof assistant and its library. Complex properties can often be proven quickly by leveraging existing lemmas (`le_abs`). The clean, highlighted presentation is typical of modern development environments for formal methods, designed for readability and precision. This snippet is a building block; such theorems are foundational for more complex proofs in analysis, algebra, or verified software development.
</details>
It achieves this through its use of the le_abs premise, which provides conditions for when an 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 SciLean. These theorems primarily focus on:
a) Fundamental Algebraic Structures: LeanAgent proves basic algebraic operations and properties, such as SciLean.scalar_div_one, which proves that dividing any number by one yields the same number, SciLean.scalar_min_zero_one, which demonstrates the minimum value between 0 and 1 is 0, and Function.invFun.id_rule, which proves that the inverse of the identity function is the identity function itself.
<details>
<summary>extracted/6256159/carbon29.png Details</summary>
### Visual Description
## Code Snippet: Lean 4 Theorem Proofs
### Overview
The image is a screenshot of a code editor or terminal window displaying three mathematical theorem statements and their proofs written in the Lean 4 programming language and proof assistant. The window has a dark theme with syntax highlighting.
### Components/Axes
* **Window Frame:** A dark gray rectangular window with rounded corners, centered on a light gray background.
* **Title Bar:** Contains three colored circles (from left to right: red, yellow, green) in the top-left corner, typical of a macOS window control interface.
* **Main Content Area:** A dark charcoal background containing the code text. The text uses a monospaced font with syntax highlighting:
* Keywords (`theorem`, `by`, `simp`, `rw`, `apply`, `exact`) are in a salmon/pink color.
* Theorems names (`scalar_div_one`, `scalar_min_zero_one`, `id_rule`) are in a light blue/teal color.
* Variables (`x`, `R`, `X`) and function names (`min`, `invFun`, `Function.invFun_comp`, `Function.injective_id`) are in a light purple/lavender color.
* Operators (`:=`, `:`, `=`, `/`, `=>`) and punctuation are in a light gray or white color.
* Numeric literals (`0`, `1`) are in a light orange color.
### Detailed Analysis
The image contains three distinct theorem blocks. The language is Lean 4.
**1. Theorem: `scalar_div_one`**
* **Statement:** `theorem scalar_div_one (x : R) : x / 1 = x := by`
* **Proof:** `simp`
* **Transcription & Translation:**
* **Lean Code:** `theorem scalar_div_one (x : R) : x / 1 = x := by simp`
* **English Translation:** This theorem states that for any element `x` of type `R` (likely a ring or field), dividing `x` by the multiplicative identity `1` yields `x`. The proof is solved by the simplifier tactic (`simp`), which applies known simplification rules.
**2. Theorem: `scalar_min_zero_one`**
* **Statement:** `theorem scalar_min_zero_one : min (0 : R) (1 : R) = 0 := by`
* **Proof:**
* `rw [min_comm]`
* `simp`
* **Transcription & Translation:**
* **Lean Code:** `theorem scalar_min_zero_one : min (0 : R) (1 : R) = 0 := by rw [min_comm] simp`
* **English Translation:** This theorem states that the minimum of `0` and `1` (both explicitly typed as elements of `R`) is `0`. The proof first rewrites (`rw`) the goal using the commutativity of the minimum function (`min_comm`), which swaps the arguments, and then solves the resulting goal with the simplifier (`simp`).
**3. Theorem: `id_rule`**
* **Statement:** `theorem id_rule : invFun (fun (x : X) => x) = fun x => x := by`
* **Proof:**
* `apply Function.invFun_comp`
* `exact Function.injective_id`
* **Transcription & Translation:**
* **Lean Code:** `theorem id_rule : invFun (fun (x : X) => x) = fun x => x := by apply Function.invFun_comp exact Function.injective_id`
* **English Translation:** This theorem states that the inverse function (`invFun`) of the identity function on type `X` (`fun (x : X) => x`) is itself the identity function (`fun x => x`). The proof applies a lemma about the composition of a function with its inverse (`Function.invFun_comp`) and then provides the exact proof that the identity function is injective (`Function.injective_id`) to close the goal.
### Key Observations
* The code demonstrates basic properties in algebra (division by one, minimum of zero and one) and function theory (inverse of the identity function).
* The proofs are concise, leveraging built-in tactics (`simp`) and library lemmas (`min_comm`, `Function.invFun_comp`, `Function.injective_id`).
* The syntax highlighting is consistent, aiding readability by distinguishing language constructs from user-defined names.
* The theorems are named in a snake_case convention (`scalar_div_one`).
### Interpretation
This image is a technical artifact from the domain of formal verification and interactive theorem proving. It showcases how mathematical truths are encoded and proven within a dependently typed language like Lean 4.
* **What it demonstrates:** The theorems are foundational, almost axiomatic, statements. Their formal proof, even for simple facts like `x / 1 = x`, is crucial for building a reliable mathematical library. The `id_rule` theorem is fundamental in category theory and functional programming, establishing that the identity function is its own inverse.
* **How elements relate:** Each block follows the pattern: `theorem [name] : [statement] := by [proof script]`. The proof scripts show a hierarchy of automation: `simp` for simple algebraic facts, `rw` for rewriting with lemmas, and `apply`/`exact` for more structured, manual proof steps.
* **Notable patterns:** The use of type ascriptions (`(0 : R)`) in the second theorem ensures clarity and avoids ambiguity. The progression from a one-line `simp` proof to a two-step proof using a rewrite rule and then `simp` illustrates different proof strategies within the same system. The image serves as a clear example of the "source code" of formal mathematics.
</details>
b) Linear and Affine Maps: LeanAgent handles basic properties of linear and affine maps effectively, recognizing their structure in IsLinearMap.isLinearMap_apply, which proves the linearity of function applications, and IsAffineMap.IsAffineMap_apply, which demonstrates the affine property of function applications.
<details>
<summary>extracted/6256159/carbon30.png Details</summary>
### Visual Description
## Screenshot: Code Editor with Formal Proof Scripts
### Overview
The image is a screenshot of a dark-themed code editor window (resembling a macOS interface with red, yellow, and green window control dots in the top-left corner) displaying two formal mathematical theorem proofs. The text is written in a formal proof language, likely Lean 4 or a similar dependent type theory system, given the syntax and tactic names. The code is presented with syntax highlighting.
### Components/Axes
* **Window Frame:** A dark gray (#2d2d30 approx.) rectangular window with rounded corners, centered on a light gray background.
* **Window Controls:** Three colored circles (red, yellow, green) positioned horizontally in the top-left corner of the window.
* **Code Area:** The main content area of the window, containing two distinct theorem statements and their proofs.
* **Text & Syntax Highlighting:**
* Keywords (`theorem`, `by`, `constructor`, `simp`) are in a salmon/pink color.
* Identifiers and types (`isLinearMap_apply`, `IsLinearMap`, `R`, `fun`, `f`, `E`, `i`, `ι`) are in a light blue/cyan color.
* The proof tactic `aesop` is in a light orange color.
* The symbol `↦` (maps to) is used within the function definition.
* The symbol `→` (function type) is used in the type signature.
### Detailed Analysis
The image contains two complete theorem statements and their proofs.
**Theorem 1 (Top Block):**
* **Statement:** `theorem isLinearMap_apply (i : ι) : IsLinearMap R (fun f : (i : ι) → E i ↦ f i) := by`
* **Proof Tactic:** `constructor`
* **Proof Tactic:** `all_goals aesop`
**Theorem 2 (Bottom Block):**
* **Statement:** `theorem IsAffineMap_apply (i : ι) : IsAffineMap R (fun f : (i : ι) → E i ↦ f i) := by`
* **Proof Tactic:** `constructor`
* **Proof Tactic:** `constructor`
* **Proof Tactic:** `simp`
* **Proof Tactic:** `simp`
### Key Observations
1. **Structural Similarity:** Both theorems have an identical structure in their statement: they are parameterized by an index `i` of type `ι` (iota), and they assert a property (`IsLinearMap` or `IsAffineMap`) over a ring `R` for a specific function. The function in question is `fun f : (i : ι) → E i ↦ f i`, which appears to be the projection or evaluation map that takes a dependent function `f` (from an index `i` to a space `E i`) and returns its value `f i`.
2. **Proof Complexity:** The proof for `IsAffineMap_apply` is slightly more involved, requiring two `constructor` steps and two `simp` (simplification) steps, compared to the single `constructor` and a call to the automated tactic `aesop` for `isLinearMap_apply`.
3. **Language & Notation:** The language uses standard mathematical notation (`→`, `↦`, `ι`) embedded within a programming language syntax. The presence of tactics like `aesop` and `simp` is characteristic of modern interactive theorem provers.
### Interpretation
This screenshot captures a snippet from a formal mathematics library, likely dealing with functional analysis or linear algebra in a dependent type theory setting.
* **What the data demonstrates:** The theorems establish that the evaluation map (which extracts the `i`-th component from a dependent function space `Π i, E i`) is both a linear map and an affine map over a ring `R`. This is a fundamental, expected property in these mathematical structures.
* **How elements relate:** The two proofs are presented together, suggesting they are related lemmas, possibly part of a larger development on properties of dependent product spaces or map classifications. The simpler proof for the linear case might be a prerequisite or a more straightforward result.
* **Notable patterns/anomalies:** There are no anomalies; the proofs follow a logical and expected pattern. The use of `all_goals aesop` in the first proof indicates that after applying `constructor`, all remaining subgoals can be solved automatically by the `aesop` tactic, which is a powerful automated reasoning tool. The second proof requires more manual guidance with repeated `constructor` and `simp` tactics, indicating its goals are less immediately tractable for full automation in this context. The image provides pure factual code; its meaning is derived entirely from the semantics of the formal language it is written in.
</details>
c) Measure Theory Basics: LeanAgent starts grasping measure theory concepts, exemplified by SciLean.ite_pull_measureOf, which handles conditional measure selection between two measures based on a proposition, SciLean.Measure.prod_volume, which proves that the product of two volume measures is the volume measure itself, and SciLean.ite_pull_ennreal_toReal, which proves that conditionally pulling out an extended non-negative real and converting it to a real is equivalent to converting the individual components first.
<details>
<summary>extracted/6256159/carbon40.png Details</summary>
### Visual Description
## Code Screenshot: Lean 4 Theorem Proofs
### Overview
The image is a screenshot of a code editor window (dark theme) displaying three mathematical theorem statements and their proofs written in the Lean 4 programming language, a dependently typed functional programming language and proof assistant. The content is purely textual code; there are no charts, diagrams, or data visualizations. The text is presented with syntax highlighting.
### Components/Axes
The image contains a single component: a code editor window.
- **Window Controls**: Three colored circles (red, yellow, green) are positioned in the top-left corner, typical of a macOS window interface.
- **Code Content**: The main body contains three distinct theorem blocks. The text is monospaced and uses syntax highlighting:
- Keywords like `theorem`, `by` are in a salmon/pink color.
- Type names like `MeasurableSpace`, `Measure`, `ENNReal` are in a light blue/cyan.
- Identifiers and variables are in a light gray/white.
- Operators (`=`, `:=`, `:`, `<;>`) and punctuation are in white or light gray.
- **Background**: The editor has a dark gray background (`#2d2d2d` approximate). The window itself is centered on a lighter gray background.
### Detailed Analysis / Content Details
The following is a precise transcription of the textual content in the image. The language is **Lean 4**.
**Theorem 1: `ite_pull_measureOf`**
```lean
theorem ite_pull_measureOf {X} [MeasurableSpace X] (c : Prop) [Decidable c]
(μ ν : Measure X) (A : Set X) :
(if c then μ else ν) A
=
(if c then μ A else ν A) := by
split_ifs <;> rfl
```
* **Statement**: For a type `X` with a `MeasurableSpace`, a decidable proposition `c`, two measures `μ` and `ν` on `X`, and a set `A` in `X`, the measure of `A` under the conditionally chosen measure (`μ` if `c` is true, `ν` otherwise) is equal to the conditionally chosen value of the measure of `A` (`μ A` if `c` is true, `ν A` otherwise).
* **Proof**: The proof uses the tactic `split_ifs` to split the goal based on the condition `c`, followed by `rfl` (reflexivity) to close each subgoal.
**Theorem 2: `Measure.prod_volume`**
```lean
theorem Measure.prod_volume {X Y} [MeasureSpace X] [MeasureSpace Y] :
(Measure.prod (volume : Measure X) (volume : Measure Y)) = volume := by
rfl
```
* **Statement**: For types `X` and `Y` each with a `MeasureSpace`, the product measure of the `volume` measure on `X` and the `volume` measure on `Y` is equal to the `volume` measure (on the product space `X × Y`).
* **Proof**: The proof is by reflexivity (`rfl`), indicating this is likely a definitional equality or a previously established lemma.
**Theorem 3: `ite_pull_ennreal_toReal`**
```lean
theorem ite_pull_ennreal_toReal (c : Prop) [Decidable c] (x y : ENNReal) :
(if c then x else y).toReal
=
(if c then x.toReal else y.toReal) := by
split_ifs <;> rfl
```
* **Statement**: For a decidable proposition `c` and two extended non-negative real numbers (`ENNReal`) `x` and `y`, converting the conditionally chosen number (`x` if `c` is true, `y` otherwise) to a real number (`toReal`) is equal to the conditionally chosen conversion (`x.toReal` if `c` is true, `y.toReal` otherwise).
* **Proof**: Identical in structure to the first theorem: `split_ifs <;> rfl`.
### Key Observations
1. **Pattern**: Theorems 1 and 3 share an identical logical structure and proof tactic (`split_ifs <;> rfl`). They both "pull" an operation (`_A` for a measure, `.toReal`) out of a conditional (`if c then ... else ...`).
2. **Context**: The code is from the domain of **measure theory** and **formal verification**. It deals with concepts like measurable spaces, measures, product measures, and extended non-negative reals (`ENNReal`).
3. **Proof Style**: The proofs are extremely concise, relying on basic tactics (`rfl`, `split_ifs`), suggesting these are foundational or definitional lemmas within a larger library (likely Mathlib for Lean).
4. **Visual Layout**: The code is neatly formatted with consistent indentation. The theorems are separated by blank lines for clarity.
### Interpretation
This image does not present data for interpretation in the statistical sense. Instead, it presents **formal mathematical statements** within a proof assistant.
* **What it demonstrates**: The theorems establish basic, likely useful, properties for manipulating conditionals and measures/numbers in a formal setting. They ensure that applying an operation (like evaluating a measure on a set or converting an `ENNReal` to a `Real`) commutes with a conditional choice. This is crucial for simplifying proofs and definitions in formalized mathematics.
* **Relationship between elements**: The three theorems are independent but thematically related. The first and third are direct analogs of each other in different mathematical domains (measure theory vs. real analysis). The second theorem is a separate, fundamental property about product measures.
* **Significance**: In the context of formal verification (proving mathematical theorems with computer assistance), such lemmas are the essential "building blocks." They allow mathematicians and computer scientists to manipulate complex expressions step-by-step in a way that is guaranteed to be logically sound. The image captures a snippet of this meticulous, foundational work.
</details>
d) Floating-Point Operations: LeanAgent demonstrates an early grasp of floating-point representations and their correspondence to real numbers, shown by SciLean.re_float, proving that a floating-point number’s real-like part is itself.
<details>
<summary>extracted/6256159/carbon33.png Details</summary>
### Visual Description
\n
## Screenshot: Code Snippet in a Terminal/Editor Window
### Overview
The image displays a screenshot of a dark-themed code editor or terminal window containing a single line of code written in what appears to be a formal verification or theorem-proving language (likely Lean 4, based on syntax). The window is centered against a soft, gradient background.
### Components/Axes
* **Window Frame:** A dark gray, rectangular window with rounded corners and a subtle drop shadow, giving it a floating appearance.
* **Window Controls:** Three colored circular buttons are positioned in the top-left corner of the window frame. From left to right: red, yellow, green. These are standard macOS-style window control buttons for close, minimize, and maximize/zoom.
* **Code Content Area:** The main body of the window contains a single line of monospaced text with syntax highlighting.
* **Background:** The area surrounding the window is a smooth, gradient background transitioning from a lighter gray at the top to a slightly darker gray at the bottom.
### Detailed Analysis
**Text Transcription (Exact):**
```
theorem re_float (a : Float) : RCLike.re a = a := by
exact RCLike.re_eq_self_of_le le_rfl
```
**Syntax Highlighting & Formatting:**
* The text is rendered in a monospaced font.
* **Color Coding:**
* Keywords (`theorem`, `by`, `exact`) are in a salmon/pink color.
* The type `Float` is in a yellow/gold color.
* The theorem name (`re_float`), variable (`a`), and most other identifiers (`RCLike.re`, `RCLike.re_eq_self_of_le`, `le_rfl`) are in a light gray or off-white color.
* Operators and punctuation (`(`, `)`, `:`, `=`, `:=`) are in the same light gray color.
* The code is indented on the second line, indicating it is the proof script following the `:= by` keyword.
### Key Observations
1. **Language Identification:** The syntax (`theorem ... : ... := by`, `exact`) is characteristic of the Lean 4 theorem prover and programming language.
2. **Code Purpose:** The code defines a theorem named `re_float`. It asserts that for any term `a` of type `Float`, the expression `RCLike.re a` is equal to `a`.
3. **Proof Method:** The proof is completed in a single step using the `exact` tactic, applying a pre-existing lemma or theorem named `RCLike.re_eq_self_of_le` with the argument `le_rfl`.
4. **Contextual Inference:** The namespace `RCLike` suggests this is part of a library dealing with complex numbers or algebraic structures where `re` denotes the real part. The theorem states that the "real part" of a `Float` is the float itself, which is a tautology if `Float` is considered a subtype of real numbers.
### Interpretation
This image is a technical artifact from the domain of formal methods and dependent type theory. It captures a moment of formal verification where a programmer or mathematician has proven a basic property about floating-point numbers within a specific mathematical framework (`RCLike`).
* **What it demonstrates:** The snippet shows the conciseness and expressiveness of modern theorem-proving languages. A fundamental property is stated and proven in two lines. The use of `le_rfl` (likely short for "less-than-or-equal reflexivity") as an argument hints at the underlying logical structure, possibly relating to an ordering property of real numbers.
* **Relationship between elements:** The window controls and syntax highlighting are purely presentational, framing the core informational content: the formal statement and proof of a theorem. The code itself is the primary data.
* **Notable aspects:** The most significant observation is the *content* of the theorem. It is a foundational, almost trivial, statement. Its presence in a codebase likely serves as a building block for more complex proofs involving real numbers or complex analysis where `Float` is used as a concrete representation. The screenshot might be used in documentation, a tutorial, or a presentation to illustrate basic syntax or a specific library (`RCLike`).
</details>
The proofs during this phase are characteristically concise, often using basic tactics like simp, rfl, or aesop that do not use premises. This suggests that LeanAgent recognizes these theorems are 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:
a) Advanced Function Spaces: LeanAgent understands concepts in advanced function spaces, such as SciLean.ContCDiffMapFD_eta, which demonstrates the eta reduction property for continuously differentiable maps over finite dimensions.
<details>
<summary>extracted/6256159/carbon34.png Details</summary>
### Visual Description
\n
## Screenshot: Lean 4 Theorem Statement
### Overview
The image is a screenshot of a code editor or terminal window displaying a single theorem statement written in the Lean 4 proof assistant language. The window has a dark theme with syntax highlighting. The text is presented in a monospaced font against a dark gray background. The window itself is centered on a light gray background and features three colored window control buttons (red, yellow, green) in its top-left corner.
### Components/Axes
* **Window Frame:** A dark gray rectangular window with rounded corners and a subtle drop shadow.
* **Window Controls:** Three circular buttons in the top-left corner of the window, from left to right: red, yellow, green.
* **Code Content:** The primary content is a three-line block of code with syntax highlighting. The colors appear to be:
* Keywords (`theorem`, `by`, `simp`, `only`, `aesop`): Pink/Magenta.
* Theorem name (`ContCDiffMapFD_eta`): Light blue/cyan.
* Type constructors and certain identifiers (`FD[K,n]`, `DFunLike.ext_iff`): Yellow/Orange.
* Variables and other text (`f`, `X`, `Y`, `x`): Light gray/white.
* Punctuation and operators (`:`, `→`, `(`, `)`, `[`, `]`, `:=`): Light blue/cyan.
### Detailed Analysis / Content Details
The code is transcribed precisely below, preserving line breaks and indentation.
**Line 1:**
`theorem ContCDiffMapFD_eta (f : X →FD[K,n] Y) : (fun x ↦FD[K,n] f x) = f := by`
* **Theorem Declaration:** `theorem ContCDiffMapFD_eta`
* **Parameter:** `(f : X →FD[K,n] Y)` - Declares a variable `f` which is a function from type `X` to type `Y`, specifically a `FD[K,n]` map (likely denoting a class of continuously differentiable functions of order `n` with `K` as a coefficient or parameter).
* **Statement:** `(fun x ↦FD[K,n] f x) = f` - The theorem asserts that the function which takes an input `x` and applies `f` to it (with the `FD[K,n]` annotation) is equal to the original function `f`. This is an "eta-expansion" property.
* **Proof Start:** `:= by` - Indicates the beginning of the proof script.
**Line 2:**
` simp only [DFunLike.ext_iff]`
* **Proof Step:** An indented line containing the tactic `simp only [DFunLike.ext_iff]`.
* **Tactic:** `simp` is a simplification tactic.
* **Argument:** `only [DFunLike.ext_iff]` instructs the simplifier to use only the lemma `DFunLike.ext_iff`. This lemma likely states that two functions of a `DFunLike` type (a Lean typeclass for dependent function-like types) are equal if and only if they are equal for all inputs.
**Line 3:**
`aesop`
* **Proof Step:** A final, unindented line containing the tactic `aesop`.
* **Tactic:** `aesop` is an automated tactic that attempts to solve the goal using a predefined set of rules and strategies. In this context, after applying the simplification rule, `aesop` likely discharges the remaining, now trivial, goal.
### Key Observations
1. **Syntax Highlighting:** The code uses a consistent color scheme to distinguish language keywords, identifiers, and operators, aiding readability.
2. **Proof Structure:** The proof is concise, consisting of two tactics. The first (`simp`) reduces the goal to a simpler form using a specific extensionality lemma, and the second (`aesop`) automatically solves the simplified goal.
3. **Mathematical Content:** The theorem `ContCDiffMapFD_eta` formalizes a basic property of function equality in the context of a specific function type (`FD[K,n]`). It proves that explicitly wrapping a function call in a lambda abstraction is redundant.
### Interpretation
This image captures a snippet of formal mathematics being verified in a proof assistant. The theorem and its proof are not just text but machine-checked logical statements.
* **What it demonstrates:** The code proves a fundamental "eta-equivalence" property for a custom function type `FD[K,n]`. In simpler terms, it confirms that the system correctly recognizes that the operation `λx. f(x)` is identical to `f` itself for functions of this type. This is a basic sanity check and a necessary lemma for more complex proofs.
* **How elements relate:** The theorem statement defines the logical claim. The proof script (`simp only [DFunLike.ext_iff]` followed by `aesop`) provides the machine-verifiable evidence. The use of `DFunLike.ext_iff` suggests the `FD[K,n]` type is built upon Lean's standard dependent function type infrastructure.
* **Notable aspects:** The proof's brevity indicates that this property is considered straightforward within the formal system's library. The reliance on `aesop` for the final step shows the power of automation in modern proof assistants for handling routine logical steps once the correct simplification rule is applied. The screenshot itself is likely from a developer's environment, showing work in progress on a formalization project involving analysis or differential geometry.
</details>
b) Sophisticated Bijections: LeanAgent grows in its ability to work with product spaces and bijections, proving theorems such as Function.Bijective.Prod.mk.arg_fstsnd.Bijective_rule_simple’, which proves the bijectivity of a function that swaps elements in a product space and Function.Bijective.Equiv.invFun.arg_a0.Bijective_rule, which proves that the composition of a bijection and its inverse remains bijective. Crucially, these theorems might seem simple, but they demonstrate LeanAgent’s capability to handle abstract algebraic thinking.
<details>
<summary>extracted/6256159/carbon39.png Details</summary>
### Visual Description
## Screenshot: Code Editor with Formal Mathematical Proofs
### Overview
The image is a screenshot of a dark-themed code editor window displaying two formal mathematical theorem statements and their proofs. The code is written in a language that appears to be Lean 4 or a similar formal proof assistant, characterized by its syntax for defining theorems and constructing proofs using tactics. The window is centered on a light gray background.
### Components/Axes
* **Window Frame**: A dark gray rectangular window with rounded corners and a subtle drop shadow.
* **Title Bar**: Located at the top-left of the window, containing three colored circles (from left to right: red, yellow, green), typical of a macOS-style window control interface.
* **Content Area**: The main dark gray area containing the code text.
* **Text & Syntax Highlighting**: The code uses a monospaced font. Key elements are color-coded:
* Keywords (`theorem`, `by`, `constructor`, `intro`, `convert`, `simp`, `exact`) are in a light orange/peach color.
* Theorem names (`Prod.mk.arg_fstsnd.Bijective_rule_simple'`, `Equiv.invFun.arg_a0.Bijective_rule`) are in a pink/salmon color.
* Type annotations, function names, and other code are in a light gray/off-white color.
* The proof tactics and terms are indented under their respective theorem statements.
### Detailed Analysis
The content consists of two distinct theorem blocks.
**Theorem 1 (Top Block):**
* **Theorem Name**: `Prod.mk.arg_fstsnd.Bijective_rule_simple'`
* **Statement**: `Bijective (fun xy : X×Y => (xy.2, xy.1))`
* This asserts that the function which takes a pair `xy` from the product type `X×Y` and returns the swapped pair `(xy.2, xy.1)` is bijective (both injective and surjective).
* **Proof**: The proof is initiated with `:= by` and consists of two lines:
1. `constructor <;> intro h`
2. `all_goals aesop`
* This suggests a proof strategy that first breaks the `Bijective` goal into its injectivity and surjectivity components (`constructor`), introduces a hypothesis (`intro h`), and then uses an automated tactic (`aesop`) to solve all remaining subgoals.
**Theorem 2 (Bottom Block):**
* **Theorem Name**: `Equiv.invFun.arg_a0.Bijective_rule`
* **Parameters**:
* `(f : Y ≈ Z)`: An equivalence (bijection) between types `Y` and `Z`.
* `(g : X → Z)`: A function from type `X` to type `Z`.
* `(hf : Bijective g)`: A hypothesis that the function `g` is bijective.
* **Statement**: `Bijective (fun x => f.invFun (g x))`
* This asserts that the composition of the function `g` with the inverse function of the equivalence `f` (denoted `f.invFun`) is also bijective.
* **Proof**: The proof is initiated with `:= by` and consists of three lines:
1. `convert hf`
2. `simp [hf]`
3. `exact f.symm.bijective.comp hf`
* This proof strategy appears to convert the goal using the hypothesis `hf`, simplify it, and then provide an exact proof term leveraging the fact that the symmetric inverse of an equivalence (`f.symm`) is also bijective, and that the composition of bijective functions is bijective.
### Key Observations
1. **Language & Context**: The code is written in a formal proof language, almost certainly Lean 4, given the syntax (`≈` for equivalence, `invFun`, `bijective`, tactics like `aesop`).
2. **Purpose**: Both theorems establish rules for proving that certain constructed functions are bijective. The first deals with swapping components of a product, and the second deals with composing a function with the inverse of an equivalence.
3. **Proof Style**: The proofs are concise, relying heavily on automation (`aesop`) and existing lemmas (`f.symm.bijective.comp`), which is characteristic of modern interactive theorem proving.
4. **Visual Layout**: The two theorems are clearly separated by a blank line. The indentation of the proof steps provides a clear visual hierarchy.
### Interpretation
This screenshot captures a snippet of a formal mathematics or computer science library, likely focused on foundational type theory and equivalence relations. The theorems are "rules" or lemmas designed to be reused in larger proofs.
* **Theorem 1** formalizes the intuitive idea that swapping the elements of a pair is a reversible operation. This is a fundamental property in type theory and category theory.
* **Theorem 2** is a more general composition rule. It states that if you have a bijective function `g` from `X` to `Z`, and you "pull back" through a known bijection `f` from `Y` to `Z` (using `f`'s inverse), the resulting function from `X` to `Y` remains bijective. This is crucial for transporting properties across equivalences.
The presence of these specific, low-level lemmas suggests the code is part of a well-developed formalization effort, where such basic properties are established once and then used to build more complex results. The use of automated tactics indicates an emphasis on proof efficiency and reducing manual proof burden. The image contains no charts, data tables, or non-English text. All content is factual code and mathematical statements.
</details>
c) Abstract Algebraic Structures: LeanAgent proves further abstract algebraic properties, including SciLean.CDifferentiable.id_rule, which proves that the identity function is continuously differentiable.
<details>
<summary>extracted/6256159/carbon36.png Details</summary>
### Visual Description
## Code Snippet: Lean 4 Theorem Definition
### Overview
The image is a screenshot of a code editor window (likely on macOS, indicated by the three colored window control buttons) displaying a theorem definition written in the Lean 4 programming language and proof assistant. The code is from the `SciLean` library and proves a basic property of continuous differentiability for the identity function.
### Components/Axes
* **Window Frame:** A dark-themed editor window with a subtle drop shadow, set against a light gray gradient background.
* **Window Controls:** Three circular buttons in the top-left corner: red (close), yellow (minimize), and green (maximize/zoom).
* **Code Block:** The primary content area containing syntax-highlighted Lean 4 code.
* **Syntax Highlighting:** The code uses a color scheme:
* Keywords (`theorem`, `by`, `intro`, `unfold`, `tauto`): Light pink/salmon.
* Identifiers and types (`CDifferentiable`, `id_rule`, `K`, `fun`, `x`, `X`, `SciLean.CDifferentiableAt`): Light gray/white.
* Operators and punctuation (`:`, `=>`, `:=`): Light blue/cyan.
* The variable `x` within the function body is highlighted in yellow.
### Detailed Analysis
The complete transcribed code is as follows:
```lean
theorem CDifferentiable.id_rule : CDifferentiable K (fun x : X => x) := by
intro x
unfold SciLean.CDifferentiableAt
tauto
```
**Line-by-Line Breakdown:**
1. **Theorem Declaration:** `theorem CDifferentiable.id_rule : CDifferentiable K (fun x : X => x) := by`
* Declares a theorem named `id_rule` within the namespace `CDifferentiable`.
* The theorem's type is `CDifferentiable K (fun x : X => x)`. This asserts that the function `fun x : X => x` (the identity function mapping an element `x` of type `X` to itself) is continuously differentiable (`CDifferentiable`) with respect to a field or normed space `K`.
* The proof begins with `:= by`.
2. **Proof Tactic 1:** `intro x`
* Introduces an arbitrary point `x` of type `X` into the proof context. This corresponds to proving the statement "for all `x` in `X`".
3. **Proof Tactic 2:** `unfold SciLean.CDifferentiableAt`
* Unfolds (expands) the definition of the `SciLean.CDifferentiableAt` predicate. This likely reveals the underlying definition of what it means for a function to be continuously differentiable at a point.
4. **Proof Tactic 3:** `tauto`
* A tactic that solves goals which are tautologies (logically true statements). After unfolding the definition, the goal is presumably a logical statement that is trivially true for the identity function, allowing `tauto` to close the proof.
### Key Observations
* **Conciseness:** The proof is extremely short (three tactics), indicating that the theorem is a fundamental, almost definitional, property within the library.
* **Proof Structure:** It follows a common pattern in interactive theorem proving: introduce a variable, unfold a definition to expose the goal's structure, and then use an automated tactic to solve the resulting trivial logical statement.
* **Library Dependency:** The proof explicitly references `SciLean.CDifferentiableAt`, tying this theorem to the specific definitions and framework of the SciLean library.
### Interpretation
This code snippet demonstrates a foundational lemma in a formalized mathematics or scientific computing library. The theorem `CDifferentiable.id_rule` formally establishes that the identity function is continuously differentiable. This is a basic but essential building block for more complex proofs involving differentiation, such as proving the chain rule or the differentiability of composed functions.
The proof strategy is pedagogically clear: it reduces the abstract property of "continuous differentiability" to its core logical components by unfolding the library's definition. The use of `tauto` at the end confirms that, once the definition is expanded, the identity function's compliance with it is a matter of pure logic, requiring no intricate calculus. This snippet exemplifies how formal proof assistants like Lean are used to create a machine-checked, rigorous foundation for mathematical and computational theories.
</details>
d) Data Structures in Mathematics: LeanAgent navigates proofs involving array types in a mathematical context, proving theorems such as SciLean.ArrayType.ext, which proves that two arrays are equal if their elements are equal at all indices.
<details>
<summary>extracted/6256159/carbon37.png Details</summary>
### Visual Description
## Code Snippet: Lean Theorem Proof
### Overview
The image displays a screenshot of a code editor window containing a formal theorem statement and its proof in a language that appears to be Lean or a similar dependent type theory proof assistant. The code is presented in a dark-themed editor with syntax highlighting.
### Components/Axes
The image consists of a single, centered code block within a window frame.
1. **Window Frame:**
* A dark gray rectangular window with rounded corners.
* Top-left corner: Three colored window control dots (from left to right: red, yellow, green).
* The window is set against a light gray, slightly gradient background.
2. **Code Content:**
* The text is monospaced, typical for code editors.
* Syntax highlighting is applied:
* Keywords (`theorem`, `by`, `intro`, `apply`, `simp`, `only`) are in a salmon/pink color.
* The type `Cont` is in a teal/green color.
* The theorem name `ext` and the hypothesis name `h` are in the default text color (light gray/white).
* The proof term `SciLean.ArrayType.get_injective` is in the default text color.
* Logical symbols (`∀`, `→`, `:=`, `[`, `]`) and punctuation are in the default text color.
### Detailed Analysis / Content Details
The complete textual content of the code block is transcribed below. The language is English, with embedded mathematical notation.
**Line 1 (Theorem Statement):**
`theorem ext (x y : Cont) : (∀ i, x[i] = y[i]) → x = y := by`
* **Transcription:** `theorem ext (x y : Cont) : (∀ i, x[i] = y[i]) → x = y := by`
* **Breakdown:**
* `theorem ext`: Declares a theorem named `ext` (likely short for "extensionality").
* `(x y : Cont)`: Declares two variables, `x` and `y`, of type `Cont` (likely a type representing containers or arrays).
* `:`: Introduces the type/claim of the theorem.
* `(∀ i, x[i] = y[i])`: The premise/hypothesis. It states: "For all indices `i`, the element at index `i` in `x` is equal to the element at index `i` in `y`."
* `→`: Logical implication ("implies").
* `x = y`: The conclusion. It states: "Therefore, `x` is equal to `y`."
* `:= by`: Begins the proof script.
**Line 2 (Proof Step 1):**
` intro h`
* **Transcription:** ` intro h`
* **Breakdown:** This tactic introduces the hypothesis `(∀ i, x[i] = y[i])` into the context and names it `h`.
**Line 3 (Proof Step 2):**
` apply SciLean.ArrayType.get_injective`
* **Transcription:** ` apply SciLean.ArrayType.get_injective`
* **Breakdown:** This tactic applies a lemma or theorem named `get_injective` from the `SciLean.ArrayType` module. The name suggests this lemma states that the "get" operation (element access via index) is injective—meaning if two arrays have the same elements at all indices, they are the same array. This is precisely the extensionality principle being proven.
**Line 4 (Proof Step 3):**
` simp only [h]`
* **Transcription:** ` simp only [h]`
* **Breakdown:** This is a simplification tactic. `simp only [h]` tells the system to simplify the goal using *only* the hypothesis `h`. In this context, it likely discharges the remaining goal generated by the `apply` tactic by directly using the equality provided by `h`.
### Key Observations
1. **Proof Structure:** The proof is concise and follows a common pattern in proof assistants: introduce the hypothesis, apply a relevant lemma, and simplify.
2. **Underlying Library:** The reference to `SciLean.ArrayType` indicates this code is part of or depends on a library named "SciLean," which likely provides formalized mathematics and data structures for scientific computing in Lean.
3. **Theorem Purpose:** The theorem `ext` establishes **functional extensionality for the container type `Cont`**. It proves that two containers are equal if and only if all their elements are equal at every index. This is a fundamental property for reasoning about equality of arrays or similar data structures in formal verification.
4. **Visual Context:** The syntax highlighting and window controls suggest this is a screenshot from a modern code editor or IDE (like VS Code with a Lean extension) rather than a plain text document.
### Interpretation
This image captures a fundamental moment in formal mathematics and software verification. The theorem being proven is not just a line of code; it's a **machine-checked guarantee** about the behavior of a data structure.
* **What it demonstrates:** It shows the process of encoding a basic mathematical intuition—"two things are the same if all their parts are the same"—into a rigorous, computer-verifiable proof. The proof relies on a pre-existing lemma (`get_injective`), highlighting how formal systems build complex truths from simpler, previously established facts.
* **How elements relate:** The hypothesis `h` (the premise of element-wise equality) is the sole input to the proof. The `apply` tactic connects this specific instance to a general principle (injectivity of the getter function). The `simp` tactic then performs the final logical connection. The entire proof is a chain of dependency from the specific goal back to foundational axioms and lemmas.
* **Significance:** In the context of the SciLean library, this theorem is likely a cornerstone for proving more complex properties about scientific computations involving arrays. It ensures that when two arrays are observed to have identical contents, they can be treated as identical for all subsequent reasoning, preventing subtle bugs in verified software. The existence of such a theorem is a hallmark of a mature formalization effort, where basic properties are explicitly proven to support higher-level development.
</details>
LeanAgent proved this theorem about a traditionally computer-science-oriented data structure from a mathematical lens, which some other setups could not do.
The proofs at this stage are 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 to 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 integral manipulations to advanced function spaces indicates that LeanAgent is improving its premise selection over time. It learns to identify and apply more sophisticated mathematical structures and theorems as 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 lifelong learning setup provides it with continuously improving capabilities to reason about premises and proofs that outperform other setups.
Crucially, LeanAgent could prove re_float during lifelong learning while no 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 to process new and unique concepts from new repositories.
We gain some interesting insights from comparing the performance of LeanAgent over time on SciLean to other setups. For example, the fact that ReProver could not prove the trivial theorem SciLean.ite_pull_ennreal_toReal while LeanAgent could, even during lifelong learning, suggests that this baseline cannot handle foundational concepts. LeanAgent has a better grasp of these concepts from lifelong learning. This is due to the increased stability of LeanAgent and improvement from learning a new task, as shown in the lifelong learning metric analysis in Sec. 4.3.
Furthermore, an intriguing observation is that Setup 3 could prove Function.Bijective.Prod.mk.arg_fstsnd.Bijective_rule_simple’ during lifelong learning. However, as mentioned above, LeanAgent could only prove this theorem at the end of lifelong learning. This suggests that Setup 3 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 3 cannot prove the trivial measure theory theorem SciLean.Measure.prod_volume, whereas LeanAgent could during lifelong learning, again suggesting that it favors plasticity over stability.
An interesting case is that LeanAgent can prove SciLean.norm 2 _scalar during lifelong learning but not SciLean.norm2_scalar. Conversely, Setup 2 proved SciLean.norm2_scalar but not SciLean.norm 2 _scalar.
<details>
<summary>extracted/6256159/carbon64.png Details</summary>
### Visual Description
\n
## Code Screenshot: Lean Theorem Proofs for Scalar Norms
### Overview
The image is a screenshot of a code editor window (with macOS-style window controls) displaying two Lean theorem proofs. The code defines and proves two related properties about the norm of a scalar value within a type class `RealScalar`. The syntax highlighting suggests a modern Lean development environment, likely using the SciLean library.
### Components/Axes
* **Window Frame**: A dark-themed editor window with three colored dots (red, yellow, green) in the top-left corner, typical of a macOS interface.
* **Code Content**: Two distinct theorem blocks written in the Lean programming language/proof assistant.
* **Syntax Highlighting**:
* Keywords (`theorem`, `by`, `rw`, `symm`, `simp`, `congr`): Purple.
* Type classes and some identifiers (`RealScalar`, `Scalar`): Teal.
* Variables and standard text (`R`, `x`): White.
* Operators and symbols (`:=`, `^`, `₂`): Various colors including yellow and red.
* Library/Module names (`SciLean`): Light blue.
### Detailed Analysis
The code contains two theorems with identical names and signatures, which is unusual and may indicate an overload or a specific pedagogical example.
**Theorem 1 (Lines 1-3):**
```lean
theorem norm2_scalar {R} [RealScalar R] (x : R) :
‖x‖₂[R] = Scalar.abs x := by
rw [SciLean.scalar_norm]
```
* **Statement**: For a type `R` which is an instance of `RealScalar`, and an element `x` of type `R`, the L2 norm of `x` (denoted `‖x‖₂[R]`) is equal to the absolute value of `x` as defined in the `Scalar` structure (`Scalar.abs x`).
* **Proof**: The proof is a single tactic `rw` (rewrite) that applies a lemma named `scalar_norm` from the `SciLean` library. This suggests the library already contains a fundamental definition or lemma connecting the norm notation to the `Scalar.abs` function.
**Theorem 2 (Lines 5-10):**
```lean
theorem norm2_scalar {R} [RealScalar R] (x : R) :
‖x‖₂²[R] = x^2 := by
symm
simp [sq]
congr
simp
```
* **Statement**: For the same type `R` and element `x`, the *square* of the L2 norm of `x` (denoted `‖x‖₂²[R]`) is equal to `x` squared (`x^2`).
* **Proof**: The proof uses a sequence of tactics:
1. `symm`: Symmetrizes the goal, likely changing `‖x‖₂²[R] = x^2` to `x^2 = ‖x‖₂²[R]`.
2. `simp [sq]`: Simplifies the goal using the definition of `sq` (square).
3. `congr`: Applies congruence, breaking the goal into simpler subgoals based on the structure of the equality.
4. `simp`: Performs general simplification to close the remaining goal(s).
### Key Observations
1. **Duplicate Theorem Name**: Both theorems are named `norm2_scalar`. In Lean, this would typically cause an error unless they are in different namespaces or one is a local instance. This might be a simplified example for illustration.
2. **Proof Complexity**: The first proof is a direct rewrite, indicating a foundational lemma. The second proof is more involved, using symmetry and simplification, suggesting it derives the squared norm property from more basic principles (possibly including the first theorem).
3. **Notation**: The code uses specialized Unicode notation for norms (`‖...‖₂`) and subscripts (`₂`), common in mathematical formalization.
4. **Library Dependency**: The proof explicitly relies on the `SciLean` library, indicating this code is part of a larger scientific computing or formal mathematics project.
### Interpretation
This code snippet formalizes basic properties of scalar norms within a type-class-based algebraic hierarchy (`RealScalar`). The theorems establish that for a "real scalar" type, the L2 norm behaves as expected: its value is the absolute value, and its square is the square of the element.
The first theorem (`‖x‖₂[R] = Scalar.abs x`) acts as a definitional bridge, connecting the abstract norm notation to a concrete function (`Scalar.abs`). The second theorem builds upon this to prove a computationally useful property (`‖x‖₂²[R] = x^2`), which is fundamental in areas like optimization, physics, and machine learning where squared norms are frequently used.
The presence of the `SciLean` library suggests this is not just a theoretical exercise but part of a practical framework for verified scientific computing. The concise proofs demonstrate the power of tactic-based theorem proving: leveraging existing library lemmas (`scalar_norm`) and automated simplifiers (`simp`) to establish results with minimal manual effort. The duplicate naming, while potentially problematic in a real codebase, might be intentional here to show two different proof strategies for closely related statements.
</details>
Setup 2 uses the sq premise from mathlib4, which states that the square of an element is the same as multiplying that element by itself, while LeanAgent used the SciLean.scalar_norm 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 to 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 a sorry theorem from PFR. We can prove condRho_of_translate, which states a form of a translation invariance property of randomness measures.
<details>
<summary>extracted/6256159/carbon44.png Details</summary>
### Visual Description
## Code Snippet: Lean 4 Mathematical Lemma
### Overview
The image displays a screenshot of a code editor window (dark theme, macOS-style traffic light buttons in the top-left) containing a single mathematical lemma written in the Lean 4 proof assistant language. The lemma concerns the invariance of a conditional rho function (`condRho`) under translation of one of its arguments.
### Components/Axes
* **Window Frame**: A dark gray (`#2d2d2d` approximate) rectangular window with rounded corners, centered on a light gray (`#b0b8c4` approximate) background.
* **Window Controls**: Three circular buttons in the top-left corner of the window, from left to right: red, yellow, green.
* **Code Content**: Monospaced text with syntax highlighting. The primary text color is a light gray/off-white. Keywords (`lemma`, `by`, `simp`) are highlighted in a pink/magenta color. Type names (`Type*`, `MeasureSpace`, `Finset`, `G`, `S`) are in a light blue. The proof tactic `simp` and its arguments are in a purple/violet shade.
### Detailed Analysis / Content Details
The code is a single, complete Lean 4 lemma and its proof. The transcription is as follows:
```lean
lemma condRho_of_translate {Ω S : Type*} [MeasureSpace Ω] (X : Ω → G) (Y : Ω → S)
(A : Finset G) (s:G) : condRho (fun ω ↦ X ω + s) Y A = condRho X Y A := by
simp only [condRho, rho_of_translate]
```
**Breakdown of the Statement:**
1. **Lemma Name**: `condRho_of_translate`
2. **Implicit Parameters**: `{Ω S : Type*}` - Declares `Ω` and `S` as arbitrary types.
3. **Type Class Instance**: `[MeasureSpace Ω]` - Assumes `Ω` is equipped with a measure space structure.
4. **Function Parameters**:
* `(X : Ω → G)`: A function `X` from `Ω` to an additive group `G`.
* `(Y : Ω → S)`: A function `Y` from `Ω` to type `S`.
5. **Additional Parameters**:
* `(A : Finset G)`: A finite subset `A` of the group `G`.
* `(s:G)`: An element `s` of the group `G`.
6. **Main Claim (Theorem)**: `condRho (fun ω ↦ X ω + s) Y A = condRho X Y A`
* This states that the conditional rho function (`condRho`) applied to the *translated* function `(fun ω ↦ X ω + s)` (which adds the constant `s` to each output of `X`) is equal to `condRho` applied to the original function `X`, given the same `Y` and `A`.
7. **Proof**: `:= by simp only [condRho, rho_of_translate]`
* The proof is a single tactic call. It uses the simplifier (`simp`) with only the specified lemmas: the definition of `condRho` and a lemma named `rho_of_translate`. This suggests the result follows directly from unfolding definitions and applying a previously proven lemma about rho and translation.
### Key Observations
* **Syntactic Precision**: The code uses precise Lean 4 syntax, including the Unicode arrow `→`, the maps-to symbol `↦`, and the colon `:` for type annotations.
* **Proof Brevity**: The proof is extremely concise, indicating the result is likely a straightforward consequence of more fundamental definitions and lemmas within the formalized theory.
* **Contextual Clues**: The names `condRho`, `rho_of_translate`, `MeasureSpace`, and `Finset` strongly suggest this lemma is part of a formalization of measure theory or probability theory, possibly involving group actions or invariant measures.
### Interpretation
This image captures a formal mathematical statement and its machine-checked proof. The lemma asserts a specific **invariance property**: the value of the `condRho` function does not change when its first functional argument (`X`) is uniformly translated by a group element `s`. This is a common type of lemma in areas like ergodic theory or the study of invariant measures, where properties are expected to be unchanged under group actions.
The proof strategy (`simp only [condRho, rho_of_translate]`) reveals the logical dependency: the property is not proven from first principles here but is derived by combining the definition of `condRho` with a pre-existing lemma (`rho_of_translate`) that likely establishes a more general or foundational relationship between rho functions and translation. This exemplifies the hierarchical and reusable nature of formalized mathematics. The screenshot itself serves as a record of this verified mathematical fact within a specific digital environment.
</details>
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 rho_of_translate lemma). The fact that LeanAgent could trivially identify such a 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 to 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.
Alternate PFR Commit. We also analyze whether LeanAgent can generalize to a different commit of a repository in the curriculum. We choose commit 861715b9bf9482d2442760169cb2a3ff54091f75, because PFR/RhoFunctional.lean, the file from which we proved condRho_of_translate in the newer commit, did not exist in the old commit. This allowed the sorry theorems in the old commit to be more distinct. It proved two theorems, including the theorem multiDist_copy about the equality of distributions when copying random variables across different measure spaces that ReProver could not. LeanAgent achieved this with just the tactic rfl. However, these statements were about multiDist, another sorry theorem. Since any two instances of sorry are automatically equal by rfl, LeanAgent exploits this technicality to prove the two theorems.
<details>
<summary>extracted/6256159/carbon45.png Details</summary>
### Visual Description
## Code Screenshot: Formal Mathematical Lemmas
### Overview
The image displays a screenshot of a code editor window (dark theme, macOS-style traffic light buttons in the top-left) containing two formal lemma definitions written in a dependently-typed proof language, likely Lean 4 or a similar system. The code is syntax-highlighted. The content is purely textual and mathematical; there are no charts, graphs, or diagrams with data trends.
### Components/Axes
* **Window Frame:** A dark gray rounded rectangle with a subtle drop shadow, set against a light gray-blue background.
* **Window Controls:** Three colored circles (red, yellow, green) in the top-left corner, typical of a macOS window.
* **Code Content:** Two distinct blocks of code, each defining a `lemma`. The text uses a monospaced font with syntax highlighting:
* Keywords (`lemma`, `by`) are in a pink/red color.
* Type names (`Type*`, `MeasureSpace`, `Fin`, `Equiv.Perm`) are in green.
* Variables and identifiers are in white/light gray.
* The proof term `rfl` is in blue.
* Mathematical symbols (`ℕ`, `→`, `∀`, `↦`, `:=`) are rendered as part of the code.
### Detailed Analysis / Content Details
The image contains two complete lemma statements and their proofs.
**Lemma 1: `multiDist_copy`**
* **Declaration:** `lemma multiDist_copy {m:ℕ} {Ω : Fin m → Type*} {Ω' : Fin m → Type*}`
* **Hypotheses:**
* `(hΩ : (i : Fin m) → MeasureSpace (Ω i))`
* `(hΩ': (i : Fin m) → MeasureSpace (Ω' i)) (X : (i : Fin m) → (Ω i) → G)`
* `(X' : (i : Fin m) → (Ω' i) → G)`
* `(hident: ∀ i, IdentDistrib (X i) (X' i) (hΩ i).volume (hΩ' i).volume) :`
* **Conclusion:** `D[X ; hΩ] = D[X' ; hΩ']`
* **Proof:** `:= by rfl`
**Lemma 2: `multiDist_of_perm`**
* **Declaration:** `lemma multiDist_of_perm {m:ℕ} {Ω : Fin m → Type*}`
* **Hypotheses:**
* `(hΩ : (i : Fin m) → MeasureSpace (Ω i))`
* `(X : (i : Fin m) → (Ω i) → G) (φ : Equiv.Perm (Fin m)) :`
* **Conclusion:** `D[X ; hΩ] = D[fun i ↦ X (φ i); fun i ↦ hΩ (φ i)]`
* **Proof:** `:= by rfl`
### Key Observations
1. **Formal Proof Context:** The code is from a formal verification or proof assistant environment. The `:= by rfl` tactic indicates both lemmas are proven by reflexivity, meaning the equality is definitionally true.
2. **Mathematical Subject:** The lemmas concern measure theory and probability. Key concepts include:
* `MeasureSpace`: A space equipped with a measure.
* `IdentDistrib`: A predicate stating two random variables have identical distributions.
* `D[... ; ...]`: Likely denotes a multi-dimensional distribution or a divergence measure (e.g., differential entropy, KL divergence) constructed from a family of random variables `X` over product spaces defined by `Ω`.
* `Equiv.Perm (Fin m)`: A permutation on a finite set of `m` elements.
3. **Lemma Purpose:**
* `multiDist_copy`: Asserts that the quantity `D` is invariant if each random variable `X i` is replaced by an identically distributed copy `X' i` (with respect to their respective measure spaces).
* `multiDist_of_perm`: Asserts that `D` is invariant under a simultaneous permutation of the indices of both the random variables `X` and the measure spaces `hΩ`.
### Interpretation
This image captures a snippet of formalized mathematics, specifically within the realm of measure-theoretic probability. The lemmas establish foundational invariance properties for a mathematical object `D` defined over a collection of random variables.
* **What it demonstrates:** The code proves that the object `D` depends only on the *joint distribution* of the family of random variables `(X i)`, not on the specific underlying probability spaces `(Ω i, hΩ i)` or their labeling order. The first lemma (`multiDist_copy`) shows invariance under replacing variables with identically distributed ones. The second (`multiDist_of_perm`) shows invariance under relabeling the components via a permutation.
* **Why it matters:** Such properties are crucial for ensuring that a defined quantity (like a multi-information measure, a divergence, or an entropy) is well-defined on the space of distributions and not an artifact of a particular representation. The use of a proof assistant guarantees these properties hold with mathematical rigor.
* **Notable aspect:** The proofs are trivial (`rfl`), suggesting that the definition of `D` is constructed in such a way that these equalities hold by definition or by very basic properties of the underlying constructs (like `IdentDistrib`). The real work likely lies in the definitions that precede these lemmas, which are not shown.
</details>
This commit also provides another interesting example. The PFR maintainers used 0 = 1 as a placeholder for some sorry theorems, five of which are multiTau_min_exists, multiTau_min_sum_le, sub_multiDistance_le, sub_condMultiDistance_le, sub_condMultiDistance_le’. Interestingly, LeanAgent finds unintended constructs and proves these theorems with this proof:
<details>
<summary>extracted/6256159/carbon46.png Details</summary>
### Visual Description
## Screenshot: Formal Proof Script in Lean
### Overview
The image is a screenshot of a dark-themed code editor or terminal window displaying a short proof script written in the Lean theorem prover language. The script defines a lemma with a deliberately contradictory statement (`0 = 1`) and provides a proof that appears to be valid within a specific, non-trivial mathematical context.
### Components/Axes
* **Window Frame:** A dark gray, rounded rectangle window with a subtle drop shadow, set against a light gray gradient background.
* **Window Controls:** Three colored circles in the top-left corner of the window, from left to right: red, yellow, green. These are standard macOS-style window control buttons.
* **Code Block:** The main content area containing monospaced text with syntax highlighting. The text is left-aligned with indentation for proof steps.
### Detailed Analysis / Content Details
The following text is present in the code block, transcribed exactly as shown:
```
lemma multiTau_min_exists : 0 = 1 := by
nontriviality
simp
apply @zero_ne_one ℕ _
exact multidist_eq_zero
```
**Line-by-Line Transcription & Explanation:**
1. `lemma multiTau_min_exists : 0 = 1 := by`
* **Lemma Name:** `multiTau_min_exists`
* **Statement:** `0 = 1` (This is the proposition being proved).
* **Proof Start:** `:= by` indicates the beginning of the proof script.
2. ` nontriviality`
* **Tactic:** `nontriviality`. This is a specialized tactic, likely from a library dealing with algebraic structures. It works by proving the current goal under the assumption that the underlying type/structure is non-trivial (i.e., not all elements are equal).
3. ` simp`
* **Tactic:** `simp`. A standard simplification tactic that applies known rewrite rules and lemmas to simplify the goal.
4. ` apply @zero_ne_one ℕ _`
* **Tactic:** `apply`. Applies a lemma or theorem to the current goal.
* **Lemma Applied:** `@zero_ne_one`. This is a standard lemma stating that zero is not equal to one (`0 ≠ 1`).
* **Arguments:** `ℕ` specifies the type as the natural numbers. The underscore `_` is a placeholder for an implicit argument, likely a proof that the structure is non-trivial, which was established by the `nontriviality` tactic.
5. ` exact multidist_eq_zero`
* **Tactic:** `exact`. Provides a exact proof term to close the goal.
* **Proof Term:** `multidist_eq_zero`. This appears to be a lemma or hypothesis specific to the context of the proof (possibly related to a "multi-tau" or "multidistance" function), stating that some distance measure is equal to zero.
**Language:** The programming/proving language is **Lean**. The symbol `ℕ` is the Unicode character for the set of natural numbers (U+2115).
### Key Observations
1. **Contradictory Goal:** The lemma statement `0 = 1` is a logical contradiction in standard arithmetic. The proof's validity hinges entirely on the context established by `nontriviality` and the specific meaning of `multidist_eq_zero`.
2. **Proof Structure:** The proof is very concise (4 tactic steps). It uses a high-level algebraic tactic (`nontriviality`) to set up a context, then appears to derive a contradiction (`zero_ne_one`) from a specific property (`multidist_eq_zero`).
3. **Syntax Highlighting:** Keywords (`lemma`, `by`, `nontriviality`, `simp`, `apply`, `exact`) are highlighted in a yellow/gold color. The rest of the text is in a light gray/white. The symbol `ℕ` is also highlighted.
4. **Visual Style:** The window uses a dark theme (similar to "One Dark" or "Dracula") with a monospaced font, typical for code editors.
### Interpretation
This screenshot captures a moment of formal reasoning that is likely **pedagogical, humorous, or context-specific**.
* **What it demonstrates:** It shows how a theorem prover like Lean can be used to construct a proof of a false statement (`0 = 1`) by operating within a specific, non-standard context. The `nontriviality` tactic is key here; it allows the proof to proceed by assuming the underlying mathematical structure is not the trivial one-element structure (where `0 = 1` is true). The proof then likely uses a specialized definition (`multidist_eq_zero`) from that non-trivial context to force the contradiction.
* **Why it matters:** It highlights the importance of **context and axioms** in formal systems. A proof is only as sound as its underlying assumptions. This could be an example used to teach about:
* The power and potential pitfalls of automated tactics.
* The concept of vacuous truth or proofs in non-trivial structures.
* The specific library or theory being developed (where `multidist_eq_zero` has a particular meaning).
* **Underlying Message:** The image is a meta-commentary on formal verification itself. It playfully shows that even "obviously false" statements can be "proven" if one manipulates the context and definitions appropriately, underscoring the need for careful foundational work. It's the formal logic equivalent of a programmer writing a function that proves `False` by exploiting a type system loophole.
</details>
It combines the known fact that $0\neq 1$ with the placeholder theorem multidist_eq_zero, which states $0=1$ . As such, it proves False, allowing it to derive anything, including $0=1$ .
MiniF2F. This repository consists of a 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 a framework, not a model, quantitatively comparing it with existing methods using a Pass@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, we append MiniF2F to the initial curriculum to demonstrate the use case of formalizing a new repository in parallel with the ones in 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 to lifelong learning.
ReProver initially demonstrated proficiency in a range of foundational mathematical areas on MiniF2F:
a) Basic Arithmetic and Number Theory: ReProver could handle simple arithmetic and modular arithmetic problems, such as mathd_numbertheory_254, a theorem about modular arithmetic and basic addition, mathd_numbertheory_342, a theorem about basic divisibility, and mathd_algebra_304, a theorem about simple exponentiation. These proofs only rely on the norm_num tactic, which evaluates arithmetic expressions. This suggests a less sophisticated proving ability of mathematics at the start of lifelong learning.
<details>
<summary>extracted/6256159/carbon47.png Details</summary>
### Visual Description
## Screenshot: Code Editor with Mathematical Theorems
### Overview
The image is a screenshot of a dark-themed code editor or terminal window, displaying three lines of formal mathematical statements written in a proof assistant language (likely Lean). Each line defines a theorem with a name, a mathematical equation, and a proof tactic. The window has a minimalist design with macOS-style window controls in the top-left corner.
### Components/Axes
* **Window Frame**: A dark gray rectangular window with rounded corners, centered on a lighter gray background.
* **Window Controls**: Three colored circles in the top-left corner of the window:
* Red (left)
* Yellow (center)
* Green (right)
* **Text Content**: Three distinct theorem statements, each formatted on a single line with syntax highlighting. The text is in a monospaced font.
* **Syntax Highlighting**:
* The keyword `theorem` is in a yellow/gold color.
* Theorem names (e.g., `mathd_numbertheory_254`) are in a light gray/white color.
* Mathematical expressions and numbers are in a light green color.
* The proof tactic `:= by norm_num` is in a muted, darker gray color.
### Detailed Analysis / Content Details
The image contains three precise mathematical statements. All text is in English, using standard mathematical notation.
1. **Theorem 1 (Top Line)**
* **Full Text**: `theorem mathd_numbertheory_254 : (239 + 174 + 83) % 10 = 6 := by norm_num`
* **Mathematical Statement**: The sum of 239, 174, and 83, modulo 10, equals 6.
* **Verification**: (239 + 174 + 83) = 496. 496 % 10 = 6. The statement is arithmetically correct.
2. **Theorem 2 (Middle Line)**
* **Full Text**: `theorem mathd_numbertheory_342 : 54 % 6 = 0 := by norm_num`
* **Mathematical Statement**: 54 modulo 6 equals 0.
* **Verification**: 54 ÷ 6 = 9 with a remainder of 0. The statement is arithmetically correct.
3. **Theorem 3 (Bottom Line)**
* **Full Text**: `theorem mathd_algebra_304 : 91^2 = 8281 := by norm_num`
* **Mathematical Statement**: 91 squared equals 8281.
* **Verification**: 91 * 91 = 8281. The statement is arithmetically correct.
### Key Observations
* **Structure**: Each theorem follows an identical syntactic pattern: `theorem [name] : [equation] := by norm_num`.
* **Naming Convention**: The theorem names suggest they are part of a structured dataset (`mathd`), categorized by field (`numbertheory`, `algebra`) and numbered (`254`, `342`, `304`).
* **Proof Tactic**: The repeated use of `:= by norm_num` indicates that each proof is completed by an automated tactic designed to verify numerical computations.
* **Visual Layout**: The text is left-aligned with consistent indentation for the proof tactic on the following line (though in this screenshot, the tactic appears on the same line for all three). The syntax highlighting creates a clear visual separation between keywords, identifiers, and mathematical content.
### Interpretation
This screenshot captures a snippet from a formal mathematics or automated theorem-proving environment. The content demonstrates the verification of basic arithmetic and algebraic facts within a rigorous, computer-checked framework.
* **Purpose**: These theorems are likely entries from a benchmark dataset (such as the `mathd` dataset) used to train or evaluate the capabilities of AI systems in formal reasoning and mathematics. The `norm_num` tactic is a common component in proof assistants like Lean for handling routine numerical calculations.
* **Significance**: The image illustrates how foundational mathematical truths are encoded and verified computationally. It highlights the intersection of computer science and pure mathematics, where logical statements are not just asserted but formally proven by machine.
* **Context**: The clean, focused presentation suggests this is a view from a developer or researcher working on formal verification, symbolic AI, or mathematical knowledge bases. The macOS-style window controls hint at the user's operating system environment.
</details>
b) Elementary Algebra: ReProver could solve basic algebraic equations and perform straightforward manipulations, such as mathd_algebra_141, which proves a statement about quadratic expressions, mathd_algebra_329, which shows a grasp of systems of linear equations, and mathd_algebra_547, which proves basic algebraic manipulation with roots.
<details>
<summary>extracted/6256159/carbon48.png Details</summary>
### Visual Description
## Code Screenshot: Lean 4 Mathematical Theorems
### Overview
The image is a screenshot of a code editor window displaying three mathematical theorem statements and their proofs written in the Lean 4 theorem prover syntax. The code is presented with syntax highlighting on a dark background. The window has the standard macOS-style traffic light buttons (red, yellow, green) in the top-left corner.
### Components/Axes
* **Window Frame**: A dark gray rounded rectangle containing the code.
* **Traffic Light Buttons**: Three colored circles (red, yellow, green) positioned horizontally in the top-left corner of the window frame.
* **Code Content**: Three distinct theorem blocks, each following a similar structure: a theorem name, variable declarations, hypotheses, a goal statement, and a proof tactic.
* **Syntax Highlighting**:
* Keywords (`theorem`, `by`, `nlinarith`, `linarith`, `simp`, `rw`) are in a pinkish-red color.
* Theorem names (`mathd_algebra_141`, etc.) are in a light orange/peach color.
* Variable names (`a`, `b`, `x`, `y`) and hypothesis labels (`h₀`, `h₁`, `h₂`) are in a light blue/cyan color.
* Numeric literals (`180`, `54`, `369`, `11`, `5`, `2`) are in a yellow color.
* Mathematical operators (`*`, `+`, `=`, `^`, `:=`, `:`, `->`) and punctuation are in white or light gray.
* The type `ℝ` (real numbers) is in a light blue color.
* Function names (`Real.sqrt`) are in white.
### Detailed Analysis
The image contains three separate theorem proofs. The language is English, embedded within Lean 4 code syntax.
**Theorem 1: `mathd_algebra_141`**
* **Variables**: `a`, `b` of type `ℝ` (real numbers).
* **Hypotheses**:
* `h₁`: `(a * b) = 180`
* `h₂`: `2 * (a + b) = 54`
* **Goal**: `(a^2 + b^2) = 369`
* **Proof Tactic**: `by nlinarith` (a tactic for nonlinear arithmetic).
**Theorem 2: `mathd_algebra_329`**
* **Variables**: `x`, `y` of type `ℝ`.
* **Hypotheses**:
* `h₀`: `3 * y = x`
* `h₁`: `2 * x + 5 * y = 11`
* **Goal**: `x + y = 4`
* **Proof Tactic**: `by linarith` (a tactic for linear arithmetic).
**Theorem 3: `mathd_algebra_547`**
* **Variables**: `x`, `y` of type `ℝ`.
* **Hypotheses**:
* `h₀`: `x = 5`
* `h₁`: `y = 2`
* **Goal**: `Real.sqrt (x ^ 3 - 2 ^ y) = 11`
* **Proof Tactic**: A multi-step proof:
1. `by simp [h₀, h₁, sq]` (simplifies using hypotheses and the definition of square).
2. `rw [Real.sqrt_eq_iff_sq_eq] <;> norm_num` (rewrites using the property that sqrt(a)=b iff b²=a, then normalizes numbers).
### Key Observations
1. **Structure**: All three theorems follow a consistent pattern: `theorem [name] ([vars] : ℝ) ([hypotheses]) : [goal] := by [tactic]`.
2. **Proof Complexity**: The proof tactics increase in complexity from a single automated tactic (`nlinarith`, `linarith`) to a combination of simplification and rewriting (`simp`, `rw`).
3. **Mathematical Content**: The theorems cover basic algebra: solving for sums of squares given product and sum (Theorem 141), solving a system of linear equations (Theorem 329), and evaluating a square root of a numeric expression (Theorem 547).
4. **Syntax**: The code uses standard Lean 4 notation. The `ℝ` symbol denotes the type of real numbers. The `:=` symbol separates the goal from the proof. The `by` keyword introduces a tactic block.
### Interpretation
This image is a technical artifact from the domain of formal verification and automated theorem proving. It demonstrates how mathematical problems are encoded and solved within a proof assistant like Lean.
* **Purpose**: These are likely example problems or test cases, possibly from a dataset (suggested by the naming scheme `mathd_algebra_XXX`), used to train or benchmark automated reasoning systems. The proofs rely on Lean's powerful arithmetic solvers (`linarith`, `nlinarith`), which can automatically discharge many goals involving linear and nonlinear arithmetic over reals.
* **Relationship Between Elements**: Each theorem block is a self-contained unit. The hypotheses provide the given information, the goal states what needs to be proven, and the tactic is the computational strategy that bridges the two. The successful proof (indicated by the lack of an error message) confirms the logical validity of the goal given the hypotheses.
* **Notable Pattern**: The progression from `linarith` to `nlinarith` to a custom `simp`/`rw` sequence illustrates different levels of automation. Linear systems are the easiest to solve automatically. Nonlinear problems (like the sum of squares in Theorem 141) require a more powerful solver. The final theorem, while arithmetically simple, requires explicit rewriting rules, showing that not all problems are solvable by a single "magic" tactic.
* **Underlying Message**: The image showcases the power and conciseness of modern theorem-proving languages. Complex mathematical reasoning is expressed in a compact, structured, and machine-verifiable format. The clean syntax highlighting and presentation suggest this is from an educational resource, a well-documented codebase, or a research paper demonstrating automated problem-solving capabilities.
</details>
c) Basic Calculus and Analysis: ReProver showed early capabilities in dealing with logarithms and exponentials, including mathd_algebra_484, a theorem involving dividing logarithmic expressions.
<details>
<summary>extracted/6256159/carbon49.png Details</summary>
### Visual Description
## Code Snippet: Lean 4 Theorem Proof
### Overview
The image is a screenshot of a code editor or terminal window with a dark theme, displaying a formal mathematical theorem and its proof written in the Lean 4 programming language and theorem prover. The content is a self-contained proof of a logarithmic identity.
### Components / Visual Elements
1. **Window Frame**: A dark gray rectangular window with rounded corners, centered on a light gray background.
2. **Window Controls**: In the top-left corner of the window, there are three colored circles arranged horizontally:
* Left: Red
* Center: Yellow/Orange
* Right: Green
These are standard macOS-style window control buttons (close, minimize, maximize).
3. **Code Content**: The main body of the window contains four lines of monospaced text with syntax highlighting. The text is left-aligned with a consistent indentation for the proof tactics.
### Detailed Content (Transcription)
The following text is present in the code block. The syntax highlighting colors are described in brackets.
**Line 1:**
`theorem mathd_algebra_484 : Real.log 27 / Real.log 3 = 3 := by`
* `theorem` (Yellow/Gold)
* `mathd_algebra_484` (White/Light Gray)
* `:` (White/Light Gray)
* `Real.log` (Purple/Magenta)
* `27` (Cyan/Teal)
* `/` (White/Light Gray)
* `Real.log` (Purple/Magenta)
* `3` (Cyan/Teal)
* `=` (White/Light Gray)
* `3` (Cyan/Teal)
* `:=` (White/Light Gray)
* `by` (Yellow/Gold)
**Line 2 (Indented):**
` field_simp`
* `field_simp` (Yellow/Gold)
**Line 3 (Indented):**
` rw [← Real.log_rpow]`
* `rw` (Yellow/Gold)
* `[` (White/Light Gray)
* `←` (White/Light Gray)
* `Real.log_rpow` (Purple/Magenta)
* `]` (White/Light Gray)
**Line 4 (Indented):**
` all_goals norm_num`
* `all_goals` (Yellow/Gold)
* `norm_num` (Yellow/Gold)
### Key Observations
* **Language & Context**: The code is written in Lean 4, a functional programming language and interactive theorem prover used for formal verification of mathematics and software.
* **Theorem Statement**: The theorem, named `mathd_algebra_484`, asserts the mathematical identity: the logarithm of 27 to the base *e* (natural log) divided by the logarithm of 3 to the base *e* equals 3. This is a specific instance of the change-of-base formula and the property `log_b(b^k) = k`, since 27 = 3³.
* **Proof Structure**: The proof is concise and uses standard Lean tactics:
1. `field_simp`: A tactic to simplify expressions in a field (like real numbers), likely clearing denominators or simplifying the fraction.
2. `rw [← Real.log_rpow]`: Rewrites the expression using the theorem `Real.log_rpow` in the reverse direction (`←`). `Real.log_rpow` likely states that `log(x^r) = r * log(x)` for real `x` and `r`. Applying it in reverse would transform `log(27)` into `log(3^3)` and then to `3 * log(3)`, allowing cancellation with the denominator.
3. `all_goals norm_num`: Applies the `norm_num` tactic to all remaining goals. `norm_num` is a tactic that solves numerical goals by normalizing arithmetic expressions.
* **Visual Design**: The dark theme with distinct syntax highlighting (yellow for keywords, purple for constants/functions, cyan for numbers) is designed for code readability. The window styling is minimalist.
### Interpretation
This image captures a moment of formal mathematical verification. It demonstrates how modern theorem-proving assistants like Lean are used to encode and rigorously verify mathematical truths.
* **What the data suggests**: The code successfully proves a basic algebraic identity. The choice of tactics (`field_simp`, `rw`, `norm_num`) indicates the proof leverages Lean's library of simplification rules and arithmetic normalization, showing the power of automated reasoning within a formal system.
* **How elements relate**: The theorem statement defines the goal. The `by` keyword introduces the proof block. Each indented line is a tactic that transforms the proof state. The sequence of tactics logically reduces the initial goal to a trivial arithmetic truth that `norm_num` can discharge.
* **Notable aspects**: The theorem name `mathd_algebra_484` suggests it may be part of a larger dataset or challenge (like the Mathlib library or a benchmarking suite). The proof's brevity highlights the effectiveness of Lean's tactic framework for algebraic manipulation. There are no outliers or anomalies; this is a correct and complete formal proof of the stated identity. The image serves as a clear example of human-readable, machine-checked mathematics.
</details>
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 theorems as straightforward enough to prove without complex retrieval of premises, similar to its behavior with previous repositories.
However, by the end of the lifelong learning process, LeanAgent exhibited significant growth in its mathematical reasoning abilities on MiniF2F:
a) Advanced Number Theory: LeanAgent showed a more advanced grasp of number theory, proving theorems like mathd_numbertheory_293, a complex theorem about divisibility involving a complex expression and mathd_numbertheory_233, a theorem dealing with modular arithmetic in $\text{ZMod}(11^{2})$ .
<details>
<summary>extracted/6256159/carbon50.png Details</summary>
### Visual Description
## Screenshot: Mathematical Theorems in a Code Editor
### Overview
The image is a screenshot of a dark-themed code editor or terminal window displaying two formal mathematical theorems and their proofs, written in a syntax consistent with a proof assistant language like Lean. The window has a standard macOS-style title bar with three colored control buttons (red, yellow, green) in the top-left corner. The text is syntax-highlighted in various colors (pink, blue, yellow, white) against a dark gray background.
### Components/Axes
* **Window Frame:** A dark gray rectangular window with rounded corners, centered on a light gray background.
* **Window Controls:** Three circular buttons in the top-left corner of the window: red (left), yellow (center), green (right).
* **Text Content:** Two distinct blocks of code, each defining a theorem and its proof. The text uses a monospaced font.
* **Syntax Highlighting:**
* Keywords (`theorem`, `by`, `exact`): Pink/Salmon
* Theorem Names (`mathd_numbertheory_293`, `mathd_numbertheory_233`): Light Blue
* Variables and Types (`n`, `N`, `h₀`, `h₁`, `b`, `ZMod`): White/Light Gray
* Numerical Values (`9`, `11`, `20`, `100`, `7`, `5`, `24`, `116`): Yellow/Orange
* Mathematical Operators and Symbols (`≤`, `|`, `*`, `+`, `:=`, `^`, `-`): White/Light Gray
### Detailed Analysis / Content Details
**Theorem 1 (Top Block):**
* **Theorem Name:** `theorem mathd_numbertheory_293`
* **Hypotheses:**
* `(n : N)` - Declares `n` as a natural number.
* `(h₀ : n ≤ 9)` - Hypothesis `h₀`: `n` is less than or equal to 9.
* `(h₁ : 11|20 * 100 + 10 * n + 7)` - Hypothesis `h₁`: 11 divides the expression `20 * 100 + 10 * n + 7`. The vertical bar `|` denotes divisibility.
* **Conclusion:** `n = 5`
* **Proof Tactic:** `:= by omega` - The proof is completed by the `omega` tactic, which is often used for solving linear integer arithmetic problems.
**Theorem 2 (Bottom Block):**
* **Theorem Name:** `theorem mathd_numbertheory_233`
* **Hypotheses:**
* `(b : ZMod (11^2))` - Declares `b` as an element of the ring of integers modulo `11^2` (which is 121).
* `(h₀ : b = 24⁻¹)` - Hypothesis `h₀`: `b` is the multiplicative inverse of 24 in the ring `ZMod 121`.
* **Conclusion:** `b = 116`
* **Proof Tactic:** `:= by exact h₀` - The proof is completed by the `exact` tactic, directly using hypothesis `h₀`. This suggests the statement `b = 116` is a direct computation or simplification of `b = 24⁻¹` within `ZMod 121`.
### Key Observations
1. **Formal Verification Context:** The code is not standard mathematical notation but formal statements meant for a proof assistant, where every logical step must be justified by a tactic (`omega`, `exact`).
2. **Number Theory Focus:** Both theorems are from number theory, dealing with divisibility (`11|...`) and modular arithmetic (`ZMod`).
3. **Specific Numerical Results:** The theorems assert specific integer solutions: `n=5` for the first, and the inverse of 24 modulo 121 being `116` for the second.
4. **Proof Strategy:** The first proof uses an automated tactic (`omega`) suitable for linear constraints, while the second uses a direct appeal to a hypothesis (`exact`), indicating the conclusion is essentially a restatement or immediate consequence of the definition given.
### Interpretation
This image captures a snippet of work in formal mathematics or computer-aided theorem proving. The theorems are likely exercises or lemmas from a collection (indicated by names like `mathd_numbertheory_293`).
* **Theorem 293** solves a constrained divisibility puzzle: Find the single-digit `n` (0-9) such that the number formed by the digits `2, 0, n, 7` (interpreted as `2000 + 10*n + 7`? Wait, the expression is `20 * 100 + 10 * n + 7`, which equals `2000 + 10n + 7 = 2007 + 10n`) is divisible by 11. The proof by `omega` confirms the unique solution is `n=5`, making the number 2057 (2007 + 50). 2057 / 11 = 187.
* **Theorem 233** computes a modular inverse. It states that in the ring of integers modulo 121, the multiplicative inverse of 24 is 116. This can be verified: `24 * 116 = 2784`. `2784 mod 121`: 121 * 23 = 2783, so `2784 - 2783 = 1`. Therefore, `24 * 116 ≡ 1 (mod 121)`, confirming `116` is indeed the inverse.
The image demonstrates the process of encoding classical number theory problems into a formal language for machine verification, highlighting the intersection of pure mathematics and computer science. The use of specific tactics reveals the underlying logical structure required for the computer to accept the proofs.
</details>
b) Sophisticated Algebra: LeanAgent showed a better grasp of more complex algebraic manipulations. Theorems include mathd_algebra_148, which involves function definitions and solving for unknown coefficients, and amc12a_2016_p3, involving a special case of a function.
<details>
<summary>extracted/6256159/carbon61.png Details</summary>
### Visual Description
\n
## Screenshot: Formal Mathematical Proof Code
### Overview
The image displays a dark-themed code editor window (resembling a macOS interface with red, yellow, and green window control dots in the top-left corner) containing two formal mathematical theorem statements and their proofs. The code is written in a formal proof language, likely Lean, with syntax highlighting. The content consists of two distinct theorems: one algebraic and one from a mathematics competition.
### Components/Axes
* **UI Elements**: A dark gray editor window with a subtle drop shadow, set against a light gray-blue background. The window has three colored circles (red, yellow, green) in its top-left corner.
* **Code Structure**: The code is presented in a monospaced font with syntax highlighting. Key colors include:
* **Blue/Cyan**: Theorem names, type declarations (`ℝ`, `→`).
* **White/Light Gray**: General code text, parentheses, colons.
* **Red**: Numerical constants (e.g., `3`, `9`, `2`, `5`, `40`).
* **Green**: Proof tactics (`by`, `linarith`, `norm_num`, `field_simp`, `norm_cast`).
* **Content Layout**: The two theorem blocks are separated by a blank line. Each follows a similar structure: a `theorem` declaration, a list of parameters and hypotheses in parentheses, a conclusion, and a proof starting with `:= by`.
### Detailed Analysis
The image contains two complete, self-contained formal proofs.
**Theorem 1: `mathd_algebra_148`**
* **Declaration**: `theorem mathd_algebra_148`
* **Parameters & Hypotheses**:
* `(c : ℝ)` - `c` is a real number.
* `(f : ℝ → ℝ)` - `f` is a function from real numbers to real numbers.
* `(h₀ : ∀ x, f x = c * x^3 - 9 * x + 3)` - Hypothesis `h₀`: For all `x`, `f(x) = c*x³ - 9*x + 3`.
* `(h₁ : f 2 = 9)` - Hypothesis `h₁`: `f(2) = 9`.
* **Conclusion**: `c = 3`
* **Proof**: `:= by linarith [h₀ 2]`
* The proof uses the `linarith` (linear arithmetic) tactic, supplied with the instantiation of hypothesis `h₀` at `x=2` (i.e., `f(2) = c*2³ - 9*2 + 3`). Combined with `h₁` (`f(2)=9`), this allows the tactic to solve for `c`.
**Theorem 2: `amc12a_2016_p3`**
* **Declaration**: `theorem amc12a_2016_p3`
* **Parameters & Hypotheses**:
* `(f : ℝ → ℝ → ℝ)` - `f` is a function taking two real numbers and returning a real number.
* `(h₀ : ∀ x, ∀ (y) (_ : y ≠ 0), f x y = x - y * Int.floor (x / y))` - Hypothesis `h₀`: For all `x` and all `y` where `y ≠ 0`, `f(x, y) = x - y * floor(x / y)`. This defines `f` as the remainder operation (modulo).
* **Conclusion**: `f (3 / 8) (-(2 / 5)) = -(1 / 40)`
* **Proof**: `:= by norm_num [h₀] field_simp norm_cast`
* The proof uses a sequence of tactics: `norm_num` (normalizes numerical expressions using hypothesis `h₀`), `field_simp` (simplifies expressions in a field), and `norm_cast` (manages type casts between numeric types).
### Key Observations
1. **Formal Verification**: The code represents machine-checkable proofs of mathematical statements, not just informal descriptions.
2. **Proof Strategy Contrast**: The first proof is very concise, relying on a single powerful tactic (`linarith`) applied to a specific instance of a hypothesis. The second proof uses a sequence of more specialized simplification and normalization tactics.
3. **Mathematical Content**: The first theorem is a straightforward algebraic solve for a coefficient. The second theorem formalizes a property of the modulo operation (specifically, the remainder when dividing `3/8` by `-2/5`) and is sourced from the 2016 AMC 12A competition (Problem 3).
4. **Syntax Highlighting**: The color scheme aids readability by distinguishing between theorem names, types, numerical values, and proof commands.
### Interpretation
This image is a snapshot of formal mathematics in practice. It demonstrates how abstract mathematical problems—solving for a constant in a cubic function and evaluating a specific modular arithmetic expression—can be translated into a precise, logical language for computer verification.
The first theorem (`mathd_algebra_148`) shows the power of automated reasoning (`linarith`) for solving linear constraints derived from algebraic definitions. The second theorem (`amc12a_2016_p3`) is more intricate, requiring the formal definition of the floor function (`Int.floor`) and the manipulation of rational numbers. The proof tactics suggest the challenge lies in correctly simplifying the expression `3/8 - (-2/5) * floor((3/8)/(-2/5))` to `-1/40`.
The presence of a competition problem (`amc12a_2016_p3`) indicates this code might be part of a repository for formalizing olympiad or contest problems, serving as both a verification tool and an educational resource. The clean, highlighted presentation suggests it is meant for human reading as well as machine execution, bridging the gap between human mathematical intuition and formal logical rigor.
</details>
c) Advanced Calculus and Analysis: LeanAgent demonstrated improved capabilities in handling more complex analytical problems, including mathd_algebra_270, a theorem involving function composition and rational expressions.
<details>
<summary>extracted/6256159/carbon52.png Details</summary>
### Visual Description
\n
## Code Snippet: Lean Theorem Proof
### Overview
The image is a screenshot of a code editor window (likely on macOS, indicated by the three colored window control dots in the top-left corner) displaying a theorem and its proof written in the Lean theorem prover language. The code is presented with syntax highlighting on a dark background.
### Components/Axes
This is not a chart or diagram with axes. The components are the lines of code within the editor window.
**Window Elements:**
* **Top-left corner:** Three circular window control buttons (red, yellow, green).
* **Main content area:** A block of code with syntax highlighting. The text colors are part of the theme and help distinguish language elements.
### Detailed Analysis / Content Details
The following text is present in the image, transcribed exactly as it appears, including syntax highlighting colors noted descriptively:
1. **Line 1 (Pink text):** `theorem mathd_algebra_270`
* This declares a theorem named `mathd_algebra_270`.
2. **Line 2 (Mixed colors):** ` (f : ℝ → ℝ)`
* This is a parameter declaration. It states that `f` is a function from the real numbers (`ℝ`) to the real numbers (`ℝ`). The symbol `ℝ` is rendered in a distinct color (likely blue or cyan).
3. **Line 3 (Mixed colors):** ` (h₀ : ∀ x, x ≠ -2 → f x = 1 / (x + 2)) :`
* This declares a hypothesis named `h₀`.
* The hypothesis states: "For all `x`, if `x` is not equal to `-2`, then `f x` equals `1 / (x + 2)`."
* Symbols: `∀` (for all), `≠` (not equal), `→` (implies), `ℝ` (real numbers) are present.
4. **Line 4 (Mixed colors):** ` f (f 1) = 3/7 := by`
* This is the goal of the theorem: to prove that `f (f 1)` equals `3/7`.
* The `:= by` indicates the start of the proof.
5. **Line 5 (Mixed colors):** ` set_option tactic.skipAssignedInstances false in norm_num [h₀]`
* This is the proof tactic.
* It first sets an option (`tactic.skipAssignedInstances`) to `false`.
* Then it uses the `norm_num` tactic, providing the hypothesis `h₀` as a parameter in square brackets `[h₀]`.
### Key Observations
* **Language:** The code is written in Lean, a formal proof management system and functional programming language.
* **Structure:** The code follows a standard Lean theorem structure: `theorem name : statement := by proof`.
* **Mathematical Content:** The theorem defines a function `f` with a specific rational expression and asks to compute the value of its composition at a point (`f(f(1))`).
* **Proof Method:** The proof relies on the `norm_num` tactic, which is used for normalizing numerical expressions, and it explicitly uses the given hypothesis `h₀`.
### Interpretation
This image captures a formal mathematical statement and its verification within a computer-assisted proof system.
* **What the data suggests:** The code represents a solved problem, likely from a mathematics competition or textbook (suggested by the name `mathd_algebra_270`). It demonstrates the use of a theorem prover to verify an algebraic computation.
* **How elements relate:** The hypothesis `h₀` defines the function `f`. The goal is a specific numerical claim about `f`. The proof tactic `norm_num` uses the definition in `h₀` to compute the value `f(1) = 1/(1+2) = 1/3`, and then `f(f(1)) = f(1/3) = 1/(1/3 + 2) = 1/(7/3) = 3/7`, thereby proving the goal.
* **Notable aspects:** The use of `set_option tactic.skipAssignedInstances false` is a technical detail specific to the Lean tactic state, indicating a precise control over how the `norm_num` tactic behaves in this context. The entire snippet is a self-contained, machine-checkable proof of a simple algebraic identity.
</details>
d) Complex Induction: LeanAgent became adept at more advanced induction proofs. An example is induction_12dvd4expnp1p20, a theorem about divisibility that requires an induction proof.
<details>
<summary>extracted/6256159/carbon54.png Details</summary>
### Visual Description
\n
## Screenshot: Lean 4 Theorem Proof Snippet
### Overview
The image is a screenshot of a code editor or terminal window displaying a formal mathematical theorem and its proof written in the Lean 4 proof assistant language. The window has a dark theme with syntax-highlighted text. The content is a self-contained proof of a number theory statement.
### Components/Axes
* **Window Frame:** A dark gray rectangular window with rounded corners, centered on a light gray background.
* **Window Controls:** Three colored circles (red, yellow, green) are positioned in the top-left corner of the window, typical of macOS window controls.
* **Code Content:** The main body of the window contains six lines of monospaced text with syntax highlighting. Keywords (`theorem`, `by`, `norm_num`, `induction'`, `with`, `simp`, `omega`) are in a gold/yellow color. The theorem name and other identifiers are in a light gray/white. The type `ℕ` (natural numbers) is highlighted in green.
### Detailed Analysis
The text content is transcribed precisely below. The language is English with mathematical notation.
**Line 1:** `theorem induction_12dvd4expnp1p20 (n : ℕ) : 12 | 4^(n+1) + 20 := by`
* **Theorem Name:** `induction_12dvd4expnp1p20`
* **Variable Declaration:** `(n : ℕ)` declares a variable `n` of type `ℕ` (the set of natural numbers {0, 1, 2, ...}).
* **Theorem Statement:** `12 | 4^(n+1) + 20`
* The symbol `|` denotes "divides". The statement asserts that for any natural number `n`, the integer 12 divides the number `4^(n+1) + 20`.
* **Proof Start:** `:= by` indicates the beginning of the proof script.
**Lines 2-6 (Proof Script):**
* **Line 2:** ` norm_num` - A tactic that solves goals involving numeric computations.
* **Line 3:** ` induction' n with n hn` - The core proof strategy. It performs induction on the variable `n`. The `with n hn` clause introduces the inductive hypothesis: for a given `n`, assume the statement holds (this is `hn`), and then prove it for `n+1`.
* **Line 4:** ` simp` - A tactic that simplifies expressions using a set of predefined rules.
* **Line 5:** ` omega` - A tactic that solves linear arithmetic goals, often used to handle the remaining arithmetic after simplification.
### Key Observations
1. **Conciseness:** The proof is remarkably short (4 tactic lines), indicating the use of powerful, automated tactics (`norm_num`, `omega`) in Lean 4.
2. **Proof Structure:** The proof follows a classic induction pattern: establish a base case (handled implicitly by `norm_num` or the induction principle) and then prove the inductive step.
3. **Syntax Highlighting:** The color scheme aids readability by distinguishing language keywords from user-defined names and types.
4. **Mathematical Content:** The theorem is a specific divisibility property. The expression `4^(n+1) + 20` can be rewritten as `4 * 4^n + 20`. The proof likely shows that this expression is always a multiple of 12 by analyzing it modulo 12.
### Interpretation
This image captures a moment of formal verification in mathematics. It demonstrates how modern proof assistants like Lean can encode and automatically verify number-theoretic statements.
* **What the data suggests:** The code successfully proves the proposition `∀ n ∈ ℕ, 12 divides (4^(n+1) + 20)`. This is a true mathematical fact. For example:
* n=0: `4^(1) + 20 = 24`, which is 12 * 2.
* n=1: `4^(2) + 20 = 36`, which is 12 * 3.
* n=2: `4^(3) + 20 = 84`, which is 12 * 7.
* **How elements relate:** The `induction'` tactic sets up the logical framework. The `simp` and `omega` tactics then perform the algebraic manipulation and arithmetic reasoning needed to discharge the goal for the inductive step, relying on the inductive hypothesis `hn`.
* **Notable aspects:** The proof's brevity highlights the effectiveness of Lean's tactic framework. The theorem name `induction_12dvd4expnp1p20` is a descriptive, machine-generated identifier that encodes the method (`induction`), the divisor (`12dvd`), and the expression (`4expnp1p20` for `4^(n+1)+20`). This is a common practice in formal mathematics libraries for traceability.
</details>
e) Complex Quantifiers and Inequalities: LeanAgent increased its ability to prove more complex logical statements, such as amc12a_2002_p6, a theorem involving multiple existential quantifiers and inequalities.
<details>
<summary>extracted/6256159/carbon55.png Details</summary>
### Visual Description
\n
## [Code Screenshot]: Formal Proof of a Mathematical Theorem
### Overview
The image is a screenshot of a code editor window (dark theme) displaying a formal mathematical theorem and its proof written in a dependently-typed proof assistant language, most likely Lean 4. The code defines a theorem named `amc12a_2002_p6` and provides a concise proof script.
### Components/Axes
* **Window Frame**: A dark gray rectangular window with rounded corners, centered on a light gray background. The top-left corner contains three colored circles (red, yellow, green), mimicking macOS window controls.
* **Code Content**: The primary content is a block of monospaced text with syntax highlighting. The text is left-aligned within the window.
* **Syntax Highlighting Colors**:
* **Yellow/Gold**: Keywords (`theorem`, `lift`, `to`, `using`, `cases'`, `with`, `exact`, `by`, `simp`).
* **Green**: Type identifiers and some logical symbols (`ℕ`, `ℕ+`, `∃`, `∧`, `≤`).
* **White/Light Gray**: Theorem name, variable names, hypothesis names, proof terms, and most operators (`amc12a_2002_p6`, `n`, `h₀`, `m`, `p`, `*`, `+`, `_`, `lt_add_of_pos_right`, `zero_lt_one`, `1`).
### Detailed Analysis / Content Details
**Transcription of the Code:**
```lean
theorem amc12a_2002_p6 (n : ℕ) (h₀ : 0 < n) : ∃ m, (m > n ∧ ∃ p, m * p ≤ m + p) := by
lift n to ℕ+ using h₀
cases' n with n
exact (_, lt_add_of_pos_right _ zero_lt_one, 1, by simp)
```
**Line-by-Line Breakdown:**
1. **Theorem Declaration**:
* `theorem amc12a_2002_p6`: Declares a theorem with the name `amc12a_2002_p6`, indicating it is likely the solution to Problem 6 from the 2002 AMC 12A competition.
* `(n : ℕ)`: The theorem is parameterized by a variable `n` of type `ℕ` (natural numbers).
* `(h₀ : 0 < n)`: A hypothesis `h₀` stating that `n` is greater than 0 (i.e., `n` is positive).
* `: ∃ m, (m > n ∧ ∃ p, m * p ≤ m + p)`: The proposition to be proven. It states: "There exists a natural number `m` such that `m` is greater than `n`, AND there exists a natural number `p` such that `m * p` is less than or equal to `m + p`."
* `:= by`: Begins the proof script.
2. **Proof Script**:
* `lift n to ℕ+ using h₀`: This tactic uses the hypothesis `h₀` (0 < n) to "lift" `n` from the type `ℕ` (natural numbers) to `ℕ+` (positive natural numbers). This is a type refinement step.
* `cases' n with n`: This tactic performs case analysis on the positive natural number `n`. The `with n` part suggests it might be destructing it into its underlying natural number component, though the exact behavior depends on the definition of `ℕ+`.
* `exact (_, lt_add_of_pos_right _ zero_lt_one, 1, by simp)`: This provides the exact proof term to close the goal. It constructs a tuple (likely a dependent pair) containing:
* `_`: A placeholder for the existential witness `m`. The underscore indicates it will be inferred by the type checker.
* `lt_add_of_pos_right _ zero_lt_one`: A proof of the first conjunct `m > n`. It applies a lemma `lt_add_of_pos_right` with arguments `_` (likely `n`) and `zero_lt_one` (a proof that 0 < 1).
* `1`: The witness for the existential `p`. The proof asserts that `p = 1` works.
* `by simp`: A proof of the second conjunct `m * 1 ≤ m + 1`. The `simp` tactic simplifies this inequality, which holds for all natural numbers `m`.
### Key Observations
1. **Conciseness**: The entire proof is completed in three tactic steps after the theorem declaration, demonstrating the power of the proof assistant's automation and library.
2. **Proof Strategy**: The proof does not explicitly construct the witness `m`. Instead, it relies on type inference (`_`) and a general lemma (`lt_add_of_pos_right`) that likely states `n < n + k` for any positive `k`. The choice of `p = 1` is explicit and simplifies the inequality to a trivial truth.
3. **Syntax**: The code uses specific syntax (`:= by`, `cases'`, `ℕ+`) characteristic of the Lean 4 proof assistant and its mathematical library (Mathlib).
4. **Visual Layout**: The code is presented in a clean, syntax-highlighted block within a stylized window, suggesting it might be from a documentation page, a tutorial, or a social media post showcasing a formal proof.
### Interpretation
This image captures a formal verification of a number theory problem from a mathematics competition. The theorem states a property about positive integers: for any positive integer `n`, you can always find a larger integer `m` and another integer `p` such that the product `m*p` is no greater than the sum `m+p`.
The proof reveals the underlying mathematical insight: the property holds trivially if you choose `p = 1`. In that case, the inequality becomes `m * 1 ≤ m + 1`, which simplifies to `m ≤ m + 1`, always true. The only non-trivial part is ensuring `m > n`, which the proof handles by invoking a general lemma about addition increasing order.
The existence of such a formal proof demonstrates how competition mathematics problems can be translated into and rigorously verified within a computer-based formal system. The code is not just a description but a machine-checkable certificate of the theorem's truth. The use of placeholders (`_`) and automation (`simp`) highlights the balance between human-guided strategy and computer-driven verification in modern interactive theorem proving.
</details>
The proofs at this later stage are more sophisticated, usually involving multiple steps and combining various mathematical concepts or indicating a better ability to connect different areas of mathematics, mirroring the progression observed in Mathematics in Lean Source and SciLean. For example, as shown above, LeanAgent provides a one-line proof to the relatively advanced theorem mathd_numbertheory_233. The proof means the hypothesis directly proves the goal. This suggests that LeanAgent grasps modular arithmetic and recognizes when a given hypothesis is sufficient to prove the goal without additional steps.
Furthermore, as shown above, LeanAgent uses four tactics to prove the induction_12dvd4expnp1p20 theorem. This demonstrates its ability to handle more complex number theory proofs and use advanced tactics. This again shows that LeanAgent can recognize when it does not require complex premise retrieval.
LeanAgent demonstrates a similar grasp of the theorem amc12a_2002_p6. Notably, it combines the simple premises lt_add_of_pos_right, which describes how an element is less than that element added with a positive one, and zero_lt_one, which states that 0 is less than 1, with more advanced tactics like lift, cases, and exact with complex term construction. This demonstrates its ability to reuse foundational concepts for more complex proofs of abstract mathematical concepts, showing its stability.
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 arithmetic and algebra to LeanAgent’s more advanced number theory, calculus, and abstract algebra. This aligns with the observations from Mathematics in Lean Source and SciLean, further supporting the effectiveness of LeanAgent’s lifelong learning approach in 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 problems 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.lean 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): Pass@1 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 a 33.61% cumulative accuracy on the Lean4 test set, but this makes a direct comparison with the Pass@1 rates of LeanAgent and ReProver infeasible. Moreover, DeepSeek-Prover-V1.5 (Xin et al., 2024b) reports a state-of-the-art result of 63.5% on the Lean4 test set.
However, LeanAgent is a lifelong learning framework, not a 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 a 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 retriever as the starting one in LeanAgent, allowing for a more faithful comparison. We use ReProver because past work has shown that retrieval leads to improved generalizability.
Moreover, we design LeanAgent to continuously generalize to and improve on ever-expanding mathematical knowledge without forgetting previously learned knowledge. Our goal is not to beat the MiniF2F benchmark; instead, we aim to 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 to 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 to ReProver in real number properties and can handle basic inequality reasoning, proving book.irrational.lem_aux_ii, which involves real analysis and inequalities.
<details>
<summary>extracted/6256159/carbon56.png Details</summary>
### Visual Description
\n
## Code Snippet: Formal Lemma in a Proof Assistant
### Overview
The image displays a screenshot of a code editor or terminal window containing a single line of formal mathematical code. The code defines a lemma (a proven statement) named `lem_aux_ii` within a proof assistant language, likely Lean 4, given the syntax. The window has a dark theme with syntax highlighting.
### Components
* **Window Frame:** A dark gray rectangular window with rounded corners, centered on a light gray background.
* **Window Controls:** Three colored circles in the top-left corner: red, yellow, and green, typical of macOS window controls.
* **Code Block:** The main content area contains a single, multi-part statement written in a monospaced font with syntax highlighting. The colors differentiate keywords, variables, types, and operators.
### Content Details (Transcription)
The exact text within the code block is:
```
lemma lem_aux_ii (n : ℕ) (x : ℝ) (h_1 : 0 < x) (h_2 : x < 0) :
(0 < f_aux n x) ∧ (f_aux n x < (1 : ℝ) / n.factorial) := by
constructor <;> linarith
```
**Breakdown of the Code Statement:**
1. **`lemma lem_aux_ii`**: Declares a new lemma with the identifier `lem_aux_ii`.
2. **`(n : ℕ)`**: Declares a variable `n` of type `ℕ` (the set of natural numbers).
3. **`(x : ℝ)`**: Declares a variable `x` of type `ℝ` (the set of real numbers).
4. **`(h_1 : 0 < x)`**: Declares a hypothesis `h_1` stating that `0` is less than `x` (i.e., `x` is positive).
5. **`(h_2 : x < 0)`**: Declares a hypothesis `h_2` stating that `x` is less than `0` (i.e., `x` is negative).
6. **`:`**: Separates the lemma's parameters and hypotheses from its conclusion.
7. **`(0 < f_aux n x) ∧ (f_aux n x < (1 : ℝ) / n.factorial)`**: The conclusion to be proven. It is a logical conjunction (`∧`, meaning "and") of two inequalities:
* `0 < f_aux n x`: The function `f_aux` applied to `n` and `x` is greater than `0`.
* `f_aux n x < (1 : ℝ) / n.factorial`: The same function value is less than `1` divided by `n` factorial (where `1` is explicitly typed as a real number `(1 : ℝ)`).
8. **`:= by`**: Indicates the start of the proof script.
9. **`constructor <;> linarith`**: The proof tactic. `constructor` is used to break the conjunction (`∧`) in the goal into two subgoals. The `<;>` operator applies the subsequent tactic (`linarith`, a tactic for solving linear arithmetic problems) to each subgoal generated by `constructor`.
### Key Observations
* **Contradictory Hypotheses:** The hypotheses `h_1 : 0 < x` and `h_2 : x < 0` are mutually exclusive. No real number `x` can be both strictly greater than and strictly less than zero simultaneously.
* **Proof Strategy:** The proof uses `linarith` after `constructor`. Given the contradictory hypotheses, `linarith` can likely derive a contradiction (e.g., `0 < 0`), which allows it to prove any goal, including the stated inequalities about `f_aux n x`. This suggests the lemma might be vacuously true or part of a proof by contradiction.
* **Syntax Highlighting:** Keywords (`lemma`, `by`, `constructor`) are in a salmon/pink color. Types (`ℕ`, `ℝ`) and the number `1` are in a teal/cyan color. Variables (`n`, `x`, `h_1`, `h_2`) and the function name `f_aux` are in a light orange/yellow color. Operators (`:`, `<`, `∧`, `/`, `:=`, `<;>`) are in a light blue color.
### Interpretation
This image captures a snippet of formal mathematics being verified by a computer. The lemma `lem_aux_ii` states a property about an unspecified function `f_aux`: for any natural number `n` and real number `x`, if `x` is both positive and negative (an impossible condition), then the value of `f_aux n x` is bounded between `0` and `1/n!`.
The primary informational content is the **code itself**. The logical structure reveals a common technique in formal proofs: establishing a result under an impossible assumption, which is trivially true because the assumption can never hold. The proof tactic `linarith` is powerful enough to recognize this and close the proof automatically. The function `f_aux` is not defined here, implying this lemma is part of a larger development, possibly related to analysis, series, or combinatorics where factorial bounds are common. The screenshot serves as documentation or an example of this specific formal statement and its concise proof.
</details>
b) Number Theory: LeanAgent shows capabilities in fundamental number theory concepts, proving book.quadratic_reciprocity.quadratic_reciprocity_2, a key result in quadratic reciprocity.
<details>
<summary>extracted/6256159/carbon57.png Details</summary>
### Visual Description
\n
## Code Snippet: Formal Proof of Quadratic Reciprocity
### Overview
The image displays a screenshot of a code editor or terminal window with a dark theme. It contains a single, complete line of formal code representing a mathematical theorem and its proof. The code is written in a language that appears to be a proof assistant (like Lean), using formal logic and type theory to state and prove the law of quadratic reciprocity.
### Components/Axes
* **Window Frame:** A dark gray rectangular window with rounded corners. The top-left corner contains three circular window control buttons (red, yellow, green), characteristic of a macOS interface.
* **Code Content:** The main body of the window contains a single, multi-part statement written in a monospaced font with syntax highlighting. The text is left-aligned.
* **Syntax Highlighting Colors:**
* Keywords (`theorem`, `by`, `exact`): Light pink/salmon.
* Theorem/Function names (`quadratic_reciprocity_2`, `legendre_sym`, `book.quadratic_reciprocity.quadratic_reciprocity_1`): Light blue/cyan.
* Variables and parameters (`p`, `q`, `hp`, `hq`): Light orange/peach.
* Types and constants (`ℕ`, `Nat.Prime`, `Fact`): Light green.
* Operators and punctuation (`:`, `≠`, `*`, `^`, `/`, `:=`): White or light gray.
* Numeric literals (`2`, `1`): Light purple.
### Detailed Analysis
The code is a formal theorem statement and proof. Here is the precise transcription:
**Line 1:** `theorem quadratic_reciprocity_2 (p q : ℕ) (hp : p ≠ 2) (hq : q ≠ 2)`
* Declares a theorem named `quadratic_reciprocity_2`.
* Takes four parameters:
* `p` and `q`, which are of type `ℕ` (the natural numbers).
* `hp`, which is a proof (or hypothesis) that `p` is not equal to 2.
* `hq`, which is a proof that `q` is not equal to 2.
**Line 2:** `[Fact (Nat.Prime p)] [Fact (Nat.Prime q)] :`
* This line provides additional typeclass instances or facts.
* `[Fact (Nat.Prime p)]`: Asserts the fact that `p` is a prime number.
* `[Fact (Nat.Prime q)]`: Asserts the fact that `q` is a prime number.
* The colon `:` ends the parameter and hypothesis list, leading to the theorem's statement.
**Line 3:** `(legendre_sym p q) * (legendre_sym q p) = -1 ^ (((p-1) / 2 * (q - 1) / 2 ) := by`
* This is the core statement of the theorem.
* `(legendre_sym p q)`: Represents the Legendre symbol `(p/q)`.
* `(legendre_sym q p)`: Represents the Legendre symbol `(q/p)`.
* The statement claims that the product of these two symbols equals `-1` raised to the power of `((p-1)/2 * (q-1)/2)`.
* `:= by` indicates that the proof of this statement follows.
**Line 4:** `exact book.quadratic_reciprocity.quadratic_reciprocity_1 p q hp hq`
* This is the proof tactic.
* `exact`: A tactic that solves the goal by providing a exact term that matches the goal type.
* `book.quadratic_reciprocity.quadratic_reciprocity_1`: References a previously proven theorem (likely from a formalized library or "book") named `quadratic_reciprocity_1`.
* `p q hp hq`: The parameters passed to this referenced theorem, which matches the hypotheses of the current theorem.
### Key Observations
1. **Formal Verification:** The code is not executable in the traditional sense but is a formal, machine-checkable proof of a fundamental theorem in number theory.
2. **Theorem Dependency:** This theorem (`quadratic_reciprocity_2`) is a direct corollary or restatement of a more fundamental theorem (`quadratic_reciprocity_1`), as evidenced by the `exact` tactic.
3. **Hypothesis Constraints:** The proof explicitly requires that `p` and `q` are odd primes (not equal to 2), which is a standard condition for the most common formulation of the law of quadratic reciprocity.
4. **Mathematical Content:** The equation `(p/q)*(q/p) = (-1)^{((p-1)/2 * (q-1)/2)}` is the classic statement of the law of quadratic reciprocity, which describes the relationship between the solvability of the quadratic congruences `x² ≡ p mod q` and `x² ≡ q mod p`.
### Interpretation
This image captures a moment in the formalization of mathematics. It shows how a deep, classical result from 18th-century number theory (first proved by Gauss) is encoded in a 21st-century proof assistant. The code demonstrates the **Peircean investigative** process of moving from a general law (quadratic reciprocity) to a specific, verifiable instance (`quadratic_reciprocity_2`) by applying known facts (p and q are odd primes) and leveraging existing formal knowledge (`quadratic_reciprocity_1`).
The significance lies in the **translation of human mathematical insight into a rigid, logical structure** that a computer can validate. This process eliminates ambiguity and provides an absolute guarantee of correctness for the theorem under the given hypotheses. The snippet is a microcosm of modern formal mathematics: building complex, trusted results upon a foundation of previously verified code.
</details>
Notably, the proof of the first theorem uses no premises, and the proof of the second uses a 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 a key result in abstract algebra, wedderburn (Wedderburn’s Little Theorem), which is a crucial result in abstract algebra, stating that every finite division ring is a field.
<details>
<summary>extracted/6256159/carbon58.png Details</summary>
### Visual Description
\n
## Screenshot: Code Snippet in a Terminal/Editor Window
### Overview
The image is a screenshot of a dark-themed code editor or terminal window displaying a single line of formal mathematical code, likely written in a theorem-proving language such as Lean. The window is centered against a soft, gradient background.
### Components/Axes
1. **Window Frame**: A dark gray, rounded rectangle with a subtle drop shadow, centered on the screen.
2. **Window Controls**: Three colored circles (traffic light buttons) are positioned in the top-left corner of the window frame.
* **Red** (leftmost)
* **Yellow** (center)
* **Green** (rightmost)
3. **Code Content Area**: The main dark area of the window containing the syntax-highlighted code.
4. **Background**: A smooth, vertical gradient transitioning from a light gray at the top to a darker gray at the bottom.
### Detailed Analysis
The primary content is a single line of code with specific syntax highlighting:
* **Full Transcription**:
`theorem wedderburn (h: Fintype R): IsField R := by apply Field.toIsField`
* **Syntax Highlighting & Color Coding**:
* `theorem` and `by`: Displayed in a light, desaturated blue or gray color.
* `wedderburn`, `h`, `:`, `(`, `)`, `:=`, `.`, `toIsField`: Displayed in white or off-white.
* `Fintype` and `IsField`: Displayed in a distinct, lighter blue color, indicating they are likely types or constants.
* `R`: Displayed in a reddish-orange color, indicating it is a variable or parameter.
* `apply` and `Field`: Displayed in the same light blue as `Fintype` and `IsField`.
### Key Observations
* The code follows a clear structure: `theorem [name] ([hypothesis]): [goal] := by [tactic]`.
* The theorem is named `wedderburn`.
* The hypothesis `h` asserts that `R` is of type `Fintype` (a finite type).
* The goal is to prove that `R` is of type `IsField` (a field).
* The proof strategy is a single tactic: `apply Field.toIsField`, suggesting the use of a predefined lemma or constructor.
* The visual presentation is minimalist, focusing entirely on the code snippet with no other UI elements (like line numbers, menus, or file tabs) visible.
### Interpretation
This image captures a moment in formal verification or interactive theorem proving. The code is attempting to prove a theorem named after Wedderburn, likely referencing **Wedderburn's little theorem**, which states that every finite division ring is a commutative field (i.e., a finite field).
The code's logic is straightforward: it takes as a hypothesis (`h`) that `R` is a finite type (`Fintype R`) and aims to conclude that `R` is a field (`IsField R`). The proof is discharged by applying a rule or lemma called `Field.toIsField`. This suggests that within the formal system being used, there exists a proven statement that directly converts the property of being a finite division ring (or a similar structure implied by the context) into the property of being a field.
The screenshot is likely intended to demonstrate the conciseness of expressing a significant mathematical theorem in a formal language, or it could be part of a tutorial or documentation showing how to use a specific library or tactic. The clean, focused presentation emphasizes the code itself as the central artifact of interest.
</details>
LeanAgent’s proof of the wedderburn theorem represents the ability to handle algebraic structures. By using the Field.toIsField premise, LeanAgent shows that it has grasped how to use the knowledge of what makes a ring a 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 a growing understanding of more complex algebraic structures, proving the lemma invmap.of_eq 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.
<details>
<summary>extracted/6256159/carbon59.png Details</summary>
### Visual Description
## Code Snippet: Lean 4 Lemma Definition
### Overview
The image is a screenshot of a code editor or terminal window displaying a single lemma written in the Lean 4 proof assistant language. The code is presented with syntax highlighting on a dark background. The content is a formal mathematical statement and its proof regarding an `invmap` function within the context of a `CoxeterSystem`.
### Components
1. **Window Frame**: A dark gray, rounded rectangular window. In the top-left corner are three colored circles (red, yellow, green), characteristic of macOS window controls.
2. **Code Area**: The main content area has a dark charcoal background (`#2d2d2d` approximate). The text is monospaced and uses syntax highlighting with the following approximate color scheme:
* Keywords (`lemma`, `by`, `simp`, `unfold`, `apply`): Light pink/salmon.
* Type/Class names (`Set`, `CoxeterSystem`): Light green.
* Function/Constructor names (`invmap.of_eq`, `Presentation.invmap`, `toMatrix`, `monoidLift.mapLift.of`): Light blue/cyan.
* Variables and symbols (`S`, `G`, `s`): White or light gray.
* Punctuation and operators (`{`, `}`, `[`, `]`, `:`, `=`, `.`): White or light gray.
### Content Details (Transcription)
The complete textual content of the code snippet is transcribed below. The language is **English**, used for the Lean 4 syntax and mathematical terms.
```lean
lemma invmap.of_eq {S:Set G} [CoxeterSystem G S] {s :S} : invmap S s = s := by
simp [CoxeterSystem.Presentation.invmap]
unfold CoxeterSystem.toMatrix
apply CoxeterSystem.monoidLift.mapLift.of
```
**Line-by-Line Breakdown:**
* **Line 1 (Lemma Declaration):** `lemma invmap.of_eq {S:Set G} [CoxeterSystem G S] {s :S} : invmap S s = s := by`
* Declares a lemma named `invmap.of_eq`.
* Implicit parameters: `S` is a `Set` of `G`; there is an instance of a `CoxeterSystem` for `G` and `S`; `s` is an element of `S`.
* The statement to prove: `invmap S s = s`.
* The proof begins with `by`.
* **Line 2 (Proof Step):** ` simp [CoxeterSystem.Presentation.invmap]`
* Uses the `simp` tactic, simplifying the goal using the definition or lemma `CoxeterSystem.Presentation.invmap`.
* **Line 3 (Proof Step):** ` unfold CoxeterSystem.toMatrix`
* Unfolds (replaces with its definition) the constant `CoxeterSystem.toMatrix`.
* **Line 4 (Proof Step):** ` apply CoxeterSystem.monoidLift.mapLift.of`
* Applies the theorem or lemma `CoxeterSystem.monoidLift.mapLift.of` to close the goal.
### Key Observations
1. **Formal Mathematics**: The code is a formal proof script in Lean 4, a dependently typed functional programming language and proof assistant.
2. **Subject Matter**: The lemma pertains to **Coxeter groups** or **Coxeter systems**, a fundamental structure in geometric group theory and algebraic combinatorics. The `invmap` likely refers to an inversion map.
3. **Proof Structure**: The proof is concise (3 tactics), suggesting the result follows directly from definitions and previously established lemmas within the formalized theory.
4. **Visual Presentation**: The syntax highlighting aids readability by distinguishing language keywords, types, and user-defined terms. The dark theme is common in modern development environments.
### Interpretation
This image captures a moment in the formal verification of mathematical theorems. The lemma `invmap.of_eq` asserts that for an element `s` in the generating set `S` of a Coxeter system, the inversion map (`invmap`) acts as the identity. This is a foundational property, as inversion is a key operation in Coxeter group theory.
The proof strategy reveals how such properties are established in a proof assistant:
1. **Simplification (`simp`)**: Leans on the core definition of `invmap` provided in the `Presentation` module.
2. **Unfolding (`unfold`)**: Exposes the underlying matrix representation of the Coxeter system (`toMatrix`), which is central to its definition.
3. **Application (`apply`)**: Uses a more general lifting property (`monoidLift.mapLift.of`) about homomorphisms from the monoid generated by `S` to the group `G`.
The snippet demonstrates the **hierarchical and modular nature** of formalized mathematics. The proof doesn't re-derive basic facts but instead chains together existing components (`Presentation.invmap`, `toMatrix`, `monoidLift`). This ensures consistency and allows complex theorems to be built from verified, reusable blocks. The existence of this lemma in a codebase implies an ongoing effort to formalize the theory of Coxeter systems, which has applications in areas like reflection groups, Lie theory, and combinatorics.
</details>
LeanAgent’s proof of invmap.of_eq involves unfolding definitions and applying specific properties of Coxeter systems. This demonstrates LeanAgent’s growing understanding relative to ReProver in abstract algebra specific to the new repository it has learned from.
Hairy Ball Theorem. Moreover, LeanAgent could not prove sorry theorems from the Hairy Ball Theorem repository during lifelong learning. However, at the end of lifelong learning, LeanAgent again demonstrates a stronger understanding relative to ReProver in algebraic topology. It proves HairyBallDiff, which states a key step in the Hairy Ball Theorem, demonstrating a grasp of vector spaces, norms, and their connections to topological concepts.
<details>
<summary>extracted/6256159/carbon60.png Details</summary>
### Visual Description
## Screenshot: Code Editor Theorem Proof
### Overview
The image is a screenshot of a dark-themed code editor or terminal window displaying a formal mathematical theorem and its proof steps. The window is centered on a light gray background. The content appears to be written in a formal proof language (likely Lean or a similar theorem prover), with syntax highlighting applied to the text.
### Components/Axes
* **Window Frame:** A dark gray rectangular window with rounded corners and a subtle drop shadow.
* **Window Controls:** Three colored circles in the top-left corner of the window, from left to right: red, yellow, green. These are standard macOS-style window control buttons.
* **Text Content:** The main body of the window contains monospaced text with syntax highlighting. The text is left-aligned.
* **Background:** The window is placed on a uniform, light gray (#d0d4da approximate) background.
### Detailed Analysis / Content Details
The text within the window is transcribed below. The syntax highlighting uses distinct colors for different language elements.
**Line 1 (Yellow):** `theorem HairyBallDiff : ∃ x, v x ≠ 0 := by`
* **Color:** The keyword `theorem` and the theorem name `HairyBallDiff` are in a yellow/gold color.
* **Content:** This line declares a theorem named `HairyBallDiff`. The statement of the theorem is `∃ x, v x ≠ 0`, which translates to "There exists an x such that v(x) is not equal to 0." The `:= by` indicates the start of the proof.
**Line 2 (White/Gray):** ` use 0`
* **Color:** The command `use` and the number `0` are in a white or light gray color.
* **Content:** This is the first step of the proof. The `use` tactic provides the witness for the existential quantifier (∃). Here, the witness chosen is `0`.
**Line 3 (Purple/Pink):** ` rw [← norm_eq_zero]`
* **Color:** The tactic `rw` (rewrite) and the lemma name `norm_eq_zero` are in a purple/pink color. The arrow `←` is also highlighted.
* **Content:** This step applies a rewrite rule. `← norm_eq_zero` indicates rewriting using the lemma `norm_eq_zero` in the reverse direction (from right to left). This likely transforms the goal `v 0 ≠ 0` into a statement about the norm of `v 0` not being zero.
**Line 4 (Purple/Pink):** ` rw [vUnit, norm_zero]`
* **Color:** Similar to line 3, the tactic `rw` and the lemma names `vUnit` and `norm_zero` are in purple/pink.
* **Content:** This step applies two rewrite rules in sequence. First, it likely rewrites using a lemma named `vUnit` (which might define the value of `v` at `0` or a unit vector). Then, it rewrites using `norm_zero`, a lemma stating that the norm of the zero vector is zero. The combined effect of these rewrites is presumably to reduce the goal to a trivial truth, completing the proof.
### Key Observations
1. **Proof Strategy:** The proof is very concise (3 tactic steps). It uses the `use` tactic to provide a specific counterexample (`0`) to the statement "for all x, v(x) = 0". The subsequent rewrites leverage existing lemmas about norms and the specific function `v` to demonstrate that `v(0)` is indeed not zero.
2. **Syntax Highlighting:** The color scheme is consistent: keywords/declarations (`theorem`) are yellow, standard tactics/numbers (`use`) are white, and rewrite tactics with lemma names (`rw [...]`) are purple/pink.
3. **Mathematical Context:** The theorem name `HairyBallDiff` strongly suggests it is related to the **Hairy Ball Theorem** from differential topology, which states that there is no non-vanishing continuous tangent vector field on an even-dimensional sphere. This theorem appears to be proving a specific differential (`Diff`) property related to it, likely showing the existence of a point where a vector field `v` is non-zero.
### Interpretation
This image captures a moment of formal verification in mathematics or computer science. It shows a successfully constructed proof for a non-trivial topological theorem within a proof assistant.
* **What it demonstrates:** The code proves the existence of a point where a vector field `v` is non-zero. Given the theorem's name, this is likely a key lemma or a reformulation used in proving or applying the Hairy Ball Theorem in a formal setting.
* **How elements relate:** The window frame and controls provide the software context (a code editor on macOS). The colored text is not merely aesthetic; it encodes syntactic structure, making the proof's logic easier for a human to follow. The sequence of tactics (`use` -> `rw` -> `rw`) shows a direct, efficient proof strategy: pick a candidate point, then use algebraic properties (of norms) and definitions to verify the condition.
* **Notable aspects:** The extreme conciseness of the proof is notable. It relies heavily on pre-proven lemmas (`norm_eq_zero`, `vUnit`, `norm_zero`), highlighting the power of building upon a library of formalized mathematics. The choice of `0` as the witness is interesting; in the context of the Hairy Ball Theorem on a sphere, `0` might represent a specific point like the north pole or a coordinate origin where the vector field's behavior is known.
</details>
Crucially, only LeanAgent could prove invmap.of_eq, wedderburn, and HairyBallDiff, demonstrating that it has developed much more advanced theorem-proving capabilities than other setups. These proofs show that LeanAgent can work with highly abstract concepts and apply them to specific mathematical objects.
### A.6 Curriculum Learning Analysis
In this section, we aim to answer the following questions: (1) Why does LeanAgent use $e^{S}$ ( $S$ = number of proof steps) as its complexity metric? (2) Why does curriculum learning work in theorem proving? (3) Why does LeanAgent use curriculum learning instead of other lifelong learning methods?
Complexity Measure. There is no universal measure of proof complexity in Lean or other formal systems. One approach, the length-based measure, involves examining the proof length (number of steps or lines) and the size of the proof term in a formal system. While these can indicate verification complexity, they may not fully capture the complexity of discovering a proof (Arana & Stafford, 2023). Moreover, within the NLP literature, many works have related input length to complexity (Zaremba & Sutskever, 2015; Cirik et al., 2016; Spitkovsky et al., ; Subramanian et al., 2017; Chang et al., 2021). Starting with shorter sequences and gradually increasing length improves model quality (Li et al., 2024).
These works demonstrate the gains from basing the complexity measure on input length. As such, we 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 consider the combinatorial explosion of possible proof paths as the length of the proof increases. As such, we choose an exponential scaling. Notably, a key strength of this choice is it is easy to compute and requires no additional hyperparameters to tune.
We now discuss some alternative complexity metrics and why we chose not to use them in LeanAgent. One option is $e^{B}$ , 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 complexity metric 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 a reliable metric for statement complexity that works across various mathematical domains could be 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-based complexity, where we order theorems based on their dependency structure within the mathematical library, wasn’t used for multiple reasons. Namely, a theorem might depend on many simple results but still be relatively easy to prove, or it might depend on a 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.
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 a proof. This makes theorem proving an ideal candidate for benefitting from curriculum learning. Moreover, curriculum learning has been shown to have an 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 a 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 LeanAgent’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 LeanAgent to learn basic proof skills, which then become building blocks for more complex proofs later on. This corroborates our analysis of LeanAgent’s progression of proof complexity. Moreover, multiple past works agree that curriculum learning provides larger gains when training data is limited (Zaremba & Sutskever, 2015; Cirik et al., 2016; Spitkovsky et al., ). This is the case in formal theorem proving, where the number of formalized theorems and proofs 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 exist, 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. However, 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 plasticity. 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 a framework, not a model, we refrain from using dynamic architecture adjustment to keep LeanAgent general to many LLM architectures. Moreover, recent work selectively updates parameters with the largest momentum magnitudes and uses selective reinitialization to maintain plasticity. However, these methods often focus on balancing performance across distinct tasks. In theorem proving, where tasks form a spectrum of increasing complexity, curriculum learning provides a more structured 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 a lifelong learning context, currently lacks standardized performance metrics. To address this concern, this section discusses a 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 it 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, it could be stated that $\text{LeanAgent TPPS}=(\text{\# ReProver Theorems Proved})+(\text{\# New Theorems Proved}*X)+1$ , where $X$ represents the importance of proving a new theorem, and $\text{ReProver TPPS}=(\text{\# ReProver Theorems Proved})+1$ . Then, $\text{Improvement Factor}=(\text{LeanAgent TPPS})/(\text{ReProver TPPS})$ .
The core idea behind TPPS is to assign a higher reward for newly proven theorems, aligning with lifelong learning objectives. However, it is important to recognize its preliminary nature and potential shortcomings. First, choosing the parameter $X$ is challenging. One approach is to choose a static value, such as $X=10$ , to standardize comparisons between LeanAgent and ReProver across diverse repositories. However, this may lead to inflated or deflated metrics on such repositories. Alternatively, $X$ 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 on 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 to 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 initially considered using proof length as a proxy for difficulty (e.g., $e^{S}$ where $S$ is the number of proof steps), we found this approach problematic during proving evaluation. LeanAgent sometimes generates shorter proofs for difficult theorems, making proof length an unreliable indicator of theorem difficulty.
These issues expose broader challenges in evaluating theorem-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 exploitation of technicalities. Moreover, metrics should consider the mathematical significance of proven theorems, 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 a step towards quantifying theorem-proving performance in a lifelong learning setting, has many limitations. Future work should focus on developing more sophisticated and robust evaluation frameworks that address these challenges. For example, we 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 on how best to evaluate and compare theorem-proving systems, particularly in the context of lifelong learning. The development of standardized, reliable metrics will be crucial for measuring progress and guiding future research in this field.