Plugin marketplace
Lean 4 language server plugin for Claude Code — automatic Lake project-root detection, elan toolchain resolution, multi-project routing, live diagnostics, and interactive proof-state queries via the bundled lean-goal CLI.
Add this marketplace
Then install any plugin below by name — each page has its exact command.
Lean 4 language server with automatic Lake project-root detection (works even when the session root is above the project), elan toolchain resolution, and multi-project routing. Bundles the lean-goal CLI for proof-goal state, sorry inventory, and fast diagnostics — plus a skill teaching the interactive proving workflow.
1 skill · LSP
Shows how many plugins this repo ships, and links here.