LLMLean

LLM on your laptop:
  1. Install ollama.

  2. Pull a language model:

ollama pull solobsd/llemma-7b
  1. Add llmlean to lakefile:
require llmlean from git
  "https://github.com/cmu-l3/llmlean.git"
  1. Import:
import LLMlean

Now use a tactic described below.

LLM in the cloud:
  1. Get a together.ai API key.

  2. Set 2 environment variables in VS Code. Example:

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


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.


Customization

Please see the following:

  1. Customization