“Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4” by Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. In Proceedings of the 31^st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '25), (Arie Gurfinkel and Marijn Heule, eds.), May 2025, pp. 104-123. Hamilton, Ontario, Canada.
Machine-assisted theorem proving refers to the process of conducting structured reasoning to automatically generate proofs for mathematical theorems. Recently, there has been a surge of interest in using machine learning models in conjunction with proof assistants to perform this task. In this paper, we introduce Pantograph, a tool that provides a versatile interface to the Lean 4 proof assistant and enables efficient proof search via powerful search algorithms such as Monte Carlo Tree Search. In addition, Pantograph enables high-level reasoning by enabling a more robust handling of Lean 4's inference steps. We provide an overview of Pantograph's architecture and features. We also report on an illustrative use case: using machine learning models and proof sketches to prove Lean 4 theorems. Pantograph's innovative features pave the way for more advanced machine learning models to perform complex proof searches and high-level reasoning, equipping future researchers to design more versatile and powerful theorem provers.
BibTeX entry:
@inproceedings{ASM+25,
author = {Leni Aniva and Chuyue Sun and Brando Miranda and Clark
Barrett and Sanmi Koyejo},
editor = {Arie Gurfinkel and Marijn Heule},
title = {Pantograph: {A} Machine-to-Machine Interaction Interface for
Advanced Theorem Proving, High Level Reasoning, and Data
Extraction in Lean 4},
booktitle = {Proceedings of the {\it 31^{st}} International Conference
on Tools and Algorithms for the Construction and Analysis of
Systems (TACAS '25)},
series = {Lecture Notes in Computer Science},
volume = {15696},
pages = {104--123},
publisher = {Springer},
month = may,
year = {2025},
doi = {10.1007/978-3-031-90643-5_6},
note = {Hamilton, Ontario, Canada},
url = {http://theory.stanford.edu/~barrett/pubs/ASM+25.pdf}
}
(This webpage was created with bibtex2web.)