From bba6bd63ce3b583109c60f026be8708b4a303288 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 22 Oct 2024 22:24:05 -0700 Subject: [PATCH] doc: Paper link --- README.md | 14 +++++++++----- docs/intro.md | 16 ++++++++++++++++ 2 files changed, 25 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 89e25bf..cad254e 100644 --- a/README.md +++ b/README.md @@ -44,12 +44,16 @@ The experiments should be run in `poetry shell`. The environment variable ## Referencing +[Paper Link](https://arxiv.org/abs/2410.16429) + ```bib @misc{pantograph, - title = "Pantograph, A Machine-to-Machine Interface for Lean 4", - author = {Aniva, Leni and Miranda, Brando and Sun, Chuyue}, - year = 2024, - howpublished = {\url{https://github.com/lenianiva/PyPantograph}} + 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}, } ``` - diff --git a/docs/intro.md b/docs/intro.md index 107c532..9d31f1c 100644 --- a/docs/intro.md +++ b/docs/intro.md @@ -23,3 +23,19 @@ LeanDojo has architectural limitations that prevent it from gaining new features such as drafting without refactoring. 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}, +} +```