update paper info

Author: Kaiyu Yang

README.md

@@ -60,7 +60,7 @@ pip install .
 ## Citation
 
 [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://leandojo.org/)      
-Under review, NeurIPS (Datasets and Benchmarks Track), 2023  
+Neural Information Processing Systems (NeurIPS), 2023  
 [Kaiyu Yang](https://yangky11.github.io/), [Aidan Swope](https://aidanswope.com/about), [Alex Gu](https://minimario.github.io/), [Rahul Chalamala](https://rchalamala.github.io/),  
 [Peiyang Song](https://peiyang-song.github.io/), [Shixing Yu](https://billysx.github.io/), [Saad Godil](https://www.linkedin.com/in/saad-godil-9728353/), [Ryan Prenger](https://www.linkedin.com/in/ryan-prenger-18797ba1/), [Anima Anandkumar](http://tensorlab.cms.caltech.edu/users/anima/)
 

scripts/generate-benchmark-lean3.ipynb

@@ -11,7 +11,7 @@
     "This script uses [LeanDojo](https://leandojo.org/) to construct LeanDojo Benchmark used in our paper:\n",
     "\n",
     "[LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://leandojo.org/)      \n",
-    "Under review at NeurIPS (Datasets and Benchmarks Track), 2023  \n",
+    "NeurIPS 2023 (Datasets and Benchmarks Track)  \n",
     "[Kaiyu Yang](https://yangky11.github.io/), [Aidan Swope](https://aidanswope.com/about), [Alex Gu](https://minimario.github.io/), [Rahul Chalamala](https://rchalamala.github.io/), [Peiyang Song](https://peiyang-song.github.io/), [Shixing Yu](https://billysx.github.io/), [Saad Godil](https://www.linkedin.com/in/saad-godil-9728353/), [Ryan Prenger](https://www.linkedin.com/in/ryan-prenger-18797ba1/), [Anima Anandkumar](http://tensorlab.cms.caltech.edu/users/anima/)\n",
     "\n",
     "The dataset is constructed from [mathlib](https://github.com/leanprover-community/mathlib/tree/32a7e535287f9c73f2e4d2aef306a39190f0b504) (`32a7e535287f9c73f2e4d2aef306a39190f0b504`) and will be saved to `../leandojo_benchmark`. It includes 2000 theorems for validation, 2000 theorems for testing, and the rest for training. Please refer to our paper for details. For most use cases, you shouldn't need to generate the data and can directly use our official LeanDojo Benchmark downloadable [here](https://zenodo.org/record/8242196).\n",

scripts/generate-benchmark-lean4.ipynb

@@ -11,7 +11,7 @@
     "This script uses [LeanDojo](https://leandojo.org/) to construct LeanDojo Benchmark 4 in the appendix of our paper:\n",
     "\n",
     "[LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://leandojo.org/)      \n",
-    "Under review at NeurIPS (Datasets and Benchmarks Track), 2023  \n",
+    "NeurIPS 2023 (Datasets and Benchmarks Track)    \n",
     "[Kaiyu Yang](https://yangky11.github.io/), [Aidan Swope](https://aidanswope.com/about), [Alex Gu](https://minimario.github.io/), [Rahul Chalamala](https://rchalamala.github.io/), [Peiyang Song](https://peiyang-song.github.io/), [Shixing Yu](https://billysx.github.io/), [Saad Godil](https://www.linkedin.com/in/saad-godil-9728353/), [Ryan Prenger](https://www.linkedin.com/in/ryan-prenger-18797ba1/), [Anima Anandkumar](http://tensorlab.cms.caltech.edu/users/anima/)\n",
     "\n",
     "The dataset is constructed from [mathlib4](https://github.com/leanprover-community/mathlib4/tree/355541ae7a2455222f179dcf7f074aa2c45eb8aa) (`355541ae7a2455222f179dcf7f074aa2c45eb8aa`) and will be saved to `../leandojo_benchmark_4`. It includes 2000 theorems for validation, 2000 theorems for testing, and the rest for training. Please refer to our paper for details. For most use cases, you shouldn't need to generate the data and can directly use our official LeanDojo Benchmark 4 downloadable [here](https://zenodo.org/record/8040110).\n",