How do I use axle-mcp?

1. Click on "Install Server". 2. Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state. 3. In the chat, type @ followed by the MCP server name and your instructions, e.g., "@axle-mcp repair the sorry statements in this Lean proof" That's it! The server will respond to your query, and you can continue using it as needed. Here is a step-by-step guide with screenshots.

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.