From claude-lean4-lsp
Lean language server provides code intelligence for Lean — diagnostics, go-to-definition, find references, hover information, and type checking for .lean files.
npx claudepluginhub lucianoxu/claude-lean4-lspThis LSP server requires leanto be installed on your system. Make sure it's available in your PATH before enabling.
Add to your .lsp.json or plugin.json:
{
"lspServers": {
"lean-standalone": {
"command": "lean",
"extensionToLanguage": {
".lean": "lean"
},
"args": [
"--server"
]
}
}
}leanstdioInitialization Options:
{}Settings:
{}