Update README.md

lean-dojo · Dec 7, 2023 · 6d440d8 · 6d440d8
1 parent 1ab1332
commit 6d440d8
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -79,6 +79,8 @@ At any point in the proof, you can use the `select_premises` tactic to retrieve
 
 #### Running LLMs
 
+Lean Copilot also allows you to run the inference of LLMs in Lean, which can be used to build customized proof automation tools or a wide range of LLM-based applications not limited to theorem proving. 
+
 <img width="1123" alt="run_llms" src="https://github.com/lean-dojo/LeanCopilot/assets/5431913/a4e5b84b-a797-4216-a416-2958448aeb07">