Lean Scribe: Render and run context-rich prompts in VSCode

Stream: Machine Learning for Theorem Proving

[Oliver Dressler]

Lean Scribe is a VSCode extension that runs alongside the "Lean 4" extension. It can render and execute context-rich prompts:

• You can define prompts as markdown template files containing variables.
• Lean Scribe renders prompts based on the current context (open file, cursor, messages, goals, etc).
• You can then pick from various LLM models to run the prompt and compare.

To use Lean Scribe, run a local model with ollama or get some API keys, install the extension, and execute a command.

Check out the github readme to get started.

See the default prompts for some examples of Lean Scribe prompts covering a few use-cases.

I am looking for testers and feedback. Particularly on:

• The prompt file format: Is it intuitive? Expressive? Future-proof?
• UX: Which features and editor integrations would improve your workflow?
• Bugs: Thanks for squishing them on github!

Screenshot: Rendered prompt to learn more about a file