# LeanAgent: Lifelong Learning for Formal Theorem Proving

**Authors:** Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, Anima Anandkumar  
**arXiv:** [2410.06209](https://arxiv.org/abs/2410.06209)  
**Date:** 2024-10-08  
**Summary page:** https://www.summarizepaper.com/en/paper/2410.06209v1/

## Key points

- Large Language Models (LLMs) integrated with interactive proof assistants like Lean show promise in formal theorem proving tasks
- Existing approaches struggle with generalizability to advanced mathematics due to their static nature and limited adaptability
- LeanAgent is a novel lifelong learning framework that addresses these limitations
- Incorporates curriculum learning strategy based on mathematical difficulty
- Utilizes dynamic database for efficient management of expanding mathematical knowledge
- Implements progressive training to balance stability and plasticity
- LeanAgent successfully proves challenging theorems in domains like abstract algebra and algebraic topology, outperforming static LLM baselines by up to 11 times
- Notable achievement: ability to continuously generalize and improve on mathematical knowledge without forgetting previously learned information
- Excels in stability and backward transfer metrics, demonstrating continuous generalizability and improvement in theorem proving tasks
- Handles evolving complexity of mathematical theorems while maintaining stability and plasticity essential for lifelong learning
- Achieves near-perfect composite lifelong learning scores of 94%, emphasizing continuous generalizability and improvement

## Summary

, , , , 

In the realm of mathematical reasoning, Large Language Models (LLMs) have shown promise in tasks such as formal theorem proving when integrated with interactive proof assistants like Lean. However, existing approaches struggle with generalizability to advanced mathematics due to their static nature and limited ability to adapt to evolving complexity. To address these limitations, a novel lifelong learning framework called LeanAgent has been introduced. LeanAgent incorporates several key innovations, including a curriculum learning strategy that optimizes the learning trajectory based on mathematical difficulty, a dynamic database for efficient management of expanding mathematical knowledge, and progressive training to balance stability and plasticity. Through extensive experiments across diverse Lean repositories, LeanAgent has successfully proven 162 challenging theorems previously unproved by humans in domains like abstract algebra and algebraic topology. One of LeanAgent's notable achievements is its ability to continuously generalize and improve on ever-expanding mathematical knowledge without forgetting previously learned information. It outperforms static LLM baselines by up to 11 times and showcases a clear progression from basic concepts to advanced topics. Additionally, LeanAgent excels in stability and backward transfer metrics, demonstrating its continuous generalizability and improvement in theorem proving tasks. Furthermore, LeanAgent's success lies in its ability to handle the evolving complexity of mathematical theorems while maintaining stability and plasticity essential for lifelong learning. By incorporating curriculum learning and progressive training methods, LeanAgent achieves near-perfect composite lifelong learning scores of 94%, emphasizing its continuous generalizability and improvement. Overall, LeanAgent represents a significant advancement in lifelong learning for theorem proving by bridging the gap between static approaches and the dynamic nature of advanced mathematics.