Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4

TL;DR

Pantograph is a new interface for Lean 4 that enhances machine-assisted theorem proving by integrating advanced search algorithms and enabling high-level reasoning, facilitating more complex proof searches and reasoning tasks.

Contribution

It introduces Pantograph, a versatile tool that improves proof search efficiency and high-level reasoning capabilities in Lean 4 using machine learning and advanced algorithms.

Findings

Pantograph enables efficient proof search with Monte Carlo Tree Search.

It improves handling of Lean 4's inference steps for high-level reasoning.

The tool facilitates proof automation using machine learning models.

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.