LLMLean

LLM on your laptop:

1. Install ollama.

2. Pull a language model:

ollama pull solobsd/llemma-7b

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.

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