LLMLean
LLMlean integrates LLMs and Lean for tactic suggestions, proof completion, and more.
Here's an example of using LLMLean on problems from Mathematics in Lean:
https://github.com/user-attachments/assets/284a8b32-b7a5-4606-8240-effe086f2b82
You can use an LLM running on your laptop, or an LLM from the Open AI API or Together.ai API:

LLM in the cloud (default):
-
Get an OpenAI API key.
-
Modify
~/.config/llmlean/config.toml
(orC:\Users\<Username>\AppData\Roaming\llmlean\config.toml
on Windows), and enter the following:
api = "openai"
model = "gpt-4o"
apiKey = "<your-openai-api-key>"
(Alternatively, you may set the API key using the environment variable LLMLEAN_API_KEY
or using set_option llmlean.apiKey "<your-api-key>"
.)
Similarly, to set up an Anthropic LLM, use
api = "anthropic"
model = "claude-3-7-sonnet-20250219"
apiKey = "<your-anthropic-api-key>"
- Add
llmlean
to lakefile:
require llmlean from git
"https://github.com/cmu-l3/llmlean.git"
- Import:
import LLMlean
Now use a tactic described below.
Option 2: LLM on your laptop:
-
Install ollama.
-
Pull a language model:
ollama pull wellecks/ntpctx-llama3-8b
- Set 2 configuration variables in
~/.config/llmlean/config.toml
:
api = "ollama"
model = "wellecks/ntpctx-llama3-8b" # model name from above
Then do steps (3) and (4) above. Now use a tactic described below.
Option 3: LLM in the cloud (together.ai):
-
Get a together.ai API key.
-
Set 2 configuration variables in
~/.config/llmlean/config.toml
:
api = "together"
apiKey = "<your-together-api-key>"
Then do steps (3) and (4) above. Now use a tactic described below.
Tactics
llmstep
tactic
Next-tactic suggestions via llmstep "{prefix}"
. Examples:
-
llmstep ""
-
llmstep "apply "
The suggestions are checked in Lean.
llmqed
tactic
Complete the current proof via llmqed
. Examples:
The suggestions are checked in Lean.
For the best performance, especially for the llmqed
tactic, we recommend using the Open AI API.
Demo in PFR
Here is an example of proving a lemma with llmqed
(OpenAI GPT-4o):

And using llmqed
to make part of an existing proof simpler:

Customization
Please see the following:
Testing
Rebuild LLMLean with the config test=on
:
lake -R -Ktest=on update
lake build
Then manually check llmlean
on the files under LLMleanTest
.