# Lean4 Lsp

> 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.

## Facts
- Page: https://tashan.sh/capability/plugin-lucianoxu-claude-lean4-lsp-lean4-lsp
- tashan id: plugin:lucianoxu/claude-lean4-lsp/lean4-lsp
- Source: https://github.com/LucianoXu/claude-lean4-lsp
- Type: plugin
- Category: devtools
- tashan score: 41.0 / 100
- Adoption: 7.0
- Upkeep: not measured
- Freshness: 99.0
- Evidence coverage: 59% of the inputs this score can use
- Health: active
- Instruction depth: not yet graded
- GitHub stars: 0
- Official: no

## Install

```sh
/plugin marketplace add LucianoXu/claude-lean4-lsp
/plugin install lean4-lsp@claude-lean4-lsp
```

## Security audit
Not scanned. We audit npm-published capabilities; this one has no npm package we can resolve, or has not reached the queue. This is not a clean bill of health.

---
Measured 2026-08-14 by tashan (https://tashan.sh) from public evidence. Scorer s5.