LeanAgent: Lifelong Learning for Formal Theorem Proving

Adarsh Kumarappan, Mo Tiwari, Peiyang Song +3

Large Language Models (LLMs) have been successful in mathematical reasoning tasks such as formal theorem proving when integrated with interactive proof assistants like Lean. Existi…