LeanDojo: Machine Learning for Theorem Proving in Lean

LeanDojo overview

LeanDojo is a Python library for learning–based theorem provers in Lean, supporting both Lean 3 and Lean 4. It provides two main features:

  • Extracting data (proof states, tactics, premises, etc.) from Lean repos.

  • Interacting with Lean programmatically.


  title={{LeanDojo}: Theorem Proving with Retrieval-Augmented Language Models},
  author={Yang, Kaiyu and Swope, Aidan and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima},
  booktitle={Neural Information Processing Systems (NeurIPS)},


Indices and Tables