axiom-axle-mcp 0.1.0

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 at axle.axiommath.ai/app/console.

2. Add the MCP server to your client:

Claude Code:

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

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

Add the following to your client's MCP config file:

{
  "mcpServers": {
    "axle": {
      "command": "uvx",
      "args": ["axiom-axle-mcp"],
      "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.