LeanDojo - Theorem Proving with Retrieval-Augmented Language Models

Watch a technical seminar presentation from MIT's Department of Electrical Engineering and Computer Science researcher Alex Gu exploring LeanDojo, an open-source platform for theorem proving using language models. Learn about this innovative system that combines large language models with retrieval capabilities to tackle formal mathematical proofs in the Lean proof assistant. Discover how LeanDojo provides comprehensive toolkits, datasets, and benchmarks while addressing key challenges in automated theorem proving through premise selection. Explore the development of ReProver, a retrieval-augmented proving system that achieves impressive results with minimal computational requirements. Understand how the platform leverages program analysis for more effective premise retrieval and features a challenging benchmark of nearly 100,000 theorems. See how this MIT-licensed project aims to advance research in machine learning-based theorem proving by providing accessible, open-source tools and models that outperform non-retrieval baselines and GPT-4.