# LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

**Authors:** Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar  
**arXiv:** [2306.15626](https://arxiv.org/abs/2306.15626)  
**Date:** 2023-06-27  
**Summary page:** https://www.summarizepaper.com/en/paper/2306.15626v1/

## Key points

- Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean.
- LeanDojo is introduced as an open-source Lean playground that addresses issues of private code, data, and large compute requirements in research on machine learning methods for theorem proving.
- LeanDojo provides fine-grained annotations of premises in proofs, which is valuable for premise selection—a key bottleneck in theorem proving.
- ReProver is developed as the first LLM-based prover augmented with retrieval for selecting relevant premises from a vast math library.
- ReProver requires only one GPU week of training and is cost effective.
- A new benchmark comprising 96,962 theorems and proofs extracted from Lean's math library is constructed.
- Experimental results demonstrate that ReProver outperforms non-retrieval baselines and GPT-4 in terms of effectiveness.
- The work provides open-source LLM-based theorem provers without proprietary datasets released under a permissive MIT license to facilitate further research.
- The new benchmark and experimental results validate the performance of ReProver and contribute to advancing research in this field.

## Summary

Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. To address the issue of private code, data and large compute requirements that create substantial barriers to research on machine learning methods for theorem proving, the authors introduce LeanDojo: an open-source Lean playground that includes toolkits, data, models and benchmarks. It provides fine-grained annotations of premises in proofs which is valuable for premise selection—a key bottleneck in theorem proving. Leveraging this data, the authors develop ReProver (Retrieval-Augmented Prover), which is the first LLM-based prover augmented with retrieval for selecting relevant premises from a vast math library. Notably, ReProver requires only one GPU week of training and is cost effective. Additionally, they construct a new benchmark comprising 96,962 theorems and proofs extracted from Lean's math library. Experimental results demonstrate that ReProver outperforms non-retrieval baselines and GPT-4 in terms of effectiveness. This work provides a set of open-source LLM-based theorem provers without any proprietary datasets released under a permissive MIT license to facilitate further research in this area. The new benchmark and experimental results validate the performance of ReProver and contribute to advancing research in this field.