justincasher · justincasher · Aug 2, 2026 · Aug 2, 2026 · Aug 2, 2026 · Aug 2, 2026
diff --git a/.agents/plugins/marketplace.json b/.agents/plugins/marketplace.json
@@ -0,0 +1,20 @@
+{
+  "name": "lean-explore",
+  "interface": {
+    "displayName": "Lean Explore"
+  },
+  "plugins": [
+    {
+      "name": "lean-explore",
+      "source": {
+        "source": "local",
+        "path": "./plugins/lean-explore"
+      },
+      "policy": {
+        "installation": "AVAILABLE",
+        "authentication": "ON_INSTALL"
+      },
+      "category": "Developer Tools"
+    }
+  ]
+}
diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json
@@ -0,0 +1,16 @@
+{
+  "name": "lean-explore",
+  "owner": {
+    "name": "Justin Asher",
+    "email": "justinchadwickasher@gmail.com"
+  },
+  "description": "Plugins for searching Lean 4 declarations with LeanExplore.",
+  "plugins": [
+    {
+      "name": "lean-explore",
+      "source": "./plugins/lean-explore",
+      "description": "Search Lean 4 declarations through the hosted LeanExplore MCP server.",
+      "version": "0.1.0"
+    }
+  ]
+}
diff --git a/README.md b/README.md
@@ -56,6 +56,34 @@ lean-explore data fetch
 lean-explore mcp serve --backend local
 ```
 
+## Claude Code and Codex plugin
+
+The repository includes a plugin for both Claude Code and Codex. It connects to
+the hosted MCP server, so it does not need a Python install, a local search
+index, account, API key, or browser authorization. The tools are available as
+soon as the plugin is installed.
+
+The hosted endpoint allows 30 POST requests per client IP in any 60-second
+window. Protocol initialization and tool-discovery requests count toward the
+limit, and clients sharing a public IP share the same budget.
+
+In Claude Code:
+
+```text
+/plugin marketplace add justincasher/lean-explore
+/plugin install lean-explore@lean-explore
+/reload-plugins
+```
+
+In Codex:
+
+```bash
+codex plugin marketplace add https://github.com/justincasher/lean-explore
+codex plugin add lean-explore@lean-explore
+```
+
+Start a new Codex session after installation so the MCP tools are loaded.
+
 ## Documentation
 
 Full docs live in the [`docs/`](docs/README.md) folder, or at [https://www.leanexplore.com/docs](https://www.leanexplore.com/docs).

diff --git a/docs/README.md b/docs/README.md
@@ -29,7 +29,7 @@ LeanExplore has two backends and you pick one per task:
 | | **Remote API** | **Local backend** |
 |---|---|---|
 | Install | `pip install lean-explore` | `pip install lean-explore[local]` |
-| Requires | API key | ~1 GB of data + a few GB of model weights |
+| Requires | Network access | ~1 GB of data + a few GB of model weights |
 | Network | Required per query | Only for initial data fetch |
 | Use when | You want zero setup | You want offline, private, or tunable search |
 

diff --git a/docs/api-client.md b/docs/api-client.md
@@ -4,20 +4,13 @@
 LeanExplore API. It ships with the base package: no PyTorch, no local
 indices, no data download required.
 
-## Install and authenticate
+## Install
 
 ```bash
 pip install lean-explore
 ```
 
-Get an API key from <https://www.leanexplore.com> and set it as an
-environment variable:
-
-```bash
-export LEANEXPLORE_API_KEY="your-key-here"
-```
-
-Or pass it explicitly to the client constructor.
+No account or API key is required.
 
 ## Quick start
 
@@ -26,7 +19,7 @@ import asyncio
 from lean_explore.api import ApiClient
 
 async def main():
-    client = ApiClient()  # reads LEANEXPLORE_API_KEY
+    client = ApiClient()
 
     response = await client.search("prime number divisibility", limit=5)
     for result in response.results:
@@ -46,7 +39,7 @@ ApiClient(api_key: str | None = None, timeout: float = 10.0)
 
 | Parameter | Default | Description |
 |---|---|---|
-| `api_key` | `None` | API key. Falls back to `LEANEXPLORE_API_KEY` env var. Raises `ValueError` if neither is provided. |
+| `api_key` | `None` | Deprecated compatibility argument. Accepted and ignored. |
 | `timeout` | `10.0` | HTTP timeout in seconds for every request. |
 
 The client hits `https://www.leanexplore.com/api/v2` by default.
@@ -95,7 +88,7 @@ import asyncio
 from lean_explore.api import ApiClient
 
 async def main():
-    client = ApiClient(api_key="sk-...", timeout=15.0)
+    client = ApiClient(timeout=15.0)
 
     response = await client.search(
         query="continuous function on a compact set",
@@ -132,5 +125,4 @@ asyncio.run(main())
 
 - [Data Models](./data-models.md): field reference for `SearchResult` and
   `SearchResponse`.
-- [Configuration](./configuration.md): environment variables including
-  `LEANEXPLORE_API_KEY`.
+- [Configuration](./configuration.md): environment variables and data paths.
diff --git a/docs/cli.md b/docs/cli.md
@@ -39,12 +39,8 @@ lean-explore search QUERY [OPTIONS]
 
 ### Requirements
 
-`lean-explore search` uses the remote API. You must have `LEANEXPLORE_API_KEY`
-set in your environment:
-
-```bash
-export LEANEXPLORE_API_KEY="your-key-here"
-```
+`lean-explore search` uses the public remote API. No account or API key is
+required.
 
 ### Examples
 
@@ -71,12 +67,11 @@ lean-explore mcp serve [OPTIONS]
 | Flag | Default | Description |
 |---|---|---|
 | `--backend`, `-b` | `api` | Backend to use: `api` or `local`. |
-| `--api-key` | (none) | API key for the `api` backend. Overrides `LEANEXPLORE_API_KEY`. |
+| `--api-key` | (none) | Deprecated compatibility option. Accepted and ignored. |
 
 ### Backends
 
-- **`api`**: Delegates every query to the hosted LeanExplore API. Requires an
-  API key (via env var or `--api-key`).
+- **`api`**: Delegates every query to the public hosted LeanExplore API.
 - **`local`**: Runs the full hybrid search pipeline on-device. Requires
   `pip install lean-explore[local]` and `lean-explore data fetch`.
 
@@ -86,7 +81,7 @@ lean-explore mcp serve [OPTIONS]
 # Remote API (most users)
 lean-explore mcp serve --backend api
 
-# Remote API with an inline key
+# Legacy syntax remains valid; the value is ignored
 lean-explore mcp serve --backend api --api-key sk-...
 
 # Local, fully offline backend
@@ -154,7 +149,7 @@ touch downloaded model weights; those live under `~/.cache/huggingface/`.
 All CLI commands follow standard conventions:
 
 - `0`: success
-- non-zero: an error occurred (missing API key, failed download, etc.).
+- non-zero: an error occurred (failed request, failed download, etc.).
   An error message is printed to stderr.
 
 ## See also

diff --git a/docs/configuration.md b/docs/configuration.md
@@ -8,9 +8,8 @@ live on disk, and how to override defaults. Configuration is centralized in
 
 ### Authentication
 
-| Variable | Default | Used by |
-|---|---|---|
-| `LEANEXPLORE_API_KEY` | (required for API use) | `ApiClient`, `lean-explore search`, `lean-explore mcp serve --backend api` |
+The public API, CLI search command, and stdio MCP API backend do not require
+credentials. `LEANEXPLORE_API_KEY` is deprecated and ignored when present.
 
 ### Paths
 

diff --git a/docs/getting-started.md b/docs/getting-started.md
@@ -26,18 +26,7 @@ pip install lean-explore
 This installs the CLI, the `ApiClient`, and the MCP server, roughly 50 MB
 of pure-Python and C-extension dependencies. No PyTorch.
 
-### 2. Get an API key
-
-Sign up and generate a key at <https://www.leanexplore.com>. Then export it:
-
-```bash
-export LEANEXPLORE_API_KEY="your-key-here"
-```
-
-You can also add it to your shell profile (`~/.zshrc`, `~/.bashrc`) so it
-persists between sessions.
-
-### 3. Run a search
+### 2. Run a search
 
 ```bash
 lean-explore search "prime number divisibility"
@@ -49,7 +38,7 @@ The first argument is the query. It can be a Lean declaration name, a partial
 name, or a natural-language description. The search engine handles both at
 once; you don't need to pick a mode.
 
-### 4. (Optional) Run the MCP server
+### 3. (Optional) Run the MCP server
 
 If you want to give Claude, Cursor, or another MCP client access to
 LeanExplore:

diff --git a/docs/mcp-server.md b/docs/mcp-server.md
@@ -12,6 +12,35 @@ This page covers:
 - [The tools](#the-tools) and their schemas
 - [Recommended agent workflow](#recommended-agent-workflow)
 
+## Hosted plugin (Claude Code and Codex)
+
+The recommended setup is the repository's `lean-explore` plugin. It points at
+`https://www.leanexplore.com/mcp`; no local executable, account, API key,
+browser authorization, or model data is required.
+
+The hosted endpoint allows 30 POST requests per client IP in any 60-second
+window. MCP initialization and tool-discovery requests count toward that
+total, and clients behind the same NAT or proxy share the limit. When the
+limit is reached, the server returns HTTP 429 with a `Retry-After` header.
+
+Claude Code:
+
+```text
+/plugin marketplace add justincasher/lean-explore
+/plugin install lean-explore@lean-explore
+/reload-plugins
+```
+
+Codex:
+
+```bash
+codex plugin marketplace add https://github.com/justincasher/lean-explore
+codex plugin add lean-explore@lean-explore
+```
+
+The stdio server described below remains available for existing configurations
+and for the fully local backend.
+
 ## Running the server
 
 The server speaks MCP over stdio; your client launches it as a subprocess.
@@ -23,7 +52,7 @@ You rarely invoke it directly except for debugging.
 lean-explore mcp serve --backend api
 ```
 
-Requires `LEANEXPLORE_API_KEY` in the environment, or pass `--api-key`:
+No account or API key is required. The old option remains accepted as a no-op:
 
 ```bash
 lean-explore mcp serve --backend api --api-key sk-...
@@ -55,10 +84,7 @@ on macOS):
   "mcpServers": {
     "lean-explore": {
       "command": "lean-explore",
-      "args": ["mcp", "serve", "--backend", "api"],
-      "env": {
-        "LEANEXPLORE_API_KEY": "your-key-here"
-      }
+      "args": ["mcp", "serve", "--backend", "api"]
     }
   }
 }
@@ -84,8 +110,6 @@ Any client that accepts a command + args will work. Point it at the
 
 ### Troubleshooting
 
-- **"API key required"**: set `LEANEXPLORE_API_KEY` in the `env` block (for
-  MCP clients that support it) or pass `--api-key` in `args`.
 - **"Essential data files for the local backend are missing"**: run
   `lean-explore data fetch` first.
 - **Tools do not appear in the client**: check the client's MCP logs. The

diff --git a/openapi.yaml b/openapi.yaml
@@ -7,8 +7,8 @@ info:
     Lean 4 declarations from indexed projects including Mathlib, PhysLean,
     FLT, and more.
 
-    Authentication is required via an API key provided as a Bearer token
-    in the Authorization header.
+    The API is public and does not require authentication. Legacy API-key
+    headers are accepted by the HTTP stack but have no effect.
   contact:
     name: Justin Asher
     email: justinchadwickasher@gmail.com
@@ -28,14 +28,6 @@ servers:
     description: Production LeanExplore API Server
 
 components:
-  securitySchemes:
-    BearerAuth:
-      type: http
-      scheme: bearer
-      description: >-
-        API key provided as a Bearer token.
-        Example: `Authorization: Bearer YOUR_API_KEY`
-
   schemas:
     SearchResult:
       type: object
@@ -120,10 +112,7 @@ components:
         msg:
           type: string
           description: Human-readable error message.
-          example: "Invalid or missing API key"
-
-security:
-  - BearerAuth: []
+          example: "Invalid request"
 
 paths:
   /search:
@@ -162,14 +151,8 @@ paths:
             application/json:
               schema:
                 $ref: '#/components/schemas/ApiError'
-        '401':
-          description: Unauthorized - Invalid or missing API key.
-          content:
-            application/json:
-              schema:
-                $ref: '#/components/schemas/ApiError'
         '429':
-          description: Too Many Requests - Rate limit exceeded.
+          description: Too Many Requests - Per-IP search limit of 30 requests per minute exceeded.
           content:
             application/json:
               schema:
@@ -204,20 +187,14 @@ paths:
             application/json:
               schema:
                 $ref: '#/components/schemas/SearchResult'
-        '401':
-          description: Unauthorized - Invalid or missing API key.
-          content:
-            application/json:
-              schema:
-                $ref: '#/components/schemas/ApiError'
         '404':
           description: Not Found - Declaration does not exist.
           content:
             application/json:
               schema:
                 $ref: '#/components/schemas/ApiError'
         '429':
-          description: Too Many Requests - Rate limit exceeded.
+          description: Too Many Requests - Per-IP declaration limit of 240 requests per minute exceeded.
           content:
             application/json:
               schema:

diff --git a/plugins/lean-explore/.claude-plugin/plugin.json b/plugins/lean-explore/.claude-plugin/plugin.json
@@ -0,0 +1,13 @@
+{
+  "name": "lean-explore",
+  "version": "0.1.0",
+  "description": "Search Lean 4 declarations through the hosted LeanExplore MCP server.",
+  "author": {
+    "name": "Justin Asher",
+    "email": "justinchadwickasher@gmail.com"
+  },
+  "homepage": "https://www.leanexplore.com/docs/mcp",
+  "repository": "https://github.com/justincasher/lean-explore",
+  "license": "Apache-2.0",
+  "keywords": ["lean", "lean4", "mathlib", "mcp", "theorem-proving"]
+}