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

arXiv: https://arxiv.org/abs/2410.16429 · HTML: https://mlsanity.com/paper/2410.16429/

## Key facts

- Cited by 18 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 28 references that are in the map.
- First posted on arXiv 21 Oct 2024.

## Builds on (most cited first, 10 of 10)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [Learning to Prove Theorems by Learning to Generate Theorems](https://mlsanity.com/paper/2002.07019/) (2020)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Graph Contrastive Pre-training for Effective Theorem Reasoning](https://mlsanity.com/paper/2108.10821/) (2021)

## Built on by (most cited first, 18 of 18)

- [Advancing Mathematics Research with AI-Driven Formal Proof Search](https://mlsanity.com/paper/2605.22763/) (2026)
- [LeanExplore: A search engine for Lean 4 declarations](https://mlsanity.com/paper/2506.11085/) (2025)
- [Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models](https://mlsanity.com/paper/2506.11487/) (2025)
- [Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving](https://mlsanity.com/paper/2507.02726/) (2025)
- [RLMEval: Evaluating Research-Level Neural Theorem Proving](https://mlsanity.com/paper/2510.25427/) (2025)
- [AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities](https://mlsanity.com/paper/2606.26442/) (2026)
- [LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4](https://mlsanity.com/paper/2507.14722/) (2025)
- [Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving](https://mlsanity.com/paper/2505.04528/) (2025)
- [ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving](https://mlsanity.com/paper/2502.04671/) (2025)
- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers](https://mlsanity.com/paper/2607.19407/) (2026)
- [Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4](https://mlsanity.com/paper/2602.18767/) (2026)
- [Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4](https://mlsanity.com/paper/2605.25556/) (2026)
- [Automating Formal Verification with Agent-Guided Tree Search](https://mlsanity.com/paper/2605.27485/) (2026)
- [Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean](https://mlsanity.com/paper/2609.39544/) (2026)
- [FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification](https://mlsanity.com/paper/2610.00885/) (2026)
- [NanoProof: Open and Efficient Automated Theorem Proving in Lean 4](https://mlsanity.com/paper/2610.11605/) (2026)
- [Do Theorem Provers Need Theorem-Proving Agents? mini-Lean-agent: A Coding-Agent Baseline for Lean](https://mlsanity.com/paper/2610.17331/) (2026)

## Abstract (arXiv)

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.