LeanLibrary
To install LeanLibrary, run
uv pip install lean-library
install Pantograph
uv add git+https://github.com/stanford-centaur/PyPantograph
make sure you've installed CUDA-compiled torch,
uv pip install torch torchvision torchaudio --index-url https://download.pytorch.org/whl/cu126
export your Github access token,
export GITHUB_ACCESS_TOKEN=<GITHUB_ACCESS_TOKEN>
Example
from leanlibrary.agent.hf_agent import HFAgent
from leanlibrary.trainer.sft_trainer import SFTTrainer
url = "https://github.com/durant42040/lean4-example"
commit = "005de00d03f1aaa32cb2923d5e3cbaf0b954a192"
trainer = SFTTrainer(
model_name="deepseek-ai/DeepSeek-Prover-V2-7B",
output_dir="outputs-deepseek",
epochs_per_repo=1,
batch_size=2,
lr=2e-5,
)
agent = HFAgent(trainer=trainer)
agent.setup_github_repository(url=url, commit=commit)
agent.train()
agent.prove()
1 maintainer
Metadata
1 maintainer
Release files for lean-library 1.0.2
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Source distribution (sdist)
| File | Size | Uploaded | |
|---|---|---|---|
| lean_library-1.0.2.tar.gz | 126.3 kB | Details |
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Reset |
|---|---|---|---|---|
| lean_library-1.0.2-py3-none-any.whl | Python 3 | none | any | Details |
Total release size: 283.7 kB
Release files / lean_library-1.0.2.tar.gz
| Download URL | lean_library-1.0.2.tar.gz |
|---|---|
| Size | 126.3 kB |
| Tags | Source |
|
SHA-256 checksum How to use checksums |
6082b801df5882dedf7ac12a7cc9169edb1efac16f74bf88b36f0a52f128b9fd
|
|
BLAKE2b-256 checksum How to use checksums |
b0bc71d776c8b5eec7fa952306810aacebe2dae17faa10f9f3494c2390550535
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
twine/6.1.0 CPython/3.11.8
|
Release files / lean_library-1.0.2-py3-none-any.whl
| Download URL | lean_library-1.0.2-py3-none-any.whl |
|---|---|
| Size | 157.4 kB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
9b1ba8658001280a21b2fd16a1f8d8e87c3cda50871a9a94df79f9c1707cf017
|
|
BLAKE2b-256 checksum How to use checksums |
b436107bc8202209cad1aff496701704cea5bafc3ca6a3e478ae6a0fa937165f
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
twine/6.1.0 CPython/3.11.8
|
