From 7cdfd3136e3e7db00e7975ed129c838a1833eebf Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Sun, 10 Dec 2023 08:48:48 -0800 Subject: [PATCH] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index ce7bc91..569d972 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ Lean Copilot: LLMs as Copilots for Theorem Proving in Lean ========================================================== -Lean Copilot allows large language models (LLMs) to be used in Lean for proof automation, e.g., suggesting tactics/premises and searching for proofs. Users can use our built-in models from [LeanDojo](https://leandojo.org/) or bring their own models that run either locally (w/ or w/o GPUs) or on the cloud. +Lean Copilot allows large language models (LLMs) to be used in Lean for proof automation, e.g., suggesting tactics/premises and searching for proofs. You can use our built-in models from [LeanDojo](https://leandojo.org/) or bring your own models that run either locally (w/ or w/o GPUs) or on the cloud.