# LeanAgent: Lifelong Learning for Formal Theorem Proving

arXiv: https://arxiv.org/abs/2410.06209 · HTML: https://mlsanity.com/paper/2410.06209/

## Key facts

- Cited by 35 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 42 of its 85 references that are in the map.
- First posted on arXiv 8 Oct 2024.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 30 of 42)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Overcoming catastrophic forgetting in neural networks](https://mlsanity.com/paper/1612.00796/) (2016)
- [Learning without Forgetting](https://mlsanity.com/paper/1606.09282/) (2016)
- [Gradient Episodic Memory for Continual Learning](https://mlsanity.com/paper/1706.08840/) (2017)
- [Improving language models by retrieving from trillions of tokens](https://mlsanity.com/paper/2112.04426/) (2021)
- [Continual Learning with Deep Generative Replay](https://mlsanity.com/paper/1705.08690/) (2017)
- [Efficient Lifelong Learning with A-GEM](https://mlsanity.com/paper/1812.00420/) (2018)
- [A Comprehensive Survey of Continual Learning: Theory, Method and Application](https://mlsanity.com/paper/2302.00487/) (2023)
- [ByT5: Towards a token-free future with pre-trained byte-to-byte models](https://mlsanity.com/paper/2105.13626/) (2021)
- [GaLore: Memory-Efficient LLM Training by Gradient Low-Rank Projection](https://mlsanity.com/paper/2403.03507/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [DocPrompting: Generating Code by Retrieving the Docs](https://mlsanity.com/paper/2207.05987/) (2022)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [ReACC: A Retrieval-Augmented Code Completion Framework](https://mlsanity.com/paper/2203.07722/) (2022)
- [Don't forget, there is more than forgetting: new metrics for Continual Learning](https://mlsanity.com/paper/1810.13166/) (2018)
- [Learning to Execute](https://mlsanity.com/paper/1410.4615/) (2014)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Continual Learning and Catastrophic Forgetting](https://mlsanity.com/paper/2403.05175/) (2024)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [Continual evaluation for lifelong learning: Identifying the stability gap](https://mlsanity.com/paper/2205.13452/) (2022)
- [FIMO: A Challenge Formal Dataset for Automated Theorem Proving](https://mlsanity.com/paper/2309.04295/) (2023)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)

## Built on by (most cited first, 30 of 35)

- [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025)
- [MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving](https://mlsanity.com/paper/2503.03205/) (2025)
- [FEABench: Evaluating Language Models on Multiphysics Reasoning Ability](https://mlsanity.com/paper/2504.06260/) (2025)
- [Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skills](https://mlsanity.com/paper/2512.16301/) (2025)
- [Large Language Model Reasoning Failures](https://mlsanity.com/paper/2602.06176/) (2026)
- [REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning](https://mlsanity.com/paper/2505.20613/) (2025)
- [LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction](https://mlsanity.com/paper/2502.17925/) (2025)
- [MerLean: An Agentic Framework for Autoformalization in Quantum Computation](https://mlsanity.com/paper/2602.16554/) (2026)
- [Autonomous Research Agents: A Survey of AI Scientists and the Verification Gap](https://mlsanity.com/paper/2608.05179/) (2026)
- [RLMEval: Evaluating Research-Level Neural Theorem Proving](https://mlsanity.com/paper/2510.25427/) (2025)
- [SorryDB: Can AI Provers Complete Real-World Lean Theorems?](https://mlsanity.com/paper/2603.02668/) (2026)
- [Diverse Inference and Verification for Advanced Reasoning](https://mlsanity.com/paper/2502.09955/) (2025)
- [Towards trustworthy agentic AI: a comprehensive survey of safety, robustness, privacy, and system security](https://mlsanity.com/paper/2605.23989/) (2026)
- [Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance](https://mlsanity.com/paper/2606.14000/) (2026)
- [OpenAI-o1 AB Testing: Does the o1 model really do good reasoning in math problem solving?](https://mlsanity.com/paper/2411.06198/) (2024)
- [The Agentic Researcher: A Practical Guide to AI-Assisted Research in Mathematics and Machine Learning](https://mlsanity.com/paper/2603.15914/) (2026)
- [A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam](https://mlsanity.com/paper/2504.04945/) (2025)
- [Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair](https://mlsanity.com/paper/2605.17475/) (2026)
- [Interactive Evaluation Requires a Design Science](https://mlsanity.com/paper/2605.17829/) (2026)
- [Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving](https://mlsanity.com/paper/2503.09730/) (2025)
- [Vero: Can AI Agents Build Formally Verified Software Repositories?](https://mlsanity.com/paper/2608.13522/) (2026)
- [CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization](https://mlsanity.com/paper/2502.18532/) (2025)
- [Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4](https://mlsanity.com/paper/2604.15839/) (2026)
- [Benchmarking Testing in Automated Theorem Proving](https://mlsanity.com/paper/2604.23698/) (2026)
- [Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory](https://mlsanity.com/paper/2606.20642/) (2026)
- [Decodable but Not Faithful: Coupling Natural-Language Rationales to Programmatic Verifiers](https://mlsanity.com/paper/2606.21678/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [LLM Framework for Discovering Major Mathematical Conjectures: AI's Quest for the Next Riemann Hypothesis](https://mlsanity.com/paper/2607.28632/) (2026)
- [Deep Learning based discovery of Integrable Systems](https://mlsanity.com/paper/2503.10469/) (2025)
- [Domain Adapted Large Language Models for Additive Manufacturing](https://mlsanity.com/paper/2603.22017/) (2026)

## Abstract (arXiv)

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.