Pantograph: A Machine-to-Machine Interaction Interface for Advanced
  Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
Authors: name: Leni Aniva; name: Chuyue Sun; name: Brando Miranda; name: Clark Barrett; name: Sanmi Koyejo
Published: 2024-10-21 18:49:28

Abstract: 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.