LeanDojo: Machine Learning for Theorem Proving in Lean
Project description
LeanDojo: Machine Learning for Theorem Proving in Lean
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.
Requirements
- Linux or macOS
- Git >= 2.25
- Python >= 3.9
- Docker strongly recommended
Installation
LeanDojo is available on PyPI and can be installed via pip:
pip install lean-dojo
It can also be installed locally from this Git repo:
pip install .
Documentation
LeanDojo's documentation is available on Read the Docs.
Related Links
- LeanDojo Website: The official website of LeanDojo.
- LeanDojo Benchmark: The dataset used in our paper, consisting of 96,962 theorems and proofs extracted from mathlib by generate-benchmark-lean3.ipynb.
- LeanDojo Benchmark 4: The Lean 4 version of LeanDojo Benchmark, consisting of 91,766 theorems and proofs extracted from mathlib4 by generate-benchmark-lean4.ipynb.
- ReProver: The ReProver (Retrieval-Augmented Prover) model in our paper.
Citation
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Under review, NeuIPS (Datasets and Benchmarks Track), 2023
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala,
Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar
@article{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},
journal={arXiv preprint arXiv:xxxx.xxxxx},
year={2023}
}
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
lean_dojo-1.0.0.tar.gz
(123.1 kB
view hashes)
Built Distribution
lean_dojo-1.0.0-py3-none-any.whl
(72.1 kB
view hashes)
Close
Hashes for lean_dojo-1.0.0-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 4ecf4736ea7ce6171987e4249dfb6600a634a5114429963bad0beea5be951207 |
|
MD5 | 47ebe5ec5ef4dc8e33144529a452c3aa |
|
BLAKE2b-256 | 18071f69f56301d59647a82dd1723bf196c8a387ca551402baf4cccf190136a7 |