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.

[Open AXLE Playground](https://axle.axiommath.ai/)

### AXLE API

Integrate verify_proof, extract_theorems, and scalable proof infrastructure into your own systems.

[View API Docs](https://axle.axiommath.ai/v1/docs/)

Need higher capacity or production access? Submit our [API capacity interest form](https://docs.google.com/forms/d/1MFj9n5CsaulwjH2vkb-FwyfCmvYvLawcA4zglBVeO5A/edit)

## Entry editors AXLE TEAM

### Alex Schneidman

### Jimmy Xin

### Chris Cummins

## Latest from the Territory

[View All Entries](/content/territory/index.html)

**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.

[View All Entries](/content/territory/index.html)

Releasing AXLE