Skip to content

Quick Start

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.26.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.26.0

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

Next Steps