title: Pantograph: A Machine-to-Machine Interaction Interface for Advanced
    Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
summary: 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.
paper_authors._id: 671c206eaadccdbd12a7e607
paper_authors.name: Leni Aniva
paper_authors._id: 671c206eaadccdbd12a7e608
paper_authors.name: Chuyue Sun
paper_authors._id: 671c206eaadccdbd12a7e609
paper_authors.name: Brando Miranda
paper_authors.status: claimed_verified
paper_authors.statusLastChangedAt: 2024-10-28T10:37:12.902Z
paper_authors._id: 60ec6453046c81764c7e06f0
paper_authors.avatarUrl: https://cdn-avatars.huggingface.co/v1/production/uploads/60ec6453046c81764c7e06f0/gnKlFE5bkpvbDQNb2jrnV.png
paper_authors.fullname: Brando Miranda
paper_authors.type: user
paper_authors.user: brando
paper_authors._id: 671c206eaadccdbd12a7e60a
paper_authors.name: Clark Barrett
paper_authors._id: 671c206eaadccdbd12a7e60b
paper_authors.name: Sanmi Koyejo
paper_title: Pantograph: A Machine-to-Machine Interaction Interface for Advanced
    Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
paper_summary: 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.
paper_ai_keywords: Pantograph Monte Carlo Tree Search Lean 4 proof assistant proof sketches inference steps theorem proving machine-assisted theorem proving