From b83f1d66a8a12169354d74f7bf37ddaefa9e784b Mon Sep 17 00:00:00 2001
From: Peiyang Song <p_song@ucsb.edu>
Date: Sun, 21 Apr 2024 22:29:56 -0700
Subject: [PATCH] Update README.md

Include the link to full paper on Arxiv.
---
 README.md | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/README.md b/README.md
index daee312..904d917 100644
--- a/README.md
+++ b/README.md
@@ -184,14 +184,13 @@ theorem mul_left_comm : ∀ a b c : G, a * (b * c) = b * (a * c)
 
 ## Citation
 
-Below is our workshop paper describing an earlier version of Lean Copilot. We plan to release the full paper in early 2024. Stay tuned!
+If you find our work useful, please consider citing our paper:
 
 ```BibTeX
-@inproceedings{song2023towards,
+@article{song2024towards,
   title={Towards Large Language Models as Copilots for Theorem Proving in {Lean}},
-  author={Song, Peiyang and Yang, Kaiyu and Anandkumar, Anima},
-  comment={The last two authors advised equally.},
-  booktitle={The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS'23},
-  year={2023}
+  author={Peiyang Song and Kaiyu Yang and Anima Anandkumar},
+  year={2024},
+  journal = {arXiv preprint arXiv: Arxiv-2404.12534}
 }
 ```