PyPantograph

A Machine-to-Machine Interaction System for Lean 4.

Features:

• Programmatically execute tactics (goal_tactic)
• Handling of metavariable coupling
• Whole file specification conformity check (check_track)
• Extraction of tactic invocation data
• Inspection of Lean constants

Installation

1. Install uv
2. Install elan: See Lean Manual

Install as a project dependency

3. Add the package to your project:

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

Build wheels from source

3. Clone this repository with submodules:

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

4. Execute

cd <repo-path>
uv build

5. Built wheels can be found at dist/*.whl

Documentation

Build the documentations by

uv run --group dev jupyter-book build doc

Then serve

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

Examples

For API interaction examples, see examples/README.md.

Contributing

Execute unit tests with

uv run pytest

Reference

Paper Link

@misc{pantograph,
      title={Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4},
      author={Leni Aniva and Chuyue Sun and Brando Miranda and Clark Barrett and Sanmi Koyejo},
      year={2024},
      eprint={2410.16429},
      archivePrefix={arXiv},
      primaryClass={cs.LO},
      url={https://arxiv.org/abs/2410.16429},
}