LeanDojo: Theorem Proving in Lean Using Language Models

LeanDojo is a framework designed to enhance theorem proving in Lean using retrieval-augmented language models (LLMs). It introduces Lean Copilot, which assists users by suggesting tactics and searching for proofs, allowing for the integration of both local and cloud-based models. LeanDojo extracts proofs from Lean into datasets for training machine learning models, enabling these models to interact with Lean's proof environment effectively. The framework includes two benchmarks: LeanDojo Benchmark and LeanDojo Benchmark 4, which consist of extensive collections of theorems, proofs, tactics, and premises sourced from math libraries.

Key features of LeanDojo include detailed premise information and a challenging data split that encourages models to generalize rather than memorize proofs. The environment created by LeanDojo allows for interactive proof state observation and tactic execution, essential for training and evaluating provers. Experiments demonstrate that the ReProver model, trained on LeanDojo Benchmark, outperforms existing proof automation tactics, including those based on GPT-4.

Additionally, LeanDojo has successfully discovered new proofs and identified formalization bugs in theorem statements. A ChatGPT plugin has been developed to enable theorem proving through interaction with Lean, allowing for a blend of informal and formal mathematics, although it faces challenges in proof accuracy compared to specialized models. The team behind LeanDojo includes researchers from various institutions, contributing to advancements in automated theorem proving.