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.

ExternalAgent is the quickest path to theorem proving in LeanDojo v2 when local GPU resources are unavailable, or when you want to benchmark frontier-scale models like DeepSeek-Prover-V2-671B without managing model weights. It skips the training stage entirely — there is no trainer, no fine-tuning loop, and no checkpoint management. Instead, it delegates all inference to the HuggingFace Inference API via an ExternalProver, making it straightforward to swap in any model accessible through that API.

​
Class Definition

lean_dojo_v2.agent.external_agent.ExternalAgent(BaseAgent)
ExternalAgent extends BaseAgent. It does not build Lean dependencies during tracing (_get_build_deps() returns False) and initialises an ExternalProver backed by the specified HuggingFace Inference API model when prove() is called.

​
Constructor

ExternalAgent(
    model_name: str = "deepseek-ai/DeepSeek-Prover-V2-671B:novita",
)
ExternalAgent accepts only a single constructor parameter. It does not expose a database_path argument; the underlying DynamicDatabase is always initialised with its default path.
​
model_name
str
default:"deepseek-ai/DeepSeek-Prover-V2-671B:novita"
The HuggingFace Inference API model identifier. The optional :<provider> suffix selects a specific inference backend — for example, :novita routes requests through the Novita inference provider. Any model accessible via the HF Inference API can be used here.

​
Behaviour

MethodDetail
_get_build_deps()Always returns False. Dependency tracing is skipped to keep setup fast.
_setup_prover()Constructs ExternalProver(model_name=self.model_name).
TrainingNot supported. ExternalAgent has no self.trainer; calling train() will raise an AttributeError.
For gated models, set the HF_TOKEN environment variable to a valid HuggingFace access token before calling prove(). The :novita suffix in the default model name routes requests to the Novita inference provider, which hosts the 671B parameter DeepSeek-Prover-V2 model.

​
Example

The following example is adapted from examples/external_api.py. No training step is required — prove(whole_proof=True) queries the API model directly for each sorry theorem: 
from lean_dojo_v2.agent import ExternalAgent

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

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

agent.prove(whole_proof=True)  # No train() call needed
After setup_github_repository(), the repository is traced and all sorry theorems are extracted from the database. prove() then iterates over each unproved sorry theorem and queries the API model for a proof.

​
Whole-Proof Generation

Call prove(whole_proof=True) to generate a complete proof block in a single model forward pass instead of running tactic-by-tactic best-first search. This is particularly effective with large frontier models that have strong single-shot reasoning capabilities.
agent.prove(whole_proof=True)
When whole_proof=True, prove_theorem() calls self.prover.generate_whole_proof(theorem) and prints the result. Tactic search via a Pantograph Server is bypassed entirely, which reduces API round-trips and is faster for models that can reliably produce complete proofs.

​
Using a Different Model

Swap in any other model available on the HuggingFace Inference API by changing model_name: 
from lean_dojo_v2.agent import ExternalAgent

# Use a smaller model for quick experiments
agent = ExternalAgent(model_name="deepseek-ai/DeepSeek-Prover-V2-7B")
agent.setup_github_repository(
    url="https://github.com/durant42040/lean4-example",
    commit="3e23ab0bfdcfdbd5b11ab53c2cd8b5d16492e9c2",
)
agent.prove()
ExternalAgent does not support train() or evaluate(). If you need to fine-tune the model on your own traced repositories before proving, use HFAgent or LeanAgent instead.

Build docs developers (and LLMs) love

Get started for freeTalk to us