Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
This work addresses the problem of automating complex mathematical reasoning for researchers in theorem proving and AI, though it appears incremental as it builds on existing proof assistant frameworks.
The paper tackles the challenge of machine-assisted theorem proving by introducing Pantograph, a tool that interfaces with the Lean 4 proof assistant to enable efficient proof search using algorithms like Monte Carlo Tree Search and robust handling of inference steps, resulting in capabilities for high-level reasoning and data extraction.
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.