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 1 concurrent active request.

To obtain an API key, visit axle.axiommath.ai/app/console

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¶

Variable	Default	Description
`AXLE_API_KEY`	—	API key for authentication
`AXLE_API_URL`	`http://10.1.10.100:8989`	API server URL
`AXLE_TIMEOUT_SECONDS`	`1_800`	Base timeout in seconds for retry window if service is temporarily unavailable
`AXLE_MAX_CONCURRENCY`	`20`	Max concurrent requests

Example¶

export AXLE_API_KEY=your-api-key
export AXLE_API_URL=http://10.1.10.100:8989
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.STAGING_URL,
    base_timeout_seconds=600,
    max_concurrency=50,
)

If api_key is not passed to the constructor, the client reads from the AXLE_API_KEY environment variable.

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 http://10.1.10.100:8989 check file.lean --environment lean-4.26.0

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

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

API Endpoints¶

Environment	URL
Production	`http://10.1.10.100:8989`
Staging	`http://10.1.10.100:8989`

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.26.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 http://10.1.10.100:8989/v1/environments | jq

Environment Response Format¶

Each environment includes the following fields:

Field	Type	Description
`name`	`str`	Environment identifier to use in requests (e.g., `"lean-4.26.0"`)
`lean_toolchain`	`str`	Lean toolchain version (e.g., `"leanprover/lean4:v4.26.0"`)
`repo_url`	`str \| null`	Git repository URL for custom environments
`revision`	`str \| null`	Git revision/commit hash for custom environments
`subdir`	`str \| null`	Subdirectory within the repository
`imports`	`str`	Default imports available (e.g., `"import Mathlib"`)
`description`	`str`	Human-readable description

Example Environments¶

[
  {
    "name": "lean-4.21.0",
    "lean_toolchain": "leanprover/lean4:v4.21.0",
    "imports": "import Mathlib",
    "description": "Lean 4.21.0 with Mathlib"
  },
  {
    "name": "pnt-4.26.0",
    "lean_toolchain": "leanprover/lean4:v4.26.0",
    "repo_url": "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd",
    "revision": "d24e98e2384cd191486517bfca980576772f6c17",
    "imports": "import Mathlib\nimport PrimeNumberTheoremAnd",
    "description": "Lean + Mathlib version 4.26.0 with Terence Tao's Prime Number Theorem Project"
  }
]

Limitations¶

Header Handling¶

All requests to AXLE are assumed to have the same header (import statements), which is derived from the imports field of the environment. You can discover the expected imports for any environment by querying the environments endpoint.

By default, if your code includes a different header than the environment expects, AXLE will raise a user error. This strict behavior ensures you are aware of any import mismatches that could lead to unexpected results.

If you want AXLE to automatically replace mismatched imports with the environment's default header, set ignore_imports=True in your request. When enabled, AXLE will: 1. Log a warning about the import mismatch 2. Replace your code's import statements with the environment's default imports 3. Return the modified code in the content field of the response

Note that behavior may be inconsistent if the header in your code does not match the environment's expected header.

AXLE Scope¶

AXLE was designed with simple imports, theorems, and definitions in mind. While we attempt to support other Lean commands and constructs (other declaration types, open commands, section/namespace blocks, etc.), and attempt to fail fast on them with the normalize tool, we make no guarantees about stability when using AXLE with these constructs.