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 https://axle.axiommath.ai/
  2. Python API - pip install axiom-axle (Python API Reference)
  3. CLI - axle verify-proof, axle check, etc. (CLI Reference)
  4. HTTP API - Direct REST calls with curl

See the Quick Start tutorial for examples of each method.

Available Tools

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

See tools documentation for detailed parameters and response fields.

Public Deployments

AXLE's public deployment follows a weekly release schedule:

  • Maintenance Window: Every Wednesday at 10:00 AM Pacific Time
  • Expected Downtime: Brief interruption (typically under 5 minutes) during restart
  • Updates: New features, bug fixes, and improvements deployed weekly

After each deployment, the changelog is updated with details on what changed.

Submitting Issues

If you encounter bugs, unexpected behavior, or have feature requests:

FILE A BUG

Resources