Koskamo

LeanWarp MCP

LeanWarp is a hosted Lean 4 API for proof agents that checks and verifies Lean 4 proofs with Mathlib already loaded. It allows agents to inspect goals, try tactics, and verify proofs against exact statements using commands like check, inspect, try-tactics, and verify.

Visit Isagoge Labs

Package and access

Local package with source-attributed installation metadata. Koskamo does not execute packages during review.

LeanWarp MCP logo, by Isagoge LabsCommunity listingLocal stdioSource reviewed; not executedPublished by Isagoge Labs
You need:Create an API key
Vendor documentation

What you can do with it

  • Check and verify Lean 4 proofs on hosted workers
  • Inspect proof goals and local context
  • Try tactics on open goals without editing files
  • Verify proofs against intended statements

Source and maintenance

Community listingRegistry 0.2.5
mcp-registry: io.github.Isagoge-Labs/leanwarp@0.2.5Source repositoryProject website
Maintenance checked

Packages and installation

Source-provided package data. Koskamo has not executed or live-probed this package.

leanwarp 0.2.5

pypiuvx
leanwarp package definition
{
  "version": "0.2.5",
  "transport": "stdio",
  "identifier": "leanwarp",
  "runtimeHint": "uvx",
  "registryType": "pypi",
  "registryBaseUrl": "https://pypi.org",
  "packageArguments": [
    {
      "name": "--project",
      "type": "named",
      "format": "filepath",
      "isRequired": true,
      "description": "Absolute path to the Lean project directory to check."
    },
    {
      "type": "positional",
      "value": "mcp"
    }
  ],
  "environmentVariables": [
    {
      "name": "LEANWARP_API_KEY",
      "format": "string",
      "isRequired": true,
      "description": "Your LeanWarp API key (lw_live_...), from https://isagoge.in/dashboard?section=keys."
    }
  ]
}

Tools

Reported by the attributed source; not independently observed by Koskamo.

No tool definitions available.

Connect from your client

Each snippet configures the same source-provided package; replace placeholders before use.

This server is operated by the named third party. Listing and endpoint checks are not an endorsement or a security audit. Review the operator's permissions, terms, and data handling before connecting. How listings are checked and corrected.

Cursor

Merge this local stdio configuration, replace every placeholder environment value, and restart Cursor. Koskamo has not executed this package.
Cursor configuration
{
  "mcpServers": {
    "leanwarp-mcp": {
      "command": "uvx",
      "args": [
        "leanwarp==0.2.5",
        "mcp"
      ],
      "env": {
        "LEANWARP_API_KEY": "<YOUR_LEANWARP_API_KEY>"
      }
    }
  }
}

Cline

Merge this local stdio configuration, replace every placeholder environment value, and restart Cline. Koskamo has not executed this package.
Cline configuration
{
  "mcpServers": {
    "leanwarp-mcp": {
      "command": "uvx",
      "args": [
        "leanwarp==0.2.5",
        "mcp"
      ],
      "env": {
        "LEANWARP_API_KEY": "<YOUR_LEANWARP_API_KEY>"
      }
    }
  }
}

VS Code

Merge this local stdio configuration, replace every placeholder environment value, and restart VS Code. Koskamo has not executed this package.
VS Code configuration
{
  "servers": {
    "leanwarp-mcp": {
      "type": "stdio",
      "command": "uvx",
      "args": [
        "leanwarp==0.2.5",
        "mcp"
      ],
      "env": {
        "LEANWARP_API_KEY": "<YOUR_LEANWARP_API_KEY>"
      }
    }
  }
}

Claude Desktop

Merge this local stdio configuration, replace every placeholder environment value, and restart Claude Desktop. Koskamo has not executed this package.
Claude Desktop configuration
{
  "mcpServers": {
    "leanwarp-mcp": {
      "command": "uvx",
      "args": [
        "leanwarp==0.2.5",
        "mcp"
      ],
      "env": {
        "LEANWARP_API_KEY": "<YOUR_LEANWARP_API_KEY>"
      }
    }
  }
}

Let your agent find its tools

Find servers like LeanWarp MCP from your agent. Add Koskamo once to search the index for endpoints, access requirements, and client setup. Public discovery needs no key.

Connect Koskamo Explore workflows
See all 8,850