claudeindex
Plugin

lean4-lake-lsp

Lean 4 language server via Lake — for Lake projects with dependencies (e.g., Mathlib). Replaces the inefficient CLI-based lake build workflow with native LSP integration for interactive theorem proving.

Installation

1

Add the marketplace

/plugin marketplace add Piebald-AI/claude-code-lsps
2

Install plugins

/plugin

Run these commands in Claude Code to add this plugin to your environment. The marketplace must be added before you can install its plugins.

Repository & Links

Plugin Source

View Plugin Code

GitHub Repository

Piebald-AI/claude-code-lsps

Details & Metadata