2025
LeanAgent: Lifelong Learning for Formal Theorem Proving
ICLR 2025poster
Large Language Models (LLMs) have been successful in mathematical reasoning tasks such as formal theorem proving when integrated with interactive proof assistants like Lean. Existing approaches involve training or fine-tuning an LLM on a specific dataset to perform well on particular domains, such a…