We’re excited to release the Axiom Lean Engine (AXLE) to the public. As AI systems tackle increasingly complex mathematical problems, having reliable, scalable infrastructure for proof verification is becoming essential. AXLE provides a suite of proof verification and manipulation primitives we’ve leveraged across all of our research efforts. It has empowered our researchers to train new models, explore novel frameworks for proof generation, and deploy our internal mathematical reasoning engine to solve real world problems.
As the scope of our work expanded in the last 6 months, we built a hosted service that
Provides safe proof verification faster than existing tools
Provides flexible, robust proof manipulation utilities that respect our strict requirements for correctness and trust.
Simplifies the integration of the Lean runtime into reasoning engines.
AXLE is a managed service providing these primitives at scale, including verify_proof, extract_theorems, and others which are crucial for effectively running Lean-based reasoning engines. This enables anyone to explore proof generation techniques without needing to worry about deploying Lean.
AXLE has already served millions of requests internally at Axiom:
For training our in-house AI models.
During AxiomProver’s 12/12 achievement on the Putnam 2025 exam.
In solving open research conjectures, including (Fel, Partial Vandiver, etc).