Research map / Large language models / Agents, code and math
LeanAgent: Lifelong Learning for Formal Theorem Proving
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes LeanAgent, a lifelong learning framework that curriculum-orders Lean repositories by theorem difficulty, progressively trains a ReProver-style premise retriever, and proves 162 sorry theorems across 22 Lean repositories.
Problem
LLM-based theorem provers for Lean are trained on static datasets (e.g., LeanDojo4/mathlib4) and fail to generalize to research-level mathematics across evolving Lean repositories, suffering catastrophic forgetting when adapted sequentially.
Approach
Treats formalization across Lean repositories as a lifelong learning stream: repositories are ordered by a curriculum based on theorem difficulty (exponential in proof steps), the ByT5-based retriever is progressively trained one epoch per repository with stability/plasticity metrics, and a dynamic database supports single-repo dataset construction and sorry-theorem proving.
Key results
- LeanAgent achieves 75.34% lower WF5, 59.97% lower FM, and 16.25% higher Expanded BWT than the next best single-repo setup, with a composite score of 0.9357 vs 0.6107.
- LeanAgent proves 162 previously unproven sorry theorems across 22 Lean repositories, including PFR formalization content, abstract algebra and algebraic topology theorems.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use LeanAgent's single-repository curriculum training (Exp3) rather than the next-best single-repository setup (Exp8) | ReProver retriever in single-repo lifelong learning · Single-repo lifelong learning | WF5: 75.34% lower WF5 | Helped |
| Use LeanAgent's single-repository curriculum training (Exp3) rather than the next-best single-repository setup (Exp8) | ReProver retriever in single-repo lifelong learning · Single-repo lifelong learning | FM: 59.97% lower FM | Helped |
| Use LeanAgent's single-repository curriculum training (Exp3) rather than the next-best single-repository setup (Exp7) | ReProver retriever in single-repo lifelong learning · Single-repo lifelong learning | Expanded BWT: 16.25% higher Expanded BWT | Helped |
| Use LeanAgent's single-repository curriculum training (Exp3) rather than Exp8 | ReProver retriever in single-repo lifelong learning · Single-repo lifelong learning | Composite Score: 0.6107 -> 0.9357 | Helped |
| Use Exp8's curriculum/EWC-related setup rather than LeanAgent (Exp3) | ReProver retriever in single-repo lifelong learning · Single-repo lifelong learning | WP5: 38.26% higher Windowed Plasticity (WP5) | Helped |
| Use curriculum ordering instead of decreasing GitHub-star popularity ordering | Lifelong-learning experiment setups · Single-repo and merge-all lifelong learning | Composite Score | Helped |
| Use merge-all training (Exp4) rather than the next-best merge-all setup | ReProver retriever in merge-all lifelong learning · Merge-all lifelong learning | WF5: 61.68% lower WF5 | Helped |
| Use merge-all training (Exp4) rather than the next-best merge-all setup | ReProver retriever in merge-all lifelong learning · Merge-all lifelong learning | Expanded BWT: 466.63% improvement in Expanded BWT | Helped |
| Use merge-all training rather than single-repository training | Lifelong-learning retriever · Merge-all lifelong learning | IP | Hurt |
| Use the single-repo approach rather than merge-all dataset construction | LeanAgent lifelong learning · Lifelong theorem proving | Composite Score | Helped |
| Add EWC under curriculum-based ordering | Lifelong-learning retriever · Lifelong learning | stability | Hurt |
| Add EWC under GitHub-stars-based ordering | Lifelong-learning retriever · Lifelong learning | stability | Mixed |
Surprising findings
- Merge-all dataset strategies showed negative Incremental Plasticity across all experiments, suggesting difficulty adapting to growing combined datasets.
- Training with more emphasis on plasticity (e.g., EWC plus curriculum in experiment 8) led to catastrophic forgetting of trivial theorems that the stability-focused setup still proved.
Limitations
- Metrics such as WF5 and FM have ambiguous interpretation in the merge-all setting, which the authors acknowledge.
- Evaluation relies on a small set of repositories (14 for lifelong analysis) and a single run per setup, with a 10-minute proof-search timeout.
- Appendix contains unfinished TODO placeholders, and the paper lacks a rigorous justification for the composite score weights and lambda=0.1.
Experimental setup
Datasets: LeanDojo4 Benchmark ProofNet LeanEuclid Lean repositories (Mathematics in Lean, SciLean, PFR, MiniF2F, Coxeter, Hairy Ball)
Benchmarks: LeanDojo Benchmark repositories (22 Lean repos) sorry theorems in Lean repositories
Metrics: Validation R@10 Average test R@10 WF5 FM CFR Expanded BWT WP5 IP composite lifelong learning score number of sorry theorems proved
Baselines: ReProver with retrieval ReProver without retrieval EWC-based and merge-all lifelong learning setups
Builds on: ReProver LeanDojo Elastic Weight Consolidation
Closest papers by meaning
- Lean-STaR: Learning to Interleave Thinking and Proving (ICLR 2025 · similarity 0.90)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.89)
- MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving (ICML 2025 · similarity 0.89)
- HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs (ICML 2026 · similarity 0.89)
- ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.89)
- Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics (ICML 2026 · similarity 0.89)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.