LSP Server

lean-standalone

Lean language server provides code intelligence for Lean — diagnostics, go-to-definition, find references, hover information, and type checking for .lean files.

backend

Requires Language Server Binary

This LSP server requires leanto be installed on your system. Make sure it's available in your PATH before enabling.

Add to Your Project

Copy this JSON into your .lsp.json to enable this server

Add to your .lsp.json or plugin.json:

{
  "lspServers": {
    "lean-standalone": {
      "command": "lean",
      "extensionToLanguage": {
        ".lean": "lean"
      },
      "args": [
        "--server"
      ]
    }
  }
}

Supported Languages

File extensions mapped to language identifiers

lean

.lean

Details

Server configuration and transport parameters

Commandlean

Transportstdio

Arguments

Command-line arguments passed to the server process

--server

Advanced Configuration

Initialization options and workspace settings

Startup Timeout:60000ms

Shutdown Timeout:15000ms

Restart on Crash:Yes

Max Restarts:3

Initialization Options:

{}

Settings:

{}

Stats

Stars0

MaintenanceExcellent

Last CommitMar 18, 2026

Actions

Plugins (1)

claude-lean4-lsp0

Stats

Actions