### Install uv Package Manager

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Installs the uv package manager, a fast Python package installer, using a curl script. This is a prerequisite for setting up the lean-lsp-mcp server.

```bash
curl -LsSf https://astral.sh/uv/install.sh | sh
```

--------------------------------

### Lean LSP MCP Client Configuration (JSON)

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Provides an example of how to configure the Lean LSP MCP server within a client's configuration file, specifically showing how to set the transport type, command, arguments, and environment variables like LEAN_PROJECT_PATH.

```json
{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "uvx",
            "args": [
                "lean-lsp-mcp"
            ],
            "env": {
                "LEAN_PROJECT_PATH": "/path/to/your/lean/project"
            }
        }
    }
}
```

--------------------------------

### Server Transport Method Configuration (Bash)

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Demonstrates how to start the Lean LSP MCP server using different transport methods: stdio (default), streamable-http, and sse. It also shows how to specify host and port for HTTP-based transports.

```bash
uvx lean-lsp-mcp --transport stdio # Default transport
uvx lean-lsp-mcp --transport streamable-http # Available at http://127.0.0.1:8000/mcp
uvx lean-lsp-mcp --transport sse --host localhost --port 12345 # Available at http://localhost:12345/sse
```

--------------------------------

### Bearer Token Authentication Setup (Bash)

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Illustrates how to set up bearer token authentication for the Lean LSP MCP server when using streamable-http or sse transport. This involves exporting the token as an environment variable before starting the server.

```bash
export LEAN_LSP_MCP_TOKEN="your_secret_token"
uvx lean-lsp-mcp --transport streamable-http
```

--------------------------------

### Lean LSP MCP Server Configuration and Transport

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Details on configuring the Lean LSP MCP server, including supported transport methods and how to specify them via command-line arguments. It also covers the setup for streamable-http and SSE transports with host and port configurations.

```APIDOC
## Server Configuration and Transport

### Description
This section details the available transport methods for the Lean LSP MCP server and how to configure them.

### Transport Methods
- `stdio`: Standard input/output (default)
- `streamable-http`: HTTP streaming
- `sse`: Server-sent events (MCP legacy, use `streamable-http` if possible)

### Command-Line Examples

**Using `stdio` (default):**
```bash
uvx lean-lsp-mcp --transport stdio
```

**Using `streamable-http`:**
```bash
uvx lean-lsp-mcp --transport streamable-http
```

**Using `sse` with custom host and port:**
```bash
uvx lean-lsp-mcp --transport sse --host localhost --port 12345
```
```

--------------------------------

### Claude Code MCP Server Addition (Bash)

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Adds the lean-lsp MCP server using the Claude CLI. Examples show local-scoped, project-scoped (updating .mcp.json), and manual path setting for the Lean project.

```bash
# Local-scoped MCP server
claude mcp add lean-lsp uvx lean-lsp-mcp

# OR project-scoped MCP server (creates or updates a .mcp.json file in the current directory)
claude mcp add lean-lsp -s project uvx lean-lsp-mcp

# OR If you run into issues with the project path (e.g. the language server directory cannot be found), you can also set it manually e.g.
claude mcp add lean-lsp uvx lean-lsp-mcp -e LEAN_PROJECT_PATH=$PWD
```

--------------------------------

### VSCode MCP Server Configuration (JSONC)

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Manually configures the lean-lsp MCP server in VSCode's mcp.json file. It specifies the server type as 'stdio' and uses 'uvx lean-lsp-mcp' as the command and arguments.

```jsonc
{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "uvx",
            "args": [
                "lean-lsp-mcp"
            ]
        }
    }
}
```

--------------------------------

### Cursor MCP Server Configuration (JSONC)

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Configures the lean-lsp MCP server for Cursor by pasting the provided JSON into the mcp.json file. It specifies the command 'uvx' and arguments 'lean-lsp-mcp'.

```jsonc
{
    "mcpServers": {
        "lean-lsp": {
            "command": "uvx",
            "args": ["lean-lsp-mcp"]
        }
    }
}
```

--------------------------------

### Attempt Multiple Lean Proofs

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Allows for the execution of multiple Lean code snippets on a single line to evaluate different proof strategies. It returns the goal state and diagnostics for each snippet, facilitating the selection of the most promising proof attempt.

```Lean
rw [Nat.pow_sub (Fintype.card_pos_of_nonempty S)]
by_contra h_neq
```

--------------------------------

### Build Lean Project

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Executes the 'lake build' command in the root directory of a Lean project. This is recommended to ensure the language server builds quickly and to avoid potential timeouts in certain IDEs.

```bash
cd /path/to/lean/project
lake build
```

--------------------------------

### Environment Variables for lean-lsp-mcp

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Lists and describes the environment variables used to configure optional features and integrations for the lean-lsp-mcp server, including project path, authentication token, and URLs for external services.

```APIDOC
## Environment Variables

### Description
Environment variables are used to configure optional features and integrations for the `lean-lsp-mcp` server.

### Available Environment Variables
- `LEAN_PROJECT_PATH`: (optional) Path to your Lean project root. Use if the server cannot auto-detect it.
- `LEAN_LSP_MCP_TOKEN`: (optional) Secret token for bearer authentication with `streamable-http` or `sse` transport.
- `LEAN_STATE_SEARCH_URL`: (optional) URL for a self-hosted premise-search.com instance.
- `LEAN_HAMMER_URL`: (optional) URL for a self-hosted Lean Hammer Premise Search instance.

### Configuration Example (MCP Client)
Environment variables can often be set within the MCP client configuration:

```jsonc
{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "uvx",
            "args": [
                "lean-lsp-mcp"
            ],
            "env": {
                "LEAN_PROJECT_PATH": "/path/to/your/lean/project",
                "LEAN_LSP_MCP_TOKEN": "your_secret_token"
            }
        }
    }
}
```
```

--------------------------------

### Search Lean Premises (Lean Hammer)

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Searches for relevant premises based on the current proof state using the Lean Hammer Premise Search server. It returns a list of theorem names that can be used to prove the goal.

```json
[
  "MulOpposite.unop_injective",
  "MulOpposite.op_injective",
  "WellFoundedLT.induction",
  ...
]
```

--------------------------------

### Search Applicable Theorems for Proof Goal

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Finds theorems relevant to the current proof goal using premise-search.com. It targets the first goal at a specified line and column, returning a list of applicable theorems in JSON format.

```json
[
  {
    "name": "Nat.mul_zero",
    "formal_type": "∀ (n : Nat), n * 0 = 0",
    "module": "Init.Data.Nat.Basic"
  }
]
```

--------------------------------

### Run MCP Inspector CLI

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

This command uses npx to run the MCP Inspector tool. It takes a path to the lean-lsp-mcp project and specifies the server to run using Python. This is useful for debugging and inspecting the MCP server.

```bash
npx @modelcontextprotocol/inspector uvx --with-editable path/to/lean-lsp-mcp python -m lean_lsp_mcp.server
```

--------------------------------

### Search Mathlib Theorems (Natural Language)

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Searches for theorems within the Mathlib library using natural language queries via leansearch.net. It supports mixed queries, concepts, identifiers, and Lean terms, returning structured JSON data about matching theorems.

```json
{
    "module_name": "Mathlib.Logic.Function.Basic",
    "kind": "theorem",
    "name": "Function.Bijective.injective",
    "signature": " {f : α → β} (hf : Bijective f) : Injective f",
    "type": "∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Bijective f → Function.Injective f",
    "value": ":= hf.1",
    "informal_name": "Bijectivity Implies Injectivity",
    "informal_description": "For any function $f \colon \alpha \to \beta$, if $f$ is bijective, then $f$ is injective."
  }
```

--------------------------------

### File Interactions (LSP)

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Documents the available tools for interacting with Lean files via the Language Server Protocol (LSP) within the MCP server, including fetching file contents, diagnostics, and goal information.

```APIDOC
## File Interactions (LSP)

### Description
Tools for interacting with Lean files using the Language Server Protocol (LSP).

### Tools

#### `lean_file_contents`

**Description:** Get the contents of a Lean file, optionally with line number annotations.

#### `lean_diagnostic_messages`

**Description:** Get all diagnostic messages (infos, warnings, errors) for a Lean file.

**Example Output Snippet:**
```
l20c42-l20c46, severity: 1
simp made no progress

l21c11-l21c45, severity: 1
function expected at
  h_empty
term has type
  T ∩ compl T = ∅
```

#### `lean_goal`

**Description:** Get the proof goal at a specific location (line or line & column) in a Lean file.

**Example Output Snippet (line):**
```
Before:
S : Type u_1
inst✝¹ : Fintype S
inst✝ : Nonempty S
P : Finset (Set S)
hPP : ∀ T ∈ P, ∀ U ∈ P, T ∩ U ≠ ∅
hPS : ¬∃ T ∉ P, ∀ U ∈ P, T ∩ U ≠ ∅
compl : Set S → Set S := fun T ↦ univ \ T
hcompl : ∀ T ∈ P, compl T ∉ P
all_subsets : Finset (Set S) := Finset.univ
h_comp_in_P : ∀ T ∉ P, compl T ∈ P
h_partition : ∀ (T : Set S), T ∈ P ∨ compl T ∈ P
⊢ P.card = 2 ^ (Fintype.card S - 1)

After:
no goals
```

#### `lean_term_goal`

**Description:** Get the term goal at a specific position (line & column) in a Lean file.

#### `lean_hover_info`

**Description:** Retrieve hover information (documentation) for symbols, terms, and expressions in a Lean file at a specific line & column.

**Example Output Snippet (hover info on a `sorry`):**
```
The `sorry` tactic is a temporary placeholder for an incomplete tactic proof, closing the main goal using `exact sorry`.

This is intended for stubbing-out incomplete parts of a proof while still having a syntactically correct proof skeleton. Lean will give a warning whenever a proof uses `sorry`, so you aren't likely to miss it, but you can double check if a theorem depends on `sorry` by looking for `sorryAx` in the output of the `#print axioms my_thm` command, the axiom used by the implementation of `sorry`.
```

#### `lean_declaration_file`

**Description:** Get the file contents where a symbol or term is declared.

#### `lean_completions`

**Description:** Code auto-completion: Find available identifiers or import suggestions at a specific position (line & column) in a Lean file.
```

--------------------------------

### Search Lean Definitions/Theorems (Loogle)

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Utilizes loogle.lean-lang.org to find Lean definitions and theorems. Queries can be based on constant names, lemma names, subexpressions, types, or conclusions. Results are returned as a JSON array of matching entries.

```json
[
  {
    "type": " (x : ℝ) : ℝ",
    "name": "Real.sin",
    "module": "Mathlib.Data.Complex.Trigonometric"
  }
]
```

--------------------------------

### Run Lean Code Snippet

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Executes an independent Lean code snippet or file. It returns the result of the execution or any error messages encountered. This is useful for testing small pieces of Lean code in isolation.

```Lean
#eval 5 * 7 + 3
```

--------------------------------

### Bearer Token Authentication

Source: https://github.com/ooo0ooo/lean-lsp-mcp/blob/main/README.md

Explains how to secure MCP server communication using bearer token authentication for streamable-http and sse transports. It covers setting the environment variable and client-side header configuration.

```APIDOC
## Bearer Token Authentication

### Description
Transport via `streamable-http` and `sse` supports bearer token authentication to restrict access to authorized clients.

### Setup
1. **Set Environment Variable:** Set the `LEAN_LSP_MCP_TOKEN` environment variable to your secret token before starting the server.
   ```bash
   export LEAN_LSP_MCP_TOKEN="your_secret_token"
   ```
2. **Start Server:** Run the Lean LSP MCP server with the desired transport.
   ```bash
   uvx lean-lsp-mcp --transport streamable-http
   ```

### Client Configuration
Clients should include the token in the `Authorization` header.
```
Authorization: Bearer your_secret_token
```
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.