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.

BaseProver is the foundation every concrete prover in LeanDojo v2 builds on. It inherits from Pantograph’s Agent and Python’s ABC, providing a complete depth-first search loop, a default goal-prioritization heuristic, and a path-finding utility that extracts the shortest winning tactic chain from the search graph. Subclasses only need to implement two abstract methods — next_tactic() and generate_whole_proof() — while getting the entire search infrastructure for free.

​
Class

lean_dojo_v2.prover.base_prover.BaseProver(Agent, ABC)
Exported from lean_dojo_v2.prover.

​
Constructor

BaseProver()
BaseProver takes no parameters. Subclasses call super().__init__() to initialize the internal theorem state holder used during a search run.

​
Abstract Methods

​
next_tactic

@abstractmethod
def next_tactic(state: GoalState, goal_id: int) -> Optional[Tactic]
Generate the next tactic to attempt for the given goal within a goal state. This is the core decision point of every prover — it is called by search() on every step of the DFS loop.
​
state
GoalState
required
The current Pantograph GoalState object, which contains all open goals at this point in the proof.
​
goal_id
int
required
Zero-based index of the specific goal within state.goals that the prover should target next.
​
tactic
Optional[Tactic]
A Pantograph Tactic string to apply to the goal, or None to signal that the prover has no suggestion and the search should backtrack.

​
generate_whole_proof

@abstractmethod
def generate_whole_proof(theorem: Theorem) -> str
Generate a complete, self-contained proof string for theorem in a single inference call, without running the DFS search loop. This method is used by scripts that want a whole-proof output (e.g., for training data generation) rather than tactic-by-tactic search.
​
theorem
Theorem
required
A lean_dojo_v2.database.models.theorems.Theorem object whose theorem_statement field holds the full theorem … := by declaration.
​
proof
str
A Lean 4 proof string. The exact format depends on the concrete implementation; typically the tactic block body only (no theorem header).
def search(
    server: Server,
    goal: Optional[str] = None,
    theorem: Optional[Theorem] = None,
    verbose: bool = False,
) -> tuple[SearchResult, list[str]]
Runs a depth-first proof search on the given goal or theorem using the Pantograph server. This is the primary entry point for all search-based provers and orchestrates the full DFS loop, the networkx search graph, and tactic bookkeeping.

​
Search algorithm

  1. Resolves the goal string: if theorem is provided, it calls server.env_inspect(theorem.full_name) to retrieve the pretty-printed goal. Otherwise it uses goal directly.
  2. Calls server.goal_start(goal) to obtain the initial GoalState.
  3. Runs a DFS loop for up to 100 steps, attempting up to 5 tactics per goal (max_trials_per_goal=5) before backtracking.
  4. Builds a networkx.DiGraph where nodes are SearchState objects and edges carry the tactic string, goal ID, and step number. Failed tactics are stored as failure-labelled edges so the full search tree is preserved.
  5. On success, calls _find_shortest_path_to_solved() to extract the minimal tactic chain and returns it.

​
Parameters

​
server
Server
required
A running Pantograph Server instance. The server must be in automatic mode (server.is_automatic() == True).
​
goal
Optional[str]
default:"None"
A raw Lean 4 goal string to prove, e.g. "∀ {p q : Prop}, p ∧ q → q ∧ p". Exactly one of goal or theorem must be provided.
​
theorem
Optional[Theorem]
default:"None"
A Theorem object. When provided, the goal string is looked up automatically via server.env_inspect. Exactly one of goal or theorem must be provided.
​
verbose
bool
default:"false"
When True, prints step-by-step progress including the current stack depth, the tactic being attempted, and the goal it targets.

​
Return value

​
result
SearchResult
A Pantograph SearchResult containing success (bool), steps (int), duration (float), and n_goals_root (int).
​
used_tactics
list[str] | None
The ordered list of tactics on the shortest path from the initial state to the solved state. Returns None if the search failed.

​
guidance

def guidance(state: GoalState) -> list[float]
Returns a priority weight for each open goal in state. Higher weights cause the search to tackle that goal earlier in the DFS ordering. Default implementation assigns 1.0 / (len(goal.variables) + 1) to each goal — goals with fewer bound variables are prioritized, as they tend to be simpler to close.
​
state
GoalState
required
The current goal state whose goals should be scored.
​
priorities
list[float]
A list of float weights, one per goal in state.goals, in the same order.
Subclasses may override guidance() to implement custom heuristics such as learned value functions or embedding-based similarity scores.

​
_find_shortest_path_to_solved

def _find_shortest_path_to_solved(
    search_graph: nx.DiGraph,
    solved_node_id: int,
) -> list[tuple[int, str, int]]
Internal utility called automatically by search() when a proof is found. Uses networkx.shortest_path to walk from node 0 (the root) to solved_node_id through the search graph and collect the tactic sequence.
​
search_graph
nx.DiGraph
required
The directed graph built during the search run.
​
solved_node_id
int
required
The node ID of the solved SearchState.
​
path_info
list[tuple[int, str, int]]
A list of (node_id, tactic, goal_id) tuples representing each edge on the shortest path. Returns None if no path exists (logged as a warning).

​
Example

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

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

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)

​
Writing a Custom Prover

Any custom prover must inherit from BaseProver and implement both next_tactic() and generate_whole_proof(). The search loop, graph construction, and path extraction are provided automatically — only the tactic generation logic needs to be supplied.
from typing import Optional
from pantograph.expr import GoalState, Tactic
from lean_dojo_v2.prover.base_prover import BaseProver
from lean_dojo_v2.database.models.theorems import Theorem


class MyProver(BaseProver):
    def next_tactic(self, state: GoalState, goal_id: int) -> Optional[Tactic]:
        # Return a fixed tactic for illustration
        return "simp"

    def generate_whole_proof(self, theorem: Theorem) -> str:
        # Return a trivial proof for illustration
        return "simp"

​
See Also

Build docs developers (and LLMs) love

Get started for freeTalk to us