diff --git a/index.html b/index.html
index 29867f9..151b7bd 100644
--- a/index.html
+++ b/index.html
@@ -285,7 +285,7 @@ <h2 class="title is-3">Abstract</h2>
                         data, models, and benchmarks. LeanDojo extracts data from Lean and enables interaction with the proof environment programmatically. 
                         It contains fine-grained annotations of premises in proofs, providing valuable data for <em>premise selection</em>&mdash;
                         a key bottleneck in theorem proving. Using this data, we develop <em>ReProver</em> (<u>Re</u>trieval-Augmented <u>Prover</u>): 
-                        the first LLM-based prover that is augmented with retrieval for selecting premises from a vast math library. 
+                        an LLM-based prover that is augmented with retrieval for selecting premises from a vast math library. 
                         It is inexpensive and needs only one GPU week of training. Our retriever leverages LeanDojo's program analysis 
                         capability to identify accessible premises and hard negative examples, which makes retrieval much more effective. 
                         Furthermore, we construct a new benchmark consisting of 98,641 theorems and proofs extracted from Lean's math library.