LeanAgent: Lifelong Learning for Formal Theorem Proving

At our inaugural YCML at Startup School, YC Partner Ankit Gupta speaks with Adarsh Kumarappan about LeanAgent, a continual learning framework for proving formal mathematics in Lean. LeanAgent builds a curriculum from Lean repositories, learns to retrieve relevant mathematical premises, and uses tree search to construct proofs. The goal is to let a theorem-proving system learn new mathematics without forgetting what it already knows. In the paper, LeanAgent produced 155 new formal proofs across 23 domains and demonstrated backward transfer, where learning new subjects also improved its performance on earlier ones. Apply to Y Combinator: https://www.ycombinator.com/apply Work at a startup: https://www.ycombinator.com/jobs

Ankit GuptahostAdarsh Kumarappanguest

Aug 6, 20266mWatch on YouTube ↗

EPISODE INFO

Released: August 6, 2026
Duration: 6m
Channel: YC Root Access
Watch on YouTube: ▶ Open ↗

EPISODE DESCRIPTION

At our inaugural YCML at Startup School, YC Partner Ankit Gupta speaks with Adarsh Kumarappan about LeanAgent, a continual learning framework for proving formal mathematics in Lean. LeanAgent builds a curriculum from Lean repositories, learns to retrieve relevant mathematical premises, and uses tree search to construct proofs. The goal is to let a theorem-proving system learn new mathematics without forgetting what it already knows. In the paper, LeanAgent produced 155 new formal proofs across 23 domains and demonstrated backward transfer, where learning new subjects also improved its performance on earlier ones. Apply to Y Combinator: https://www.ycombinator.com/apply Work at a startup: https://www.ycombinator.com/jobs

SPEAKERS

Ankit Gupta
host
Host/interviewer for YC Root Access (Y Combinator).
Adarsh Kumarappan
guest
Researcher presenting LeanAgent, a lifelong/continual learning approach for formal theorem proving in Lean.

EPISODE SUMMARY

In this episode of YC Root Access, featuring Ankit Gupta and Adarsh Kumarappan, LeanAgent: Lifelong Learning for Formal Theorem Proving explores leanAgent uses lifelong learning to improve automated Lean theorem proving LeanAgent frames formal theorem proving in Lean as a lifelong learning problem, balancing stability (not forgetting) and plasticity (learning new material).

RELATED EPISODES