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

TL;DR

Pantograph delivers a machine-facing interface for Lean 4 that enables training and evaluation of theorem-proving agents by leveraging Monte Carlo Tree Search and explicit metavariable handling. It unifies expression-based and tactic-based proofs, supports incremental feedback, and provides data extraction for training, including draft-sketch-prove workflows. The work demonstrates a Lean 4–native DSP implementation on MiniF2F and discusses architectural and data-generation capabilities to support future hybrid AI–formal reasoning. Overall, Pantograph paves the way for more robust, ML-assisted theorem proving by offering rich proof-state observability, draft-oriented workflows, and formal verification checkpoints for generated proofs.

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.

Figures (7)

• Figure 1: A proof tree for Expression \ref{['eqn:Or commutativity']}
• Figure 2: System architecture of Pantograph. A solid arrow indicates that the component at the arrow source calls functions in the component that is the arrow's target. A human operator interacts with Lean 4's kernel via the IDE, but a machine learning agent can interact via one of Pantograph's interfaces.
• Figure 3: Call hierarchy in Pantograph during the execution of a normal tactic. The text on the right indicates the Lean 4 monad each function runs in.
• Figure 4: $\textcolor{Purple}{?2}$ becomes dormant after a tactic is applied to $\textcolor{Purple}{?1}$. It must be brought back into scope with before the proof can finish. The ellipses ($\ldots$) are plalceholders for some combination of tactics which eventually solves the descendant of $\textcolor{Purple}{?1}$.
• Figure 5: In this diagram, rectangular boxes are proof states, and circles are goals. Each proof state has 0 or more goals. A state with no goals is considered solved. If all descendant goals of a state become solved, the state itself becomes solved.