From ca28fe3468f3c709972bf1ca85c7329b9a38070b Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Thu, 14 Dec 2023 19:26:08 -0800 Subject: [PATCH] Update index.html --- index.html | 35 +++++++++++++++++------------------ 1 file changed, 17 insertions(+), 18 deletions(-) diff --git a/index.html b/index.html index 5323ce6..82ee793 100644 --- a/index.html +++ b/index.html @@ -261,6 +261,21 @@

+
+
+
+
+

LLMs as Copilots for Theorem Proving

+ +
+

We introduce Lean Copilot 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.

+
+
+
+
+ +
@@ -278,10 +293,9 @@

-

Abstract

@@ -308,6 +322,7 @@

Abstract

+-->
@@ -446,22 +461,6 @@

Chat

- - -
-
-
-
-
-

LLMs as Copilots for Theorem Proving

- -
-

We introduce Lean Copilot 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.

-
-
-
-
-