LeanAgent: Lifelong Learning for Formal Theorem Proving

The Breakthrough

LeanAgent establishes a lifelong learning framework for formal mathematics that successfully balances model stability and plasticity, enabling an agent to learn new mathematical domains without forgetting previously mastered concepts while demonstrating backward transfer.

What Actually Worked

• Curriculum Construction: The system scrapes GitHub for Lean repositories and sorts them by difficulty, calculated as an exponential function of the number of proof steps, to ensure the agent learns foundational mathematics before advancing to complex topics.
• Single-Epoch Training: The retriever model is updated for only one epoch per repository to maintain the balance between learning new premises and retaining existing knowledge.
• Tree Search Proving: The agent employs a best-first tree search that utilizes the updated retriever to suggest tactics and premises, allowing for backtracking and timeout handling during proof construction.
• Dynamic Database Integration: Newly generated proofs are fed back into the dynamic database, which serves as the agent's central knowledge store for all previously proven theorems, lemmas, and definitions.

Before / After

• Performance: The framework successfully generated 155 new formal proofs across 23 distinct mathematical domains.
• Backward Transfer: The agent exhibited improved performance on earlier, simpler domains (such as algebra) after training on more advanced, subsequent domains (such as topology).

Context

Formal theorem proving in the Lean programming language presents a significant challenge for AI because the domain is inherently cumulative, requiring the agent to build upon a vast, interconnected web of previously proven premises. The primary hurdle in continual learning is avoiding catastrophic forgetting, where a model loses its ability to perform on old tasks as it incorporates new information. LeanAgent addresses this by treating the learning process as a structured curriculum, similar to human education, and using a search-based approach to navigate the proof space.

Content References

• Tool: Lean, an open-source theorem prover and programming language, mentioned as the core environment for formal proof verification.
• Tool: ByT5, a byte-level transformer model from Google, cited as the base model used in the original research.
• Tool: Gemma, a family of open-source models from Google, mentioned as a potential modern replacement for the original base model.
• Paper: LeanAgent: Lifelong Learning for Formal Theorem Proving, presented at ICLR, authored by Adarsh Kumarappan et al., reviewed as the primary subject of the video.