Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/lean-dojo/LeanDojo-v2/llms.txt

Use this file to discover all available pages before exploring further.

This guide takes you from a fresh LeanDojo v2 installation to a working proof search in the shortest possible path. You will trace a real Lean 4 GitHub repository, build a supervised fine-tuning dataset from its sorry theorems, train a DeepSeek-Prover model on that dataset, and watch the prover close those sorrys automatically. If you do not have a GPU available, the final step shows how to do the same thing using the Hugging Face Inference API with no local model loading.
This guide assumes LeanDojo v2, Pantograph, and PyTorch are already installed and that GITHUB_ACCESS_TOKEN is exported. If not, complete the Installation page first.
1

Export your GitHub access token

The tracing pipeline calls the GitHub API to clone repositories and resolve commits. Export your token before doing anything else:
export GITHUB_ACCESS_TOKEN=ghp_your_token_here
The token must have repo and read:org scopes. LeanDojo v2 raises a ValueError at import time if GITHUB_ACCESS_TOKEN is unset or invalid.
2

Install the package

pip install lean-dojo-v2
pip install git+https://github.com/stanford-centaur/PyPantograph
pip install torch torchvision torchaudio --index-url https://download.pytorch.org/whl/cu126
3

Train and prove with HFAgent + SFTTrainer

This is the core workflow. HFAgent orchestrates three operations in sequence: tracing the repository, fine-tuning the model, and running proof search.
from lean_dojo_v2.agent.hf_agent import HFAgent
from lean_dojo_v2.trainer.sft_trainer import SFTTrainer

url = "https://github.com/durant42040/lean4-example"
commit = "b14fef0ceca29a65bc3122bf730406b33c7effe5"

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()
Save this as run_sft.py and execute it with python run_sft.py. The first run downloads and traces the repository, which may take several minutes depending on your internet connection and CPU count.
To use LoRA adapters instead of full fine-tuning, pass a peft.LoraConfig instance to SFTTrainer. This drastically reduces GPU memory requirements and is recommended for consumer-grade hardware.
4

Try the ExternalAgent (no GPU required)

ExternalAgent delegates all inference to the Hugging Face Inference API, so no local model weights are loaded. This is ideal for quick experiments or when you need the raw capacity of a 671B parameter model.
from lean_dojo_v2.agent import ExternalAgent

url = "https://github.com/durant42040/lean4-example"
commit = "3e23ab0bfdcfdbd5b11ab53c2cd8b5d16492e9c2"

agent = ExternalAgent(model_name="deepseek-ai/DeepSeek-Prover-V2-671B:novita")
agent.setup_github_repository(url, commit)
agent.prove(whole_proof=True)
The whole_proof=True flag instructs ExternalProver to generate a complete proof in one forward pass rather than searching through a tactic tree step by step — this is faster and works well with very capable models.
Set HF_TOKEN in your environment if your chosen model requires authentication: export HF_TOKEN=hf_your_token_here.
5

Understand what happened

Whether you used HFAgent or ExternalAgent, the framework executed the same pipeline under the hood:
  1. Clone & trace — setup_github_repository() cloned the target commit and ran Lean 4 with the instrumented ExtractData.lean module, capturing every theorem’s proof state, tactic sequence, and sorry location.
  2. Build dataset — Traced artifacts were converted to JSONL records and loaded into a DynamicDatabase, sorted by curriculum difficulty.
  3. Fine-tune (HFAgent only) — SFTTrainer ran supervised fine-tuning on the sorry theorems, writing a checkpoint to outputs-deepseek/.
  4. Proof search — The prover (either HFProver loading the local checkpoint, or ExternalProver calling the API) communicated with Pantograph’s Lean RPC server, generating tactics or whole proofs and validating each against the live Lean kernel until every sorry was closed or the budget was exhausted.

​
Exploring Further Examples

The examples/ directory in the repository contains ready-to-run scripts for every major workflow: 
import torch
from lean_dojo_v2.agent.hf_agent import HFAgent
from lean_dojo_v2.trainer.grpo_trainer import GRPOTrainer


def reward_func(completions, **kwargs):
    return torch.tensor([1.0] * len(completions))


url = "https://github.com/durant42040/lean4-example"
commit = "b14fef0ceca29a65bc3122bf730406b33c7effe5"

trainer = GRPOTrainer(
    model_name="deepseek-ai/DeepSeek-Prover-V2-7B",
    output_dir="outputs-deepseek",
    reward_func=reward_func,
    epochs_per_repo=1,
    batch_size=8,
    lr=2e-5,
)

agent = HFAgent(trainer=trainer)
agent.setup_github_repository(url=url, commit=commit)
agent.train()
agent.prove()

​
Next Steps

Agents Guide

Deep dive into HFAgent, LeanAgent, and ExternalAgent. Learn how to extend BaseAgent with your own trainer/prover pair.

Trainers Guide

Explore SFTTrainer, GRPOTrainer, and RetrievalTrainer — including LoRA configuration, DeepSpeed integration, and reward functions.

Architecture

Understand how the tracing pipeline, DynamicDatabase, agents, trainers, and provers fit together end to end.

Troubleshooting

Solutions for common issues: GitHub 401 errors, Lean tracing failures, missing CUDA libraries, and Pantograph errors.

Build docs developers (and LLMs) love

Get started for freeTalk to us