Skip to content

Quick Start

Try AXLE in your browser with the interactive demo notebook.

MCP Server

The axiom-axle-mcp package wraps AXLE as a Model Context Protocol server, so an AI agent can call check, verify_proof, extract_theorems, and the rest of AXLE's tools directly.

Supported clients include:

  • Claude Code, Cursor, Windsurf, VS Code, Cline, and other editors that speak MCP — point them at the axiom-axle-mcp package locally.
  • Claude web, desktop, and mobile — connect to the hosted server at https://mcp.axiommath.ai/mcp under Settings > Connectors.

See the PyPI page for detailed installation and config instructions.

Prerequisites

Before using AXLE, set your API key:

export AXLE_API_KEY=your-api-key

See Configuration for more details.

Basic Usage

Check Lean Code

The simplest operation is checking if Lean code is valid:

Python

import asyncio
from axle import AxleClient

async def main():
    async with AxleClient() as client:
        result = await client.check(
            content="import Mathlib\ntheorem citation_needed : 1 + 1 = 2 := by decide",
            environment="lean-4.28.0",
        )
        print(f"Valid: {result.okay}")
        if result.lean_messages.errors:
            print("Errors:", result.lean_messages.errors)

asyncio.run(main())

CLI

# From file
axle check mytheorem.lean --environment lean-4.28.0

# From stdin
echo "def meaning_of_life := 42\n#print meaning_of_life" | axle check - --environment lean-4.28.0

HTTP API

curl -s -X POST https://axle.axiommath.ai/api/v1/check \
    -H "Authorization: Bearer $AXLE_API_KEY" \
    -H "Content-Type: application/json" \
    -d '{"content": "import Mathlib\ntheorem citation_needed : 1 + 1 = 2 := by decide", "environment": "lean-4.28.0"}' | jq

Next Steps