~

index.html

@@ -441,10 +441,6 @@ <h2 class="title is-3"><span class="dvima">Discovering New Proofs and Uncovering
             <div class="rows is-centered ">
                 <div class="row is-full-width">
                     <h2 class="title is-3"><span class="dvima">ChatGPT for Theorem Proving</span></h2>
-
-                    <p style="font-size: 125%">We build a <a target="_blank" href="https://github.com/lean-dojo/LeanDojoChatGPT">LeanDojo ChatGPT plugin</a> that enables ChatGPT to prove theorems by interacting with Lean. Compared to specialized LLMs finetuned for theorem proving (e.g., ReProver), ChatGPT can interleave informal mathematics with formal proof steps, similar to how humans interact with proof assistants. It can explain error messages from Lean and is more steerable (by prompting engineering) than specialized provers. However, it struggles to find correct proofs in most cases.</p>
-                    <br />
-
                     <div class="columns">
                         <div class="column has-text-left video-column">
                             <video controls muted width="100%">
@@ -473,6 +469,8 @@ <h2 class="title is-3"><span class="dvima">ChatGPT for Theorem Proving</span></h
                             </div>
                         </div>
                     </div>
+                    <br />
+                    <p style="font-size: 125%">We build a <a target="_blank" href="https://github.com/lean-dojo/LeanDojoChatGPT">LeanDojo ChatGPT plugin</a> that enables ChatGPT to prove theorems by interacting with Lean. Compared to specialized LLMs finetuned for theorem proving (e.g., ReProver), ChatGPT can interleave informal mathematics with formal proof steps, similar to how humans interact with proof assistants. It can explain error messages from Lean and is more steerable (by prompting engineering) than specialized provers. However, it struggles to find correct proofs in most cases.</p>
                 </div>
             </div>
         </div>