Axiom Lean 4 Proof Verification

Axiom provides cloud-based Lean 4 proof verification through the Axle API. It compiles and checks Lean code against a full Mathlib environment without requiring a local Lean installation -- verification results come back in seconds rather than the minutes it takes to build locally.

Before First Use

Check these once per session before running any Axle commands:

1. API key: Run echo $AXLE_API_KEY. If empty, the user needs to get a key from axle.axiommath.ai/app/console and set it: export AXLE_API_KEY=<key>.
2. CLI installed: Run axle --version. If not found, install with pip install axiom-axle.
3. Lean environment: Check for a lean-toolchain file in the project root to detect the Lean version. If present, use its version (e.g., leanprover/lean4:v4.28.0 becomes lean-4.28.0). If absent, default to lean-4.28.0.

Reference Files

Read these as needed based on the task: