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.

ExternalProver lets you run LeanDojo v2 proof search against arbitrarily large language models without needing local GPU resources. Rather than loading weights locally, it forwards every tactic and whole-proof request to the HuggingFace Inference API through the HFTacticGenerator client. Out of the box it targets deepseek-ai/DeepSeek-Prover-V2-671B:novita — a 671-billion-parameter model purpose-built for Lean 4 theorem proving — but any HF Inference API-hosted model can be substituted.

​
Class

lean_dojo_v2.prover.external_prover.ExternalProver(BaseProver)
Exported from lean_dojo_v2.prover. Internally instantiates lean_dojo_v2.external_api.python.external_models.HFTacticGenerator and delegates both next_tactic and generate_whole_proof to it.

​
Constructor

ExternalProver(
    model_name: str = "deepseek-ai/DeepSeek-Prover-V2-671B:novita",
)
Constructs an HFTacticGenerator for the specified model. No model weights are downloaded — all inference happens remotely.
​
model_name
str
default:"\"deepseek-ai/DeepSeek-Prover-V2-671B:novita\""
The HuggingFace Inference API model identifier. The format is "<org>/<model-id>" or "<org>/<model-id>:<provider>". The :novita suffix selects the Novita inference provider for this model. Other provider suffixes may also be available on HuggingFace.
The :novita suffix is a HuggingFace Inference API provider selector. If you omit it, HuggingFace will route to its default provider for the model. Other providers (e.g. :together, :fireworks) may offer different throughput and pricing for the same model weights.

​
Authentication

The HuggingFace Inference API requires a valid access token for most models, including DeepSeek-Prover-V2-671B. Set the HF_TOKEN environment variable before running: 
export HF_TOKEN="hf_your_token_here"
Inference via the external API incurs usage costs charged to your HuggingFace account or the selected provider. Whole-proof generation with 671B-parameter models can be slow (tens of seconds per call) and expensive at high request volumes. Monitor your usage on the HuggingFace billing dashboard.

​
Methods

​
next_tactic

def next_tactic(state: GoalState, goal_id: int) -> Optional[Tactic]
Generates the next tactic for proof search by forwarding the goal state string to HFTacticGenerator.generate().
​
state
GoalState
required
The Pantograph GoalState at the current DFS node. Converted to a string via str(state) and sent to the API.
​
goal_id
int
required
Index of the active goal within state.goals. Passed through for interface compatibility; the external generator operates on the full state string.
​
tactic
Optional[Tactic]
A tactic string returned by the API, or None if the API call fails or produces no output.

​
generate_whole_proof

def generate_whole_proof(theorem: Theorem) -> str
Generates a complete Lean 4 proof for theorem by forwarding its string representation to HFTacticGenerator.generate_whole_proof().
​
theorem
Theorem
required
A Theorem object. Its __str__ representation (theorem_statement) is forwarded to the Inference API. You may also pass a plain theorem statement string since str() of a string returns itself, as in the example below.
​
proof
str
The complete proof string returned by the model. Format varies by model; typically a Lean 4 tactic block body.

​
Example: Whole-Proof Generation

The following example is adapted from examples/theorem_proving/generate_whole_proof.py: 
from lean_dojo_v2.prover import ExternalProver

theorem = "theorem my_and_comm : ∀ {p q : Prop}, And p q → And q p := by"
prover = ExternalProver()
proof = prover.generate_whole_proof(theorem)

print(proof)

​
Example: Proof Search via API

ExternalProver is a full BaseProver subclass and supports search() just like HFProver: 
from pantograph.server import Server
from lean_dojo_v2.prover import ExternalProver

prover = ExternalProver()  # uses default DeepSeek-Prover-V2-671B

server = Server(imports=["Init"], project_path="/path/to/traced/repo")

result, tactics = prover.search(
    server=server,
    goal="⊢ ∀ (n : Nat), 0 + n = n",
    verbose=True,
)

if result.success:
    print(f"Proved in {result.steps} steps:")
    for tactic in tactics:
        print(" ", tactic)
else:
    print("Search exhausted without finding a proof.")

​
See Also

Build docs developers (and LLMs) love

Get started for freeTalk to us