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

| Tool | Description | |------|-------------| | axle_environments | List available Lean environments (versions + Mathlib) | | axle_check | Validate Lean code and report errors/warnings/info | | axle_verify_proof | Check that a candidate proof matches a formal statement | | axle_extract_theorems | Split a file into one-theorem-per-unit with rich metadata | | axle_repair_proofs | Auto-repair broken proofs (replaces sorry with working tactics) | | axle_simplify_theorems | Remove redundant tactics and clean up proof steps | | axle_disprove | Find counterexamples to false theorems via property-based testing | | axle_theorem2sorry | Replace proof bodies with sorry (create problem templates) | | axle_have2sorry | Replace have proofs with sorry (targeted exercises) | | axle_sorry2lemma | Lift sorry placeholders into standalone top-level lemmas | | axle_have2lemma | Lift have statements into standalone top-level lemmas | | axle_theorem2lemma | Convert between theorem and lemma keywords | | axle_rename | Rename declarations and update all references | | axle_merge | Combine multiple Lean snippets into one file | | axle_normalize | Standardize Lean file formatting |

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

| Environment variable | Default | Description | |---------------------|---------|-------------| | AXLE_BIN | axle | Path to the axle binary | | AXLE_DEFAULT_ENVIRONMENT | lean-4.28.0 | Default Lean environment for all tools |

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.

MCP Servers