~

index.html

@@ -392,6 +392,18 @@ <h2 class="title is-3"><span class="dvima">Experiments</span></h2>
                 <div class="row is-full-width">
                     <h2 class="title is-3"><span class="dvima">Discovering New Proofs and Uncovering Formalization Bugs</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> of theorems that did not have Lean proofs. Our proofs have helped ProofNet uncover multiple bugs in the formalization of theorem statements.</p>
+
+                    <img src="images/minif2f.jpg" class="interpolation-image" alt="" style="display: block; margin-left: auto; margin-right: auto"/>
+                    <br />
+                    <span style="font-size: 110%"><b>Example new proofs discovered on miniF2F.</b> </span>
+
+                    <img src="images/proofnet.jpg" class="interpolation-image" alt="" style="display: block; margin-left: auto; margin-right: auto"/>
+                    <br />
+                    <span style="font-size: 110%"><b>Example new proofs discovered on ProofNet.</b> </span>
+
+                    <img src="images/proofnet_retrieval.jpg" class="interpolation-image" alt="" style="display: block; margin-left: auto; margin-right: auto"/>
+                    <br />
+                    <span style="font-size: 110%"><b>Three new proofs discovered on ProofNet that cannot be found without premise retrieval.</b> </span>
                 </div>
             </div>
         </div>