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.

HFAgent is the go-to agent when you have local GPU resources and want end-to-end control over the training process. It wraps an SFTTrainer to fine-tune any HuggingFace causal language model on your traced Lean repositories, automatically detects whether LoRA adapters are in use, and then loads the resulting checkpoint into an HFProver for tactic-by-tactic or whole-proof theorem proving — all through the unified BaseAgent interface.

​
Class Definition

lean_dojo_v2.agent.hf_agent.HFAgent(BaseAgent)
HFAgent extends BaseAgent. It does not build Lean dependencies during tracing (_get_build_deps() returns False), and it initialises an HFProver from the SFTTrainer’s output directory when prove() is called.

​
Constructor

HFAgent(
    trainer: SFTTrainer,
    database_path: str = "dynamic_database.json",
    training_config: Optional[TrainingConfig] = None,
    prover_config: Optional[ProverConfig] = None,
)
​
trainer
SFTTrainer
required
A configured lean_dojo_v2.trainer.SFTTrainer instance. The agent reads trainer.output_dir to know where to find the fine-tuned checkpoint, and checks trainer.lora_config to decide whether to load LoRA weights.
​
database_path
str
default:"dynamic_database.json"
Path to the JSON file used for DynamicDatabase persistence. Shared with the base class.
​
training_config
Optional[TrainingConfig]
default:"TrainingConfig()"
Training hyperparameters such as learning rate, batch size, and EWC lambda. Defaults to a TrainingConfig with sensible out-of-the-box values. Pass a customised instance to override individual fields.
​
prover_config
Optional[ProverConfig]
default:"ProverConfig()"
Prover runtime settings including timeout, num_sampled_tactics, num_workers, and use_vllm. Defaults to a ProverConfig with sensible out-of-the-box values.

​
Behaviour

MethodDetail
_get_build_deps()Always returns False. Lean dependency trees are not traced, keeping setup fast.
_setup_prover()Constructs HFProver(ckpt_path=self.output_dir, use_lora=self.use_lora).
use_loraSet to True automatically when trainer.lora_config is not None.
self.output_dir is taken directly from trainer.output_dir, so the checkpoint path used during proving always matches the directory written by the trainer. No manual path wiring is required.

​
Example

​
Full-parameter SFT

The following example is adapted from examples/sft.py. It fine-tunes DeepSeek-Prover-V2-7B with full-parameter SFT on a sample Lean 4 repository and then runs the prover on all sorry theorems: 
from lean_dojo_v2.agent.hf_agent import HFAgent
from lean_dojo_v2.trainer.sft_trainer import SFTTrainer

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="https://github.com/durant42040/lean4-example",
    commit="b14fef0ceca29a65bc3122bf730406b33c7effe5",
)
agent.train()
agent.prove()

​
SFT with LoRA

The following example is adapted from examples/lora.py. It fine-tunes DeepSeek-Prover-V2-7B with LoRA adapters, which reduces GPU memory requirements significantly: 
from peft import LoraConfig

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

lora_config = LoraConfig(
    r=16,
    lora_alpha=32,
    target_modules=["q_proj", "v_proj", "k_proj", "o_proj"],
    lora_dropout=0.1,
)

trainer = SFTTrainer(
    model_name="deepseek-ai/DeepSeek-Prover-V2-7B",
    output_dir="outputs-deepseek-lora",
    epochs_per_repo=5,
    batch_size=2,
    lr=2e-5,
    lora_config=lora_config,
)

agent = HFAgent(trainer=trainer)
agent.setup_github_repository(
    url="https://github.com/durant42040/lean4-example",
    commit="b14fef0ceca29a65bc3122bf730406b33c7effe5",
)
agent.train()
agent.prove()
Omit lora_config from SFTTrainer to perform full-parameter fine-tuning. HFAgent will detect that trainer.lora_config is None and load the checkpoint without LoRA when constructing the prover.

​
Whole-proof generation

Pass whole_proof=True to prove() to ask the model to emit a complete proof block in one forward pass rather than searching tactic-by-tactic: 
agent.prove(whole_proof=True)
Whole-proof generation bypasses the Pantograph proof-state verifier used during tactic search. Generated proofs are printed but not formally verified within LeanDojo v2. Verify them in your Lean environment before accepting them.

​
Multiple Repositories

HFAgent supports progressive training over several repositories. Repositories are sorted by difficulty before training, and the same SFTTrainer checkpoint directory is reused across repos: 
agent = HFAgent(trainer=trainer)

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

agent.train()   # trains on both repos, easiest first
agent.prove()   # proves sorry theorems across both repos

Build docs developers (and LLMs) love

Get started for freeTalk to us