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 the Git repo:
pip install .
Documentation
Questions and Bugs
- For general questions and discussions, please use GitHub Discussions.
- To report a potential bug, please open an issue.
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.
- LeanDojo ChatGPT Plugin
Citation
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Under review, NeurIPS (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:2306.15626},
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.1.1.tar.gz
(68.4 kB
view hashes)
Built Distribution
lean_dojo-1.1.1-py3-none-any.whl
(73.0 kB
view hashes)
Close
Hashes for lean_dojo-1.1.1-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 86b591e064cc381e6e90ebe4148b8de25a0f38c120533718730631d9d580164a |
|
MD5 | 82315af8a8e10b0509b53640f6b205b3 |
|
BLAKE2b-256 | e8ce113f1267f5896d80bc094fdf9ed62794272ec6f556cdb019051969de534c |