LeanDojo is an open-source platform for AI theorem proving in the Lean proof assistant, described in “LeanDojo: Theorem Proving with Retrieval-Augmented Language Models” (arXiv, June 2023, by Kaiyu Yang, Anima Anandkumar, and colleagues), presented as an oral at the NeurIPS 2023 Datasets and Benchmarks track. It extracts data from Lean and lets programs interact with the proof environment, turning formal proving into an environment that machine learning systems can train and be evaluated against.
The release has three parts: the LeanDojo toolkit and data-extraction tools; a benchmark of 98,734 theorems and proofs drawn from Lean’s mathematics library, including splits that test whether a prover can use premises it never saw in training; and ReProver, a language-model prover that retrieves relevant lemmas from the math library before generating each proof step. Retrieval matters because a formal library contains far too many lemmas to fit in a prompt, so the model must find the right ones. Everything was released under the MIT license without proprietary data, addressing reproducibility problems in earlier theorem-proving research.
LeanDojo became a widely used foundation for neural theorem proving and helped make Lean a common target for AI math systems. For a general reader it shows how the retrieval-augmented pattern from language models transfers to rigorous, machine-checkable mathematics, where every step must be formally valid.