LLMlean integrates LLMs and Lean for tactic suggestions, proof completion, and more.
You can use an LLM running on your laptop, or an LLM from the Open AI API or Together.ai API:
-
Install ollama.
-
Pull a language model:
ollama pull wellecks/ntpctx-llama3-8b
- Add
llmlean
to lakefile:
require llmlean from git
"https://github.com/cmu-l3/llmlean.git"
- Import:
import LLMlean
Now use a tactic described below.
-
Get an OpenAI API key.
-
Set 2 environment variables:
export LLMLEAN_API=openai
export LLMLEAN_API_KEY=your-openai-api-key
Then do steps (3) and (4) above. Now use a tactic described below.
-
Get a together.ai API key.
-
Set 2 environment variables:
export LLMLEAN_API=together
export LLMLEAN_API_KEY=your-together-api-key
Then do steps (3) and (4) above. Now use a tactic described below.
Next-tactic suggestions via llmstep "{prefix}"
. Examples:
The suggestions are checked in Lean.
Complete the current proof via llmqed
. Examples:
The suggestions are checked in Lean.
Please see the following: