LeanDojo v2 Agents: HFAgent, LeanAgent & ExternalAgent

Agents are the top-level orchestrators in LeanDojo v2. Each agent manages the full lifecycle of a theorem-proving experiment: cloning and tracing a Lean repository, training a model on the resulting tactic data, and then driving a prover to close sorry goals. All three concrete agents — HFAgent, LeanAgent, and ExternalAgent — inherit from the abstract BaseAgent class, which supplies the shared machinery for repository management and the proof loop. You choose an agent based on the kind of model you want to use: a locally fine-tuned HuggingFace checkpoint, a RAG-based retrieval model, or a large hosted model accessed over an API.

Agent Hierarchy

BaseAgent defines the interface that every agent must satisfy. It owns a DynamicDatabase, a list of registered LeanGitRepo objects, and a shared data_path for merged training artifacts. The two abstract methods every subclass must implement are:

_get_build_deps() -> bool — controls whether the Lean tracing step resolves the repository’s external dependencies. Set True for retrieval-based workflows (so premises from dependencies appear in the corpus), False otherwise.
_setup_prover() — instantiates self.prover with whatever backend the agent uses.

Agent–Trainer–Prover Pairing

Agent	Trainer	Prover	Builds Deps
`HFAgent`	`SFTTrainer` or `GRPOTrainer`	`HFProver`	`False`
`LeanAgent`	`RetrievalTrainer`	`RetrievalProver`	`True`
`ExternalAgent`	(none)	`ExternalProver`	`False`

Choosing an Agent

HFAgent
LeanAgent
ExternalAgent

Use HFAgent when you want to fine-tune a HuggingFace causal language model on your own traced Lean repository and then use that checkpoint for proof search. It is the right choice when you have a GPU available for local training and inference, and you want full control over the model, LoRA adapters, and hyperparameters.HFAgent calls _get_build_deps() → False, so dependency premises are not added to the training corpus. The prover is initialised from the same output_dir used by the trainer.Constructor

HFAgent(
    trainer: SFTTrainer,           # required – SFTTrainer or GRPOTrainer
    database_path: str = "dynamic_database.json",
    training_config: Optional[TrainingConfig] = None,
    prover_config: Optional[ProverConfig] = None,
)

Full example (examples/sft.py)

from lean_dojo_v2.agent.hf_agent import HFAgent
from lean_dojo_v2.trainer.sft_trainer import SFTTrainer

def main() -> None:
    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()

if __name__ == "__main__":
    main()

Pass a peft.LoraConfig to SFTTrainer (or GRPOTrainer) if you need parameter-efficient fine-tuning. HFAgent automatically detects the lora_config attribute and passes use_lora=True to HFProver.

Use LeanAgent for the full lifelong-learning pipeline. It trains a dense premise retriever (RetrievalTrainer) and pairs it with a RetrievalAugmentedGenerator (RetrievalProver) for RAG-based tactic generation. Because the retriever needs to index premises from a repo’s dependencies, LeanAgent sets _get_build_deps() → True.LeanAgent accepts multiple repositories and processes them in difficulty-sorted curriculum order.Constructor

LeanAgent(
    database_path: str = "dynamic_database.json",
    training_config: Optional[TrainingConfig] = None,
    prover_config: Optional[ProverConfig] = None,
)

The TrainingConfig and ProverConfig objects control all training hyperparameters and prover settings respectively. If omitted, sensible defaults are applied.Full example (examples/lean_agent.py)

from lean_dojo_v2.agent.lean_agent import LeanAgent

def main() -> None:
    url1 = "https://github.com/durant42040/lean4-example"
    commit1 = "b14fef0ceca29a65bc3122bf730406b33c7effe5"

    url2 = "https://github.com/leanprover/lean4"
    commit2 = "995161396a25153797460473262555e1792f4823"

    agent = LeanAgent()
    agent.setup_github_repository(url=url1, commit=commit1)
    agent.setup_github_repository(url=url2, commit=commit2)

    agent.train()
    agent.prove()

if __name__ == "__main__":
    main()

Because _get_build_deps() is True, tracing is significantly slower and more disk-intensive than with HFAgent. Ensure you have adequate space in your raid/ working directory before registering large repositories.

Use ExternalAgent when you want to attempt proofs immediately without any local training. It delegates all inference to the HuggingFace Inference API (or compatible endpoint), defaulting to deepseek-ai/DeepSeek-Prover-V2-671B:novita. There is no trainer — the agent goes straight from repository setup to proof search.This is the fastest path to running experiments: no GPU, no fine-tuning, no checkpoint management.Constructor

ExternalAgent(
    model_name: str = "deepseek-ai/DeepSeek-Prover-V2-671B:novita",
)

Full example

from lean_dojo_v2.agent.external_agent import ExternalAgent

def main() -> None:
    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=url, commit=commit)
    agent.prove()

if __name__ == "__main__":
    main()

ExternalAgent supports whole-proof generation — pass whole_proof=True to prove() to generate complete proofs in a single forward pass rather than running the step-by-step DFS search loop.

Common Methods

All three agents expose the same public interface defined by BaseAgent.

`setup_github_repository(url, commit)`

Clones the GitHub repository at the given URL and commit, traces it with Lean instrumentation, and registers it in the internal DynamicDatabase. The build_deps flag forwarded to the tracer is determined by _get_build_deps().

agent.setup_github_repository(
    url="https://github.com/durant42040/lean4-example",
    commit="b14fef0ceca29a65bc3122bf730406b33c7effe5",
)

Raises ValueError if tracing fails.

`setup_local_repository(path)`

Uses a local Lean project directory. The method calls LeanGitRepo.from_path(path) to extract the URL and commit from the project’s git history, then traces and registers the repo exactly like setup_github_repository.

agent.setup_local_repository("/path/to/my-lean4-project")

`train()`

Sorts all registered repositories by difficulty (via database.sort_repositories_by_difficulty()) and calls the agent’s trainer with the sorted list. Raises ValueError if no repository has been registered.

agent.train()

`prove(whole_proof=False)`

Collects all unproved sorry theorems across every registered repository, then calls prove_theorem() for each one. Pass whole_proof=True to generate complete proofs in a single forward pass instead of running the DFS search.

agent.prove()              # proof search (default)
agent.prove(whole_proof=True)  # whole-proof generation

`prove_theorem(theorem, repo, whole_proof=False)`

Proves a single theorem. In proof-search mode, the method spins up a pantograph.Server pointing at the traced repository, then calls prover.search(server=server, theorem=theorem, verbose=False). In whole-proof mode, it calls prover.generate_whole_proof(theorem) and prints the result.

result_success = agent.prove_theorem(theorem, repo, whole_proof=False)

In proof-search mode, returns True on success or False if no proof was found, and prints the sequence of used tactics when a proof is found. In whole-proof mode, prints the generated proof and returns None.

Building a Custom Agent

Subclass BaseAgent and implement the two abstract methods to wire up any trainer/prover combination you like.

from lean_dojo_v2.agent.base_agent import BaseAgent
from lean_dojo_v2.prover import HFProver
from lean_dojo_v2.trainer.grpo_trainer import GRPOTrainer


class MyCustomAgent(BaseAgent):
    def __init__(self, trainer: GRPOTrainer):
        super().__init__()
        self.trainer = trainer
        self.output_dir = trainer.output_dir

    def _get_build_deps(self) -> bool:
        # Return True to include dependency premises in the corpus
        return False

    def _setup_prover(self):
        self.prover = HFProver(
            ckpt_path=self.output_dir,
            use_lora=self.trainer.lora_config is not None,
        )

Trainers

Learn how to configure SFTTrainer, GRPOTrainer, RetrievalTrainer, and ProgressTrainer for different training objectives.

Provers

Explore the three prover backends and understand proof search vs whole-proof generation strategies.

Get Started

Concepts

Guides

Reference

LeanDojo v2 Agents: HFAgent, LeanAgent & ExternalAgent

Agent Hierarchy

Agent–Trainer–Prover Pairing

Choosing an Agent

Common Methods

`setup_github_repository(url, commit)`

`setup_local_repository(path)`

`train()`

`prove(whole_proof=False)`

`prove_theorem(theorem, repo, whole_proof=False)`

Building a Custom Agent

Trainers

Provers

Build docs developers (and LLMs) love

Get Started

Concepts

Guides

Reference

Documentation Index

​Agent Hierarchy

​Agent–Trainer–Prover Pairing

​Choosing an Agent

​Common Methods

​setup_github_repository(url, commit)

​setup_local_repository(path)

​train()

​prove(whole_proof=False)

​prove_theorem(theorem, repo, whole_proof=False)

​Building a Custom Agent

Trainers

Provers

Build docs developers (and LLMs) love

Agent Hierarchy

Agent–Trainer–Prover Pairing

Choosing an Agent

Common Methods

`setup_github_repository(url, commit)`

`setup_local_repository(path)`

`train()`

`prove(whole_proof=False)`

`prove_theorem(theorem, repo, whole_proof=False)`

Building a Custom Agent