axiom-axle-mcp 0.1.5

MCP server for Axiom Lean Engine (AXLE) — exposes Lean verification tools to Claude Code and other MCP clients

AXLE MCP Server

A Model Context Protocol server for Axiom Lean Engine — exposes Lean verification and manipulation tools to AI agents.

Setup

1. Create a free API key: https://axle.axiommath.ai/app/console.

2. Add the MCP server to your client:

Claude Code:

Replace your_api_key_here with the API key you created in step 1:

claude mcp add axle -e AXLE_API_KEY=your_api_key_here -- uvx --from axiom-axle-mcp axle-mcp-server

Other MCP clients (Cursor, Windsurf, Claude Desktop, VS Code, Cline, etc.):

Add the following to your client's MCP config file. Replace your_api_key_here with the API key you created in step 1:

{
  "mcpServers": {
    "axle": {
      "command": "uvx",
      "args": ["--from", "axiom-axle-mcp", "axle-mcp-server"],
      "env": {
        "AXLE_API_KEY": "your_api_key_here"
      }
    }
  }
}

Usage

With the MCP server installed, agents can check and fix Lean code directly:

You: Can you check if this proof compiles?

theorem add_comm (a b : Nat) : a + b = b + a := by
  ring

Ask your agent what AXLE MCP can do.