~

index.html

@@ -390,9 +390,8 @@ <h2 class="title is-3"><span class="dvima">Experiments</span></h2>
         <div class="rows">
             <div class="rows is-centered ">
                 <div class="row is-full-width">
-                    <h2 class="title is-3"><span class="dvima">Augmenting Existing Proof Repositories</span></h2>
-
-                    We evaluate ReProver on theorems in <a target="_blank" href="https://github.com/facebookresearch/miniF2F">miniF2F</a> and <a target="_blank" href="https://github.com/zhangir-azerbayev/ProofNet">ProofNet</a>. It discovers <a target="_blank" href="https://github.com/facebookresearch/miniF2F/pull/13">33 proofs in miniF2F</a>a> and <a target="_blank" href="https://github.com/zhangir-azerbayev/ProofNet/pull/14">39 proofs in ProofNet</a> that did not have Lean proofs. Our proofs have helped ProofNet uncover bugs in the formalization of theorem statements.
+                    <h2 class="title is-3"><span class="dvima">Discovering New Proofs and Uncovering Bugs for Existing Proof Repositories</span></h2>
+                    <p>We evaluate ReProver on theorems in <a target="_blank" href="https://github.com/facebookresearch/miniF2F">miniF2F</a> and <a target="_blank" href="https://github.com/zhangir-azerbayev/ProofNet">ProofNet</a>. It discovers <a target="_blank" href="https://github.com/facebookresearch/miniF2F/pull/13">33 proofs in miniF2F</a> and <a target="_blank" href="https://github.com/zhangir-azerbayev/ProofNet/pull/14">39 proofs in ProofNet</a> that did not have Lean proofs. Our proofs have helped ProofNet uncover multiple bugs in the formalization of theorem statements.</p>
                 </div>
             </div>
         </div>