Releasing AXLE | Axiom
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.
Axiom Lean Engine
User: axle.axiommath.ai API Endpoint
Worker: "Is this proof correct?"
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).
AXLE is now available as a free service
Interactive sandbox
Test verify_proof, extract theorems, and experiment with proof transformations in seconds.
AXLE API
Integrate verify_proof, extract_theorems, and scalable proof infrastructure into your own systems.
Need higher capacity or production access? Submit our API capacity interest form
Entry editors AXLE TEAM
Alex Schneidman
Jimmy Xin
Chris Cummins
Latest from the Territory
The Address Before the Room
One family is a third the size of the other — but that third is a doorway, not the matching that has to be built behind it.
The Same Ground
In the right coordinate, Kaprekar's process is not a different puzzle in every base — it is one operation: doubling.
The Figure and the Remainder
A multiplicity that reads as the blur of cancellation comes into focus, in natural families, as an exact count of bounded Dyck-path structures.
The Reveal
In the hardest window for lattice triangles, a density-1 result rules out almost every candidate.
Releasing AXLE