Uploaded August 2026 | Updated September 2026, 2 weeks ago
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: ycombinator.com/apply
Work at a startup: ycombinator.com/jobs
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: ycombinator.com/apply
Work at a startup: ycombinator.com/jobs
