Axiom Lean Engine

Axiom Lean Engine is an open-source Python client and command-line interface for AxiomMath's cloud-based Lean 4 theorem proving and verification API. It provides tools for checking formal proofs, analyzing proof states, and manipulating mathematical declarations. Researchers can verify theorems, extract declarations, simplify formal statements, and repair incomplete proofs. The engine supports bulk proof analysis and optimized execution through cached Lean environments. It also provides utilities for merging proofs, examining errors, and testing mathematical conjectures. Its Model Context Protocol integration enables AI coding assistants and automated theorem provers to access verification tools. AXLE supports configurable Lean environments and mathematical libraries, making it useful for formal mathematics and AI-assisted proof research.