YC Root AccessLeanAgent: Lifelong Learning for Formal Theorem Proving
CHAPTERS
- 0:07 – 0:14
LeanAgent in one sentence: lifelong learning for formal theorem proving
Ankit introduces Adarsh and his ICLR work, LeanAgent, positioning it as a solution to continual/lifelong learning in a demanding domain: formal mathematics. The conversation frames the core challenge as improving over time without catastrophic forgetting.
- •Context: presented at YCML; work previously presented at ICLR
- •LeanAgent targets continual/lifelong learning
- •Formal theorem proving chosen as a challenging testbed
- •Goal: learn new material while retaining earlier knowledge
- 0:14 – 0:45
Stability vs. plasticity: the core trade-off in continual learning
Adarsh explains the two failure modes of continual learning: models that become too stable (frozen) and models that are too plastic (forgetful). LeanAgent is designed to land in the “sweet spot” between these extremes.
- •Excess stability prevents learning new information
- •Excess plasticity causes catastrophic forgetting
- •Lifelong learning requires balancing both forces
- •Motivation for designing training/update rules that preserve prior capability
- 0:45 – 1:33
Why formal math is an ideal stress test (and what ‘backward transfer’ means)
The discussion motivates math as cumulative and prerequisite-driven, making it a natural curriculum domain. Adarsh introduces backward transfer: learning later concepts can improve performance on earlier ones, creating a nuanced view of “forgetting vs. updating.”
- •Math builds hierarchically (algebra → calculus/analysis, etc.)
- •Curriculum ordering matters in cumulative domains
- •Backward transfer: new learning can improve earlier skills
- •Trade-off isn’t purely about retaining old knowledge unchanged
- 1:33 – 2:03
Lean basics: proofs as code, tactics, premises, and goals
Adarsh describes Lean as a programming language where proofs are written like code and verified by a compiler. He breaks down the interactive proving workflow: tactics consume premises to transform goals until there are “no goals left.”
- •Lean proofs are code checked by the compiler
- •IDE shows hypotheses and current goal state
- •Tactics are function-like proof steps
- •Premises are prior theorems/lemmas/definitions used as inputs
- 2:03 – 2:34
The bottleneck: retrieving the right premises in an ever-growing math library
With huge numbers of interconnected theorems, selecting relevant premises at each proof step becomes a central challenge. The problem compounds over time as repositories and theorem collections expand, making retrieval and non-forgetting tightly linked.
- •Premise selection is difficult due to massive theorem sets
- •Math is highly interconnected, increasing retrieval ambiguity
- •Growth over time raises continual-learning pressures
- •LeanAgent targets retrieval quality while preserving older knowledge
- 2:34 – 3:10
Agentic pipeline overview: scrape repos and build an easy-to-hard curriculum
LeanAgent begins by scraping GitHub for Lean repositories and then automatically infers a curriculum from foundational to advanced material. This mirrors how humans progress through math topics by mastering simpler theorems before harder ones.
- •Automated discovery of Lean code via GitHub scraping
- •Need for curriculum learning across many repositories
- •Ordering content from easy to hard to enable accumulation
- •Continual agent receives iteratively harder math over time
- 3:10 – 3:40
How LeanAgent measures difficulty and sorts repositories
Adarsh explains a practical heuristic: theorem complexity grows exponentially with the number of proof steps, and this helps categorize theorems as easy/medium/hard. Repositories are then ordered by their distribution (e.g., more easy theorems first) to construct the training curriculum.
- •Difficulty proxy: exponential in number of proof steps
- •Compute distributions of easy/medium/hard per repo
- •Sort repositories to prioritize foundational content
- •Curriculum drives the rest of the learning loop
- 3:40 – 4:10
Dynamic database + one-epoch updates: the ‘brain’ that balances forgetting and learning
LeanAgent maintains a dynamic database storing theorems, premises, and proofs as it progresses. To balance stability and plasticity, it takes the latest retriever and trains it only briefly (one epoch) on new material to incorporate new premises without overwriting old ones.
- •Dynamic database stores proofs, premises, and learned artifacts
- •Retriever is continually updated to reflect newest knowledge
- •One-epoch training as a simple stability/plasticity control
- •Emphasis: learn new premises while retaining earlier retrieval ability
- 4:10 – 4:21
Proving loop: retrieval → tactic generation → best-first tree search → add new proofs
Once updated, the retriever feeds a tactic generator that expands a proof search tree. LeanAgent uses best-first tree search with practical controls (backtracking, timeouts), and successful new proofs are written back into the database, creating a self-improving cycle.
- •Retriever supplies relevant premises for each proof step
- •Tactic generator proposes next proof actions
- •Best-first tree search explores proof states efficiently
- •Backtracking/timeouts manage search; found proofs are stored for future use
- 4:21 – 4:37
What “train for one epoch” means in practice for Lean code corpora
Ankit clarifies that the training is effectively a pass over the newly collected code/proofs, updating the underlying model used for retrieval. Adarsh confirms the interpretation, reinforcing the simplicity of the update step within the broader agentic system.
- •One epoch = one pass over the latest repository/corpus slice
- •Model is updated with Lean code/proof data
- •Update is lightweight relative to full retraining
- •Fits the continual-learning framing of incremental improvement
- 4:37 – 5:28
Results and the emergent benefit: backward transfer across domains
Adarsh reports LeanAgent proved 155 new formal proofs across 23 domains, including areas associated with Terence Tao’s repositories. Beyond non-forgetting, the system exhibited backward transfer—new learning improving earlier-domain performance—supporting the lifelong learning thesis.
- •155 new formal proofs across 23 domains
- •Includes combinatorics and other advanced areas (e.g., Tao-related domains)
- •Demonstrates learning without forgetting
- •Backward transfer observed: later learning boosts earlier performance
- 5:28 – 6:50
Looking forward: stronger base models, small-model practicality, and search vs. RL
The conversation closes on how the approach might change with today’s more capable coding/math agents and improved open-source models. Adarsh suggests upgrading base models (while keeping them runnable), and argues step-by-step tree search remains valuable versus more expensive test-time RL, akin to an AlphaEvolve-style search-centric strategy.
- •Debate on where Lean is most useful across domains
- •Base model upgrades (beyond ByT5) could improve performance
- •Small models are intentional for accessibility and local execution
- •Tree search remains effective; test-time RL can work but is costly
