Axle MCP Server

axle-mcp

An MCP server that exposes the AXLE (Axiom Lean Engine) CLI as tools for AI assistants like Claude.

AXLE is a remote API for Lean 4 proof engineering — it can check, repair, simplify, extract, and transform Lean theorems without requiring a local Lean installation.

Tools

Requirements

• Python 3.11+
• `mcp` Python package (pip install mcp)
• The axle CLI installed and accessible

Installation

1. Install dependencies

pip install mcp

2. Clone this repo

git clone https://github.com/Vilin97/axle-mcp
cd axle-mcp

3. Register with Claude Code

claude mcp add axle -s user \
  -e AXLE_BIN=/path/to/axle \
  -e AXLE_DEFAULT_ENVIRONMENT=lean-4.28.0 \
  -- python /path/to/axle-mcp/server.py

4. Register with Claude Desktop

Add to your claude_desktop_config.json:

{
  "mcpServers": {
    "axle": {
      "command": "python",
      "args": ["/path/to/axle-mcp/server.py"],
      "env": {
        "AXLE_BIN": "/path/to/axle",
        "AXLE_DEFAULT_ENVIRONMENT": "lean-4.28.0"
      }
    }
  }
}

Configuration

Usage examples

Once registered, Claude can use these tools directly. Some examples of what you can ask:

• "Check if this Lean theorem compiles" → axle_check
• "Repair the sorry'd proofs in this file" → axle_repair_proofs
• "Turn this proof into a problem set by replacing proofs with sorry" → axle_theorem2sorry
• "Does this theorem have a counterexample?" → axle_disprove
• "Extract each theorem into its own self-contained snippet" → axle_extract_theorems
• "Merge these two Lean files into one" → axle_merge

Common parameters

Most tools accept these optional parameters:

• environment — Lean environment to use (run axle_environments to list available ones)
• names — comma-separated declaration names to process (default: all)
• indices — comma-separated 0-based indices to process
• timeout — max execution time in seconds (default: 120)
• ignore_imports — ignore import mismatches between the code and the environment

How it works

Each MCP tool wraps the corresponding axle CLI command, passing Lean source code via stdin and returning the structured JSON response from the AXLE API. Tools that require multiple file arguments (verify-proof, merge) write temporary files automatically and clean them up after the call.