Configuration

AXLE can be configured via environment variables or constructor arguments.

Authentication

AXLE uses API key authentication for active request rate limiting. Requests without an API key are limited to 10 concurrent active requests.

To obtain an API key, visit axle.axiommath.ai/app/console. If you need higher rate limits, you can request more capacity.

Setting Your API Key

The recommended way to configure your API key is via the AXLE_API_KEY environment variable:

export AXLE_API_KEY=your-api-key

You can also pass it directly when creating the client (see Python Configuration below).

Environment Variables

Example

export AXLE_API_KEY=your-api-key
export AXLE_API_URL=https://axle.axiommath.ai
export AXLE_TIMEOUT_SECONDS=600
export AXLE_MAX_CONCURRENCY=50

Python Configuration

Constructor Arguments

from axle import AxleClient

# API key from environment variable (recommended)
client = AxleClient()

# Explicit API key
client = AxleClient(api_key="your-api-key")

# Custom URL, timeout, and concurrency
client = AxleClient(
    api_key="your-api-key",
    url=AxleClient.DEFAULT_URL,
    base_timeout_seconds=600,
    max_concurrency=50,
)

All constructor arguments fall back to environment variables if not provided.

CLI Configuration

The CLI reads the AXLE_API_KEY environment variable automatically. Set it before running CLI commands:

export AXLE_API_KEY=your-api-key

Global Options

# Custom API URL
axle --url https://axle.axiommath.ai check file.lean --environment lean-4.28.0

# JSON output
axle --json check file.lean --environment lean-4.28.0

# Output to file
axle theorem2sorry input.lean --environment lean-4.28.0 -o output.lean

Lean Environments

AXLE supports multiple Lean environments, each containing a specific Lean version and set of dependencies (e.g., Mathlib). Every API request requires an environment parameter specifying which environment to use. To get started, we recommend using the latest Lean + Mathlib version, which at the time of writing is packaged in lean-4.28.0.

Discovering Available Environments

You can query the available environments using any access method:

Python

import asyncio
from axle import AxleClient

async def main():
    async with AxleClient() as client:
        environments = await client.environments()
        for env in environments:
            print(f"{env.name}: {env.description}")

asyncio.run(main())

CLI

axle environments

HTTP API

curl -s -H "Authorization: Bearer $AXLE_API_KEY" https://axle.axiommath.ai/v1/environments | jq

The Authorization header is required for all requests.

Environment Response Format

Each environment includes the following fields:

Example Environments

[\
  {\
    "name": "lean-4.21.0",\
    "lean_toolchain": "leanprover/lean4:v4.21.0",\
    "imports": "import Mathlib",\
    "description": "Lean 4.21.0 with Mathlib"\
  }]

See Import Mismatches for important notes on how AXLE handles import statements.