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.

HFProver brings locally fine-tuned language models into the LeanDojo v2 proof search pipeline. It loads any HuggingFace causal language model — whether a full checkpoint saved by SFTTrainer or a LoRA adapter saved alongside the base weights — and wraps it in the BaseProver search loop. At each step the prover builds a structured chat prompt from the current goal state, samples five candidate tactics, filters out illegal ones like sorry, and randomly selects a valid candidate to pass back to the search engine.

​
Class

lean_dojo_v2.prover.hf_prover.HFProver(BaseProver)
Exported from lean_dojo_v2.prover.

​
Constructor

HFProver(
    ckpt_path: str,
    use_lora: bool = False,
    device: str = "auto",
)
Loads the tokenizer and model from ckpt_path onto the target device and sets the model to evaluation mode. Construction is blocking — the model is fully loaded before the constructor returns.
​
ckpt_path
str
required
Path to the saved model checkpoint directory. This should be the output directory of a SFTTrainer or GRPOTrainer run and must contain the tokenizer files alongside the model weights.
​
use_lora
bool
default:"false"
When True, loads the checkpoint using peft.AutoPeftModelForCausalLM, which expects adapter files (adapter_config.json, adapter_model.safetensors, etc.) alongside the base model reference. When False, uses transformers.AutoModelForCausalLM for a standard full-weight checkpoint.
​
device
str
default:"\"auto\""
Device placement string. "auto" resolves to cuda if a GPU is available, otherwise falls back to cpu. Any string accepted by torch.device() is valid (e.g. "cuda:1", "mps").
Set use_lora=True when loading LoRA adapters produced by SFTTrainer(lora_config=...). The checkpoint directory must contain the adapter files (adapter_config.json, adapter_model.safetensors). For full fine-tuned checkpoints, leave this at the default False.

​
Methods

​
next_tactic

def next_tactic(state: GoalState, goal_id: int) -> Optional[Tactic]
Generates a single tactic for the given goal during proof search. Called automatically by BaseProver.search() on every DFS step. Prompt format — the goal state is embedded in a three-section chat template: 
### System:
You are a Lean 4 tactic generator. Given a goal state,
output exactly ONE Lean tactic that advances or solves the goal.
Rules:
- Output only the tactic text; no prose, quotes, or code fences.
- Single line only; no `by` blocks.
- Never use `sorry` or `admit`.
### User:
{goal_str}

### Assistant:
Generation parameters — max_new_tokens=64, num_return_sequences=5, temperature=0.7, top_p=0.9. After decoding, each candidate is trimmed to its first line and first <;> clause, and any candidate equal to "sorry" is discarded. One tactic is chosen uniformly at random from the remaining valid candidates.
​
state
GoalState
required
The Pantograph GoalState at the current DFS node. Its string representation is used directly as the {goal_str} in the prompt.
​
goal_id
int
required
Index of the active goal within state.goals that the prover should address.
​
tactic
Optional[Tactic]
A tactic string such as "simp", "exact h", or "omega", or None if the model is not yet initialized (the theorem attribute has not been set by search()).

​
generate_whole_proof

def generate_whole_proof(theorem: Theorem) -> str
Generates a complete Lean 4 proof for theorem in a single inference pass without running the DFS search loop. Prompt format — uses the same ### System / ### User / ### Assistant template as next_tactic, but the user message is the full theorem_statement string and the system instruction asks for a complete proof body. Generation parameters — max_new_tokens=512, num_return_sequences=1, temperature=0.7, top_p=0.9. The <;> combinator is stripped from the output before returning.
​
theorem
Theorem
required
The Theorem object to prove. Its __str__ representation (theorem_statement) is used as the model input.
​
proof
str
The decoded proof body string, with leading/trailing whitespace and <;> combinator tokens removed.
The following example is adapted directly from examples/theorem_proving/generate_tactics.py: 
from pantograph.server import Server
from lean_dojo_v2.prover import HFProver

prover = HFProver(ckpt_path="outputs-deepseek")

server = Server()

result, used_tactics = prover.search(
    server=server,
    goal="∀ {p q : Prop}, p ∧ q → q ∧ p",
    verbose=False,
)

print(result)
if result.success:
    for tactic in used_tactics:
        print(tactic)

​
Example: Whole-Proof Generation

from lean_dojo_v2.prover import HFProver
from lean_dojo_v2.database.models.theorems import Theorem
from pathlib import Path
from lean_dojo_v2.lean_dojo.data_extraction.lean import Pos

prover = HFProver(ckpt_path="outputs-deepseek", use_lora=True)

theorem = Theorem(
    full_name="my_and_comm",
    file_path=Path("MyProject/Basic.lean"),
    start=Pos(1, 0),
    end=Pos(1, 60),
    url="https://github.com/my-org/my-repo",
    commit="abc123",
    theorem_statement="theorem my_and_comm : ∀ {p q : Prop}, And p q → And q p := by",
)

proof = prover.generate_whole_proof(theorem)
print(proof)

​
Notes

next_tactic() returns None if self.theorem has not been set. When calling search(), theorem is set automatically. If you call next_tactic() directly (outside of search()), ensure you set prover.theorem first.
Five candidate sequences are generated on every tactic call. On CPU this can be slow for large models. Consider fine-tuning a smaller model (e.g. DeepSeek-R1-Distill-Qwen-1.5B) for interactive use, or use ExternalProver to offload inference entirely.

​
See Also

Build docs developers (and LLMs) love

Get started for freeTalk to us