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+
mcpPython package (pip install mcp)- The
axleCLI 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 (runaxle_environmentsto list available ones)names— comma-separated declaration names to process (default: all)indices— comma-separated 0-based indices to processtimeout— 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.
