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:

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

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.

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

import LLMlean

Now use a tactic described below.

ollama pull wellecks/ntpctx-llama3-8b

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.

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.

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: