Update index.html

lean-dojo · Dec 15, 2023 · ca28fe3 · ca28fe3
1 parent 7a2e37d
commit ca28fe3
Showing 1 changed file with 17 additions and 18 deletions.
diff --git a/index.html b/index.html
@@ -261,6 +261,21 @@ <h3 class="title is-4 conference-authors"><a target="_blank" href="https://nips.
 </section>
 -->
 
+<section class="section">
+    <div class="container is-max-widescreen">
+        <div class="rows">
+            <div class="rows is-centered ">
+                <div class="row is-full-width">
+                    <h2 class="title is-3"><span class="lean-infer">LLMs as Copilots for Theorem Proving</span></h2>
+                    <img src="images/LeanInfer.png" width="70%" class="interpolation-image" alt="" style="display: block; margin-left: auto; margin-right: auto"/>
+                    <br />
+                    <p style="font-size: 125%">We introduce <a target="_blank" href="https://github.com/lean-dojo/LeanCopilot">Lean Copilot</a> for LLMs to act as copilots in Lean for proof automation, e.g., suggesting tactics/premises and searching for proofs. Users can use our ReProver model or bring their own models that run either locally (w/ or w/o GPUs) or on the cloud.</p>
+                </div>
+            </div>
+        </div>
+    </div>
+</section>
+
 <section class="section">
     <div class="container is-max-widescreen">
         <div class="rows">
@@ -278,10 +293,9 @@ <h3 class="title is-4 conference-authors"><a target="_blank" href="https://nips.
         </div>
     </div>
 </section>
-
+<!--
 <section class="section">
     <div class="container is-max-desktop">
-        <!-- Abstract. -->
         <div class="columns is-centered has-text-centered">
             <div class="column">
                 <h2 class="title is-3">Abstract</h2>
@@ -308,6 +322,7 @@ <h2 class="title is-3">Abstract</h2>
         </div>
     </div>
 </section>
+-->
 
 
 <section class="section">
@@ -446,22 +461,6 @@ <h2 class="title is-3"><span class="dvima" id="chatgpt-for-theorem-proving">Chat
         </div>
     </div>
 </section>
-
-
-<section class="section">
-    <div class="container is-max-widescreen">
-        <div class="rows">
-            <div class="rows is-centered ">
-                <div class="row is-full-width">
-                    <h2 class="title is-3"><span class="lean-infer">LLMs as Copilots for Theorem Proving</span></h2>
-                    <img src="images/LeanInfer.png" width="70%" class="interpolation-image" alt="" style="display: block; margin-left: auto; margin-right: auto"/>
-                    <br />
-                    <p style="font-size: 125%">We introduce <a target="_blank" href="https://github.com/lean-dojo/LeanCopilot">Lean Copilot</a> for LLMs to act as copilots in Lean for proof automation, e.g., suggesting tactics/premises and searching for proofs. Users can use our ReProver model or bring their own models that run either locally (w/ or w/o GPUs) or on the cloud.</p>
-                </div>
-            </div>
-        </div>
-    </div>
-</section>
 
 
 <section class="section">