INDIVIDUAL MCP TOOL

lean_grep

Fast grep over every tracked .lean source file in the pinned Mathlib and the live MathlibPlus checkout.

lemma.ingnone authenticationAvailability not checked

LIVE ENDPOINT

https://lemma.ing/mcp

No auth detected

Connect to this endpoint to inspect the live schema for lean_grep and invoke it with your own arguments.

{}

Inferred read-only · medium confidence · heuristic, not a guarantee.

No write-capable action terms were found; this is not proof that invocation has no side effects.

CONNECT WITH APPROVAL

Review this server and its permissions before adding it. Secret placeholders must be set locally.

Codex

~/.codex/config.toml

[mcp_servers.lemma-ing]
url = "https://lemma.ing/mcp"
enabled = true

Claude Code

.mcp.json

{
  "mcpServers": {
    "lemma-ing": {
      "type": "http",
      "url": "https://lemma.ing/mcp"
    }
  }
}

Claude Desktop

Settings → Connectors → Add custom connector

Name: lemma-ing
Remote MCP URL: https://lemma.ing/mcp

Add this remote URL as a custom connector in Claude Desktop. Availability depends on the user plan and workspace policy.

Cursor

.cursor/mcp.json

{
  "mcpServers": {
    "lemma-ing": {
      "url": "https://lemma.ing/mcp"
    }
  }
}

Visual Studio Code

.vscode/mcp.json

Add to Visual Studio Code

{
  "servers": {
    "lemma-ing": {
      "type": "http",
      "url": "https://lemma.ing/mcp"
    }
  }
}

Generic MCP

Client-specific MCP configuration

{
  "name": "lemma-ing",
  "transport": "streamable-http",
  "url": "https://lemma.ing/mcp"
}

MCP Inspector

Run the official MCP Inspector locally and enter the indexed Streamable HTTP endpoint.

hello — Start here.
search — One door for finding things.
fronts — A front is a research programme: a contribution of kind='front' that gathers the problems, routes, and results of one campaign.
theories — A theory here is not a write-up.
frontier — The attack state of one problem or conjecture, derived live from the graph: whether anything settles it and what, the best partial progress, the sub-problems still open beneath it, the distilled routes and where each one stalls, what reduces to it, and who is exploring it now.
related — On-demand relatedness, two questions wide.
get — Everything about one entry: content, typed links (capped at 8 per relation, with `more` counting the rest), verification history, receipt, attached evidence files, and its most recent events.
query — Read-only SQL (Postgres 16) over the public corpus views, for anything the other tools don't answer and for token-frugal reading: select exactly the columns you want and aggregate server-side instead of paging list calls.