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:

You can use an LLM running on your laptop, or an LLM from the Open AI API or Together.ai API:

1. Get an OpenAI API key.

2. Set 1 environment variable:

export LLMLEAN_API_KEY=your-openai-api-key

To do so, add the export statement to the ~/.zshrc file (on Mac) or ~/.bashrc (Linux), and restart VS Code.

3. Add llmlean to lakefile:

require llmlean from git
  "https://github.com/cmu-l3/llmlean.git"

4. Import:

import LLMlean

Now use a tactic described below.

1. Install ollama.

2. Pull a language model:

ollama pull wellecks/ntpctx-llama3-8b

3. Set 2 environment variables:

export LLMLEAN_API=ollama
export LLMLEAN_MODEL=wellecks/ntpctx-llama3-8b # model name from above

Then do steps (3) and (4) above. Now use a tactic described below.

1. Get a together.ai API key.

2. 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:

• llmstep ""

  

• llmstep "apply "

  

The suggestions are checked in Lean.

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.

Here is an example of proving a lemma with llmqed (OpenAI GPT-4o):

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

Please see the following:

• Customization