LeanHelper

A Visual Studio Code extension that provides AI-powered proof suggestions when hovering over sorry in Lean files.

Features

• Smart Hover Detection: Automatically detects when you hover over sorry in Lean files
• AI Proof Suggestions: Shows contextual proof strategies and tactics from a language model
• Context-Aware: Analyzes the full file content to understand the theorem/lemma/def context
• Configurable LLM: Works with OpenAI, Anthropic, or any compatible LLM API
• Lightweight: Minimal performance impact with fast response times

How to Use

1. Configure your API key (see Configuration section below)
2. Open any .lean file in VS Code
3. Hover over any instance of sorry in your code
4. A popup will appear with AI-generated proof suggestions

Configuration

Setting up your LLM API key:

1. Open VS Code Settings:
   • Press Cmd+Shift+P (Mac) or Ctrl+Shift+P (Windows/Linux)
   • Type "Preferences: Open Settings (JSON)"
   • Add the following configuration:

{
  "leanhelper.apiKey": "your-openai-api-key-here",
  "leanhelper.apiEndpoint": "https://api.openai.com/v1/chat/completions",
  "leanhelper.model": "gpt-4"
}

Supported LLM Services:

• OpenAI: Use https://api.openai.com/v1/chat/completions with models like gpt-4, gpt-3.5-turbo
• Anthropic: Use https://api.anthropic.com/v1/messages with models like claude-3-opus-20240229
• Other compatible APIs: Any API that follows the OpenAI chat completion format

Example

When you hover over sorry in a theorem like:

theorem add_zero (n : Nat) : n + 0 = n := by
  sorry

You'll see AI-generated suggestions like:

rw [Nat.add_zero]

The AI analyzes the full context of your file to provide relevant proof tactics.

Requirements

• Visual Studio Code 1.101.0 or higher
• Lean files (.lean extension)
• Valid LLM API key (OpenAI, Anthropic, etc.)

Extension Settings

This extension adds the following settings:

• leanhelper.apiKey: Your LLM API key
• leanhelper.apiEndpoint: The API endpoint URL
• leanhelper.model: The model name to use

Development

Building the Extension

npm install
npm run compile

Running in Development

1. Press F5 in VS Code to open a new Extension Development Host window
2. Open a .lean file in the new window
3. Add some sorry statements and hover over them to test

Customizing the LLM Integration

The extension uses a configurable API approach. To integrate with a different LLM:

1. Update the apiEndpoint in your settings
2. Modify the request format in src/extension.ts if needed
3. Adjust the response parsing if your API returns a different format

Known Issues

• Currently only works with the exact word sorry (case-insensitive)
• Requires a valid API key to function
• API calls may have rate limits depending on your service
• No caching of suggestions for repeated hovers

Release Notes

0.0.1

• Initial release
• Basic hover functionality for sorry in Lean files
• AI-powered proof suggestions via LLM API
• Configurable API settings

Contributing

Feel free to submit issues and enhancement requests!

License

This extension is provided as-is for educational and development purposes.