Pantograph: A Machine-to-Machine Interaction Interface for Advanced
  Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
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.
671c206eaadccdbd12a7e607
Leni Aniva
671c206eaadccdbd12a7e608
Chuyue Sun
671c206eaadccdbd12a7e609
Brando Miranda
claimed_verified
2024-10-28T10:37:12.902Z
60ec6453046c81764c7e06f0
https://cdn-avatars.huggingface.co/v1/production/uploads/60ec6453046c81764c7e06f0/gnKlFE5bkpvbDQNb2jrnV.png
Brando Miranda
user
brando
671c206eaadccdbd12a7e60a
Clark Barrett
671c206eaadccdbd12a7e60b
Sanmi Koyejo
Pantograph: A Machine-to-Machine Interaction Interface for Advanced
  Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
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.
Pantograph, a tool interfacing with Lean 4, leverages machine learning models and advanced search algorithms to enhance automatic theorem proving.
machine-assisted theorem proving proof assistants Monte Carlo Tree Search inference steps theorem provers