diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json
index c11e6442..e5a19f78 100644
--- a/.claude-plugin/marketplace.json
+++ b/.claude-plugin/marketplace.json
@@ -228,6 +228,26 @@
         }
       }
     },
+    {
+      "name": "lean4-lsp",
+      "description": "Lean 4 language server for theorem proving",
+      "version": "1.0.0",
+      "author": {
+        "name": "Alok Singh"
+      },
+      "source": "./plugins/lean4-lsp",
+      "category": "development",
+      "strict": false,
+      "lspServers": {
+        "lean": {
+          "command": "lake",
+          "args": ["serve", "--"],
+          "extensionToLanguage": {
+            ".lean": "lean"
+          }
+        }
+      }
+    },
     {
       "name": "agent-sdk-dev",
       "description": "Development kit for working with the Claude Agent SDK",
diff --git a/plugins/lean4-lsp/README.md b/plugins/lean4-lsp/README.md
new file mode 100644
index 00000000..9d46c07b
--- /dev/null
+++ b/plugins/lean4-lsp/README.md
@@ -0,0 +1,18 @@
+# lean4-lsp
+
+Lean 4 language server for Claude Code, providing code intelligence for theorem proving.
+
+## Supported Extensions
+`.lean`
+
+## Installation
+
+Install Lean 4 via elan:
+
+```bash
+curl https://elan.lean-lang.org -sSf | sh
+```
+
+## More Information
+- [Lean 4](https://lean-lang.org/)
+- [elan](https://github.com/leanprover/elan)