Lean LSP MCP Server

What does “Lean LSP MCP” Server do?

Lean LSP MCP is a Model Context Protocol (MCP) server that connects AI assistants with Lean Theorem Prover projects via the Language Server Protocol (LSP) using the leanclient. It enables agents and LLMs to interact with Lean projects, providing access to diagnostics, goal states, term information, hover documentation, and more. This integration streamlines development workflows for Lean users by exposing a rich agent-focused toolset, including theorem search, code completion, and project build functionality. The server aims to enhance the experience of developers, researchers, and AI agents working with Lean by making Lean’s tooling accessible in automated and interactive contexts.

List of Prompts

No information about prompt templates was found in the repository.

List of Resources

No information about exposed MCP resources was found in the repository.

List of Tools

• Lean Theorem Search: Allows agents to search for theorems using leansearch.net integration.
• Code Completion: Provides code completion suggestions for Lean files.
• Project Build: Facilitates project builds through the Lean build system.
• Diagnostics: Offers access to diagnostics within Lean projects.
• Goal States & Term Info: Exposes goal state and term information for deeper project analysis.
• Hover Documentation: Returns documentation when hovering over Lean code elements.

Use Cases of this MCP Server

• Lean Project Diagnostics: Instantly access and surface diagnostics for code correctness and debugging within Lean projects.
• Goal State Exploration: Retrieve and display current goal states for proof development and strategy planning.
• Theorem Search: Search for relevant theorems from leansearch.net to assist in proof construction.
• Code Completion for Lean: Provide intelligent code completion and suggestions for Lean, enhancing productivity.
• Automated Project Builds: Trigger and monitor Lean project builds as part of automated workflows or agentic code review.

How to set it up

Windsurf

1. Ensure uv is installed.
2. Build your Lean project by running lake build in your project root.
3. Locate the Windsurf configuration file.
4. Add the Lean LSP MCP server using the following JSON snippet:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

5. Save and restart Windsurf, then verify the MCP server is running.

Claude

1. Install uv and run lake build in your Lean project.
2. Open Claude’s configuration file.
3. Insert the MCP server configuration:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. Save and restart Claude, then confirm the server is available.

Cursor

1. Install uv and run lake build.
2. Open Cursor’s config file.
3. Add the Lean LSP MCP server:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. Save changes and restart Cursor.

Cline

1. Make sure uv is installed and run lake build.
2. Find and edit the Cline configuration file.
3. Add the server:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. Save and restart Cline.

Securing API Keys

If your setup requires API keys, use environment variables to keep them secure. Example:

{
  "mcpServers": {
    "lean-lsp-mcp": {
      "command": "lean-lsp-mcp",
      "args": [],
      "env": {
        "API_KEY": "${env:LEAN_LSP_MCP_API_KEY}"
      },
      "inputs": {
        "api_key": "${env:LEAN_LSP_MCP_API_KEY}"
      }
    }
  }
}

How to use this MCP inside flows

Using MCP in FlowHunt

To integrate MCP servers into your FlowHunt workflow, start by adding the MCP component to your flow and connecting it to your AI agent:

Click on the MCP component to open the configuration panel. In the system MCP configuration section, insert your MCP server details using this JSON format:

{
  "lean-lsp-mcp": {
    "transport": "streamable_http",
    "url": "https://yourmcpserver.example/pathtothemcp/url"
  }
}

Once configured, the AI agent is now able to use this MCP as a tool with access to all its functions and capabilities. Remember to change “lean-lsp-mcp” to whatever the actual name of your MCP server is and replace the URL with your own MCP server URL.

Overview

Based on the available documentation and code, Lean LSP MCP provides strong tooling support for Lean projects but lacks explicit prompt templates or MCP resource definitions. Sampling and roots support are not mentioned. Overall, the server is practical for Lean users but does not yet expose the full spectrum of advanced MCP features.

MCP Score