PyPantograph: Machine-to-Machine Interaction System for Lean 4

Pantograph is a machine-to-machine interaction interface designed for Lean 4. Its primary purpose is to facilitate the training and evaluation of theorem proving agents.

Key features include:

• Writing proofs using a mix of expression and tactic styles.
• Exposing minimal information to search agents to optimize search efficiency.
• Managing metavariable coupling.
• Reading and adding symbols from the environment.
• Extracting tactic training data.
• Drafting incomplete proofs.

PyPantograph is a Machine-to-Machine Interaction System designed for Lean 4. It provides several capabilities for programmatic interaction with Lean files:

• Programmatic Tactic Execution: Use goal_tactic to execute tactics.
• Metavariable Handling: Manages metavariable coupling.
• Conformity Checking: Use check_track to perform whole-file specification conformity checks.
• Data Extraction: Extract tactic invocation data.
• Lean Inspection: Inspect Lean constants.

Pantograph does not strictly mimic Lean LSP behavior to allow for more flexible tree search. Developers should be aware of these specific differences in error handling:

• Synthesis Errors: When Lean LSP reports "don't know how to synthesize placeholder", Pantograph treats this as a non-halting event. Instead of stopping, it turns the placeholder into a goal to allow the proof process to continue.
• Unresolved Goals: When Lean LSP reports "unresolved goals" (indicating a proof cannot finish at the end of a by block), Pantograph will raise an error. This is used to signal the termination of a specific proof search branch.

To build the project documentation using jupyter-book and serve it locally:

1. Build the documentation:

   uv run --group dev jupyter-book build doc

2. Serve the built HTML files:

   python3 -m http.server -d doc/_build/html

PyPantograph requires uv and elan (the Lean toolchain manager) to be installed on your system. Follow the Lean Manual for elan setup.

Install as a project dependency

To add PyPantograph to an existing project using uv:

uv add git+https://github.com/stanford-centaur/PyPantograph
uv sync

Build wheels from source

If you need to build the package from source:

1. Clone the repository including submodules:

   git clone --recurse-submodules <repo-path>

2. Build using uv:

   cd <repo-path>
   uv build

3. The resulting wheels will be located in dist/*.whl.

To execute the project's unit tests, use pytest via uv:

uv run pytest

Before running the examples, you must build the Lean project to generate the necessary compiled .olean files. Navigate into the Example directory and use lake build.

Important Requirements:

• If you modify any Lean files, you must re-run lake build.
• The Lean version used in the Example folder (including dependencies in lakefile.lean and lean-toolchain) must match exactly with the version used in the src/ directory of the main project.

pushd Example
lake build
popd

To use non-builtin Lean libraries (e.g., Aesop or Mathlib4), you must provide a list of module names via the imports parameter.

Important: You cannot import new modules after the server has already started; doing so will trigger initializer exceptions.

If you are using a specific Lean project (like Mathlib4), you must:

1. Create/set up the Lean repository using lake.
2. Run lake build in that repository to build all files.
3. Initialize the Server with the project_path pointing to that repository.

# Example with specific imports
server = Server(imports=["Mathlib"])

# Example with a specific Lean project path
server = Server(project_path="./path-to-lean-repo/")

To set up PyPantograph for development, you need to install uv, clone the repository with submodules, and install the Lean environment (elan and lake).

1. Install uv.
2. Clone the repository with submodules:

   git clone --recurse-submodules <repo-path>

3. Install elan and lake following the Lean Manual.
4. Synchronize the environment:

   cd <repo-path>
   uv sync

You can build a wheel using uv build, which will be placed in the dist directory. You can then install this wheel in downstream projects via pyproject.toml.

The site argument in goal_tactic_async determines the 'area of effect' for a tactic—specifically, which goals the tactic can see or interact with.

• Site(goal_id=N): Targets a specific goal by its ID.
• auto_resume: A boolean field in Site.
  • If True (default), Pantograph does not hide other goals.
  • If False, other goals are set to a 'dormant' state. Dormant goals are hidden from the tactic but must be explicitly reactivated later using goal_resume.

from pantograph.expr import Site

# Target a specific goal (e.g., goal index 1)
site_specific = Site(goal_id=1)
state2 = await server.goal_tactic_async(state, "apply Or.inl", site=site_specific)

# Target a goal and make all other goals dormant
site_dormant = Site(goal_id=0, auto_resume=False)
state3 = await server.goal_tactic_async(state, "exact h", site=site_dormant)

The pantograph.search module provides two distinct search paradigms:

1. Standard Search (Agent.search):

   • Uses a stack-based approach (search_stack).
   • It follows a depth-first-like pattern where it picks the highest priority unsolved goal via next_goal_id and attempts tactics.
   • If a tactic fails (TacticFailure), it records feedback and tries the next.
   • If no tactics are left for a state, it pops the state and continues.

2. MCTS Search (MCTSAgent.search):

   • Uses a tree-based approach.
   • It uses select(state) to find a trajectory through the search tree.
   • It uses estimate(state) to initialize new nodes.
   • It uses backup(states, value) to propagate values from leaf nodes back up to the root, updating total_value and visit_count for all nodes in the trajectory.

PyPantograph uses several core data structures to represent the state of a Lean formal proof.

• Expr: A type alias for str, representing Lean expressions.
• Variable: Represents a variable within a goal, containing its type (t), an optional value (v), and an optional name.
• Goal: Represents a proof goal. It includes an id, a list of variables, a target expression, an optional name, and a mode (TacticMode).
• GoalState: Represents the complete state of a proof session, containing a state_id, a list of active goals, and a list of messages.