A Machine-to-Machine Interaction System for Lean 4.
- Install
uv - Install
elan: See Lean Manual
- Add the package to your project:
uv add git+https://github.com/stanford-centaur/PyPantograph
uv sync- Clone this repository with submodules:
git clone --recurse-submodules <repo-path>- Execute
cd <repo-path>
uv build- Built wheels can be found at
dist/*.whl
Build the documentations by
uvx --with notebook jupyter-book build docsThen serve
cd docs/_build/html
python3 -m http.server -d .For API interaction examples, see examples/README.md.
@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},
}