Skip to content

AXLE - Axiom Lean Engine

Proof manipulation as infrastructure, not an afterthought

AXLE is a set of Lean utilities for theorem proving: validating candidate proofs, splitting theorems from larger files, converting proofs to sorry, and more. They are written as Lean metaprograms to be robust.

Features

  • Proof Verification: Validate proofs against formal statements
  • Code Analysis: Check Lean code for errors and extract theorems
  • Code Transformation: Rename declarations, convert keywords, simplify proofs

Usage Methods

AXLE can be accessed through:

  1. Web Interface - Interactive UI at http://10.1.10.100:8989/
  2. Python API - pip install axle
  3. CLI - axle verify-proof, axle check, etc.
  4. HTTP API - Direct REST calls with curl

Authentication

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

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

export AXLE_API_KEY=your-api-key

See Configuration for details.

Quick Example

Python

import asyncio
from axle import AxleClient

async def main():
    async with AxleClient() as client:
        result = await client.verify_proof(
            formal_statement="import Mathlib\ntheorem citation_needed : 1 = 1 := by sorry",
            content="import Mathlib\ntheorem citation_needed : 1 = 1 := rfl",
            environment="lean-4.26.0",
        )
        print(f"Valid: {result.okay}")

asyncio.run(main())

CLI

axle check myfile.lean --environment lean-4.26.0
axle verify-proof statement.lean proof.lean --environment lean-4.26.0

HTTP API

curl -s -X POST http://10.1.10.100:8989/v1/axle/check \
    -H "Authorization: Bearer $AXLE_API_KEY" \
    -d '{"content": "import Mathlib\n#eval 2+2", "environment": "lean-4.26.0"}' | jq

Available Endpoints

Endpoint Description
verify_proof Validate a proof against a formal statement
check Check Lean code for errors
extract_theorems Split file into individual theorems with dependencies
rename Rename declarations
theorem2lemma Convert between theorem and lemma keywords
theorem2sorry Strip proofs from theorems
merge Combine multiple Lean files
simplify_theorems Simplify theorem proofs
repair_proofs Attempt to repair broken proofs
have2lemma Extract have statements to standalone lemmas
have2sorry Replace have statements with sorry
sorry2lemma Extract sorry and errors to standalone lemmas
disprove Attempt to disprove theorems
normalize Standardize Lean formatting
comparator Thorough proof validation using external tool

See endpoints documentation for detailed parameters and response fields.

Submitting Issues

If you encounter bugs, unexpected behavior, or have feature requests, please submit an issue on GitHub:

https://github.com/AxiomMath/axiom-lean-engine/issues