Pantograph/docs/intro.md

# Introduction

This is Pantograph, an machine-to-machine interaction interface for Lean 4.
Its main purpose is to train and evaluate theorem proving agents. The main
features are:
1. Interfacing via the Python library, REPL, or C Library
2. A mixture of expression-based and tactic-based proofs
3. Pantograph has been designed with facilitating search in mind. A theorem
   proving agent can simultaneously explore multiple branches of the proof.
4. Handling of metavariable coupling
5. Reading/Adding symbols from the environment
6. Extraction of tactic training data
7. Support for drafting

## Design Rationale

The Lean 4 interface is not conducive to search. Readers familiar with Coq may
know that the Coq Serapi was superseded by CoqLSP. In the opinion of the
authors, this is a mistake. An interface conducive for human operators to write
proofs is often not an interface conductive to search.

Almost all of Pantograph's business logic is written in Lean, and Pantograph
achieves tighter coupling between the data extraction and proof search
components.

## Referencing

[Paper Link](https://arxiv.org/abs/2410.16429)

```bib
@misc{pantograph,
      title={Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4},
      author={Leni Aniva and Chuyue Sun and Brando Miranda and Clark Barrett and Sanmi Koyejo},
      year={2024},
      eprint={2410.16429},
      archivePrefix={arXiv},
      primaryClass={cs.LO},
      url={https://arxiv.org/abs/2410.16429},
}
```