--- title: "Pantograph — paper by Aniva et al. (2024) — summary and ideas" description: "To demonstrate the tool, the authors built what they describe as the first Lean 4 implementation of… 5 references, cited by 12 papers here." authors: ["Leni Aniva", "Chuyue Sun", "Brando Miranda", "Clark Barrett", "Sanmi Koyejo"] year: 2024 venue: "arXiv:2410.16429" source: "https://arxiv.org/abs/2410.16429" doi: "10.48550/arxiv.2410.16429" arxiv: "2410.16429" licence: "CC BY 4.0 (arXiv)" licence_url: "https://creativecommons.org/licenses/by/4.0/" summary_licence: "Elamur Cosmic License" canonical: "https://research.elamur.ai/free/en/papers/aniva-2024-pantograph-machine-machine-interaction-interface/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/aniva-2024-pantograph-machine-machine-interaction-interface/) [home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2024](https://md.research.elamur.ai/free/en/papers/2024/page/13/) / Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 # Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 **Authors:** Leni Aniva, [Chuyue Sun](https://md.research.elamur.ai/free/en/authors/chuyue-sun/), [Brando Miranda](https://md.research.elamur.ai/free/en/authors/brando-miranda/), [Clark Barrett](https://md.research.elamur.ai/free/en/authors/clark-barrett/) and [Sanmi Koyejo](https://md.research.elamur.ai/free/en/authors/sanmi-koyejo/) · **Year:** 2024 · **Venue:** [arXiv:2410.16429](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/) ([Lecture notes in computer science 2024](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/2024/)) · **Publisher:** [Springer Science+Business Media](https://md.research.elamur.ai/free/en/publishers/springer-science-business-media/) · **Licence:** [CC BY 4.0 (arXiv)](https://creativecommons.org/licenses/by/4.0/) **Links:** [Publisher's page](https://arxiv.org/abs/2410.16429) · [PDF](https://arxiv.org/pdf/2410.16429v2) · [DOI 10.48550/arxiv.2410.16429](https://doi.org/10.48550/arxiv.2410.16429) · [arXiv 2410.16429](https://arxiv.org/abs/2410.16429) · [OpenAlex](https://openalex.org/W4409974404) **Citations:** 2 citations (OpenAlex, 2026-10-14) · [12](https://md.research.elamur.ai/free/en/papers/aniva-2024-pantograph-machine-machine-interaction-interface/cited-by/) in our library, of the 149,439 papers whose bibliographies we read ## Summary Machine learning agents that search for proofs in Lean 4 depend on an interface to the proof assistant. The standard Language Server Protocol was built for humans: it tracks cursor positions and offers no easy way to collect tactic data or to leave proof gaps for automation. Pantograph is an API and REPL written entirely in Lean 4 and designed for machine users. Agents can work on goals independently, which makes tree search methods such as Monte Carlo Tree Search practical, and the tool handles metavariable coupling between dependent goals. Pantograph also supports high-level tactics, gives step-by-step feedback inside partially executed conv/calc blocks, and can resume drafts that contain `sorry`. It extracts training data such as goal states before and after each tactic, proof scripts with comments, and proofs represented as programs. To demonstrate the tool, the authors built what they describe as the first Lean 4 implementation of draft-sketch-prove (DSP). Without any training, it proved up to 28.4% of MiniF2F test theorems, setting a baseline for future hybrid LLM and formal-reasoning provers. ## Key points - Compared with LeanDojo, Pantograph has no external dependencies such as Docker and interacts faster. It also supports `have`, `let`, `conv` and `calc` incrementally, whereas LeanDojo only allows some of these as monolithic steps or not at all. - The DSP pipeline works in three stages: - An LLM writes an informal proof of the MiniF2F statement. - The same LLM turns it into Lean 4 sketches containing `sorry`. - Pantograph converts the resulting holes into goals, which the hammers aesop, simp and linarith then try to close. - Models were GPT-4o and o1-preview, run with max tokens 2048, top P 0.95 and temperature 0.8. - Success rates on MiniF2F: - GPT-4o with 3 sketches: 23.6% on validation and 28.4% on test. - One sketch: 12.7%/14.7% for GPT-4o and 10.9%/16.0% for o1-preview. - o1-preview averaged about 73–88 s per problem versus roughly 17–36 s for GPT-4o, without a clear accuracy gain. Code is available at github.com/stanford-centaur/PyPantograph. *Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.* ## Institutions - [Stanford University](https://md.research.elamur.ai/free/en/universities/stanford-university/) — University, Stanford, United States · 567 works · 335,189 citations 📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works 🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works ## Cite Cite as: Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett and Sanmi Koyejo. 2024. Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4. arXiv:2410.16429. The paper itself, not this page. BibTeX from the library's record of the work. ```bibtex @misc{aniva2024pantograph, title = {{Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4}}, author = {Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett and Sanmi Koyejo}, year = {2024}, doi = {10.48550/arxiv.2410.16429}, eprint = {2410.16429}, archivePrefix = {arXiv}, url = {https://doi.org/10.48550/arxiv.2410.16429} } ``` - [← previous Open-Endedness is Essential for Artificial Superhuman Intelligence](https://md.research.elamur.ai/free/en/papers/hughes-2024-open-endedness-essential-artificial-superhuman/) - [next → SaudiBERT: A Large Language Model Pretrained on Saudi Dialect Corpora](https://md.research.elamur.ai/free/en/papers/qarah-2024-saudibert-large-language-model-pretrained/) - [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/13/) ## References 5 references, 4 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet. 1. 1. Hello gpt-4o. — [TacticToe: Learning to Prove with Tactics](https://md.research.elamur.ai/free/en/papers/gauthier-2018-tactictoe-learning-prove-tactics/) [https://openai.com/index/hello-gpt-4o/](https://openai.com/index/hello-gpt-4o/) (9 2024) 2. Introducing openai o1-preview. https://openai.com/index/ introducing-openai-o1-preview/ (9 2024) 3. Aya developers: The aya proof assistant. https://www.aya-prover.org (2021) 4. Browne, C.B., Powley, E., Whitehouse, D., Lucas, S.M.,… [↗](https://openai.com/index/hello-gpt-4o/) 2. Cambridge University Press (2017) 8. Jiang, A.e.a.: [Draft, sketch, and prove: Guiding formal theorem provers with informal proofs](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/) (Oct 2022). https://doi.org/10.48550/arXiv.2210.12283, https://arxiv.org/abs/2210.12283v2 9. Jiang, A.Q., Li, W., Tworkowski, S., Czechowski, K., Odrzygóźdź, T., Miłoś,… [↗](https://doi.org/10.48550/arXiv.2210.12283) 3. CPP 2023, Association for Computing Machinery, New York, NY, USA (2023). https://doi.org/10.1145/3573105.3575671, https://doi.org/10.1145/3573105.3575671 14. mathlib: [The lean mathematical library](https://md.research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/). CoRR abs/1910.09336 (2019), http://arxiv.org/abs/1910.09336 15. de Moura, L., Ullrich, S.: The lean… [↗](https://doi.org/10.1145/3573105.3575671) 4. Springer International Publishing, Cham (2021) 16. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic, vol. 2283. [find](https://scholar.google.com/scholar?q=Springer+International+Publishing%2C+Cham+%282021%29+16%2E+Nipkow%2C+T%2E%2C+Paulson%2C+L%2EC%2E%2C+Wenzel%2C+M%2E%3A+Isabelle%2FHOL%3A+a+proof+assistant+for+higher%2Dorder+logic%2C+vol%2E+2283%2E) 5. Springer Science & Business Media (2002) 17. Silver, D., Hubert, T., Schrittwieser, J., Antonoglou, I., Lai, M., Guez, A., Lanctot, M., Sifre, L., Kumaran, D., Graepel, T., Lillicrap, T., Simonyan, K., Hassabis, D.: A general reinforcement learning algorithm that masters chess, shogi, and go through… — [Learning to Prove Theorems by Learning to Generate Theorems](https://md.research.elamur.ai/free/en/papers/wang-2020-learning-prove-theorems-learning-generate/) *Updated 3 November 2026*