LeanDojo: Theorem Proving in Lean Using LLMs

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 to prove theorems. The framework includes two benchmarks: LeanDojo Benchmark and LeanDojo Benchmark 4, which consist of extensive collections of theorems, proofs, tactics, and premises from math libraries. A key feature is the fine-grained annotation of premises, which aids in premise selection, a critical aspect of theorem proving. LeanDojo also addresses performance overestimation by implementing a challenging data split that requires models to generalize to new premises. The environment allows for interactive proof state observation and feedback, essential for training and evaluating provers. Experiments show that the ReProver model, trained on LeanDojo Benchmark, outperforms existing proof automation tactics. Additionally, ReProver has successfully discovered new proofs and identified formalization bugs in theorem statements. A ChatGPT plugin for LeanDojo enables informal interactions with theorem proving, although it faces challenges in finding correct proofs compared to specialized models. The team behind LeanDojo includes researchers from various institutions, contributing to the advancement of automated theorem proving.