Tool for data extraction and interacting with Lean programmatically.
LeanDojo is a Python library for learning–based theorem provers in Lean, providing two main features:
LeanDojo's current version is compatible with Lean 4 v4.3.0-rc2
or later. We strongly suggest using the current version. However, you may use the legacy
branch if you want to work with earlier versions (including Lean 3).
GITHUB_ACCESS_TOKEN
to itLeanDojo is available on PyPI and can be installed via pip:
pip install lean-dojo
It can also be installed locally from the Git repo:
pip install .
VERBOSE
to 1). The more details you provide, the better we will be able to help you.LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Neural Information Processing Systems (NeurIPS), 2023
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala,
Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar
@inproceedings{yang2023leandojo,
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)},
year={2023}
}