Python client for AXLE (Axiom Lean Engine) API
Project description
AXLE
Axiom Lean Engine - Python client and CLI for the AXLE Lean verification API.
Homepage: https://axle.axiommath.ai/
Announcements
April 8, 2026 - v1.1.1
Default option changes, a Lean version bump, and bug fixes.
Highlights:
- Default options changed:
autoImplicitis now set totrueby default, matching standard Lean behavior. - Lean 4.29.0: Added the latest stable Lean release.
- Timeout bug fix: Fixed a bug where requests were prematurely preempted. Requests now properly max out at the 15-minute maximum timeout.
See the changelog for details and other changes.
April 1, 2026 - v1.1.0
🎉 After mass feedback from the public, we're excited to announce that AXLE is switching from Lean to Rocq. The new name will be AXRE (Axiom Rocq Engine). All existing Lean proofs will be automatically translated using GPT-2. 🚀
Notable API changes:
document_messageshas been removed fromextract_theorems. To replicate old behavior, run thecontentfield of the resulting documents through thechecktool.- Lean messages now include end positions across all tools, changing the format from
-:4:38: ...to-:4:38-4:43: ....
Performance improvements:
- Reworked the Lean worker pool for faster responses, no environment warm-up time, and more secure containers.
- Improved the worker scaling pipeline to decrease delays when all worker slots are busy or offline. In the worst case, users should expect no more than a 2-3 minute delay before more worker capacity spins up.
See the changelog for details and other changes.
March 11, 2026 - v1.0.1
New documentation pages, increased rate limits, and bug fixes. See the changelog for details.
March 6, 2026
Lean Zulip Thread
Join the discussion, ask questions, and share feedback on the Lean Zulip.
Higher Rate Limits
Rate limits were unintentionally too restrictive:
- API key users: increased to 20 active requests (up from 4)
- Anonymous users: increased to 10 active requests (up from 1)
- Max timeout: increased to 15 minutes (up from 5 minutes)
Users with an API key should regenerate their key to apply the new limits.
March 5, 2026 - v1.0.0
AXLE Public Release
We're excited to release AXLE to the public! AXLE provides proof verification and manipulation primitives we've used across all of our research efforts, including training AI models and AxiomProver's 12/12 on Putnam 2025.
Playground | API docs | Why we built AXLE | Request more capacity | axle@axiommath.ai
Documentation
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Filter files by name, interpreter, ABI, and platform.
If you're not sure about the file name format, learn more about wheel file names.
Copy a direct link to the current filters
File details
Details for the file axiom_axle-1.1.1.tar.gz.
File metadata
- Download URL: axiom_axle-1.1.1.tar.gz
- Upload date:
- Size: 37.9 kB
- Tags: Source
- Uploaded using Trusted Publishing? Yes
- Uploaded via: twine/6.1.0 CPython/3.13.12
File hashes
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 |
dc906845a3afb12b02792c50b494900978a63aa29d2e47c113a02172eb7ec9d5
|
|
| MD5 |
01069015ea8483377d83b9def0b91012
|
|
| BLAKE2b-256 |
09ce0d15879d1f1023a0f607ea86d3e796fef908770ebc8ac5ee76762247c945
|
Provenance
The following attestation bundles were made for axiom_axle-1.1.1.tar.gz:
Publisher:
publish-pypi.yml on AxiomMath/axiom-lean-engine
-
Statement:
-
Statement type:
https://in-toto.io/Statement/v1 -
Predicate type:
https://docs.pypi.org/attestations/publish/v1 -
Subject name:
axiom_axle-1.1.1.tar.gz -
Subject digest:
dc906845a3afb12b02792c50b494900978a63aa29d2e47c113a02172eb7ec9d5 - Sigstore transparency entry: 1256246009
- Sigstore integration time:
-
Permalink:
AxiomMath/axiom-lean-engine@c8b3fa239e74f0d29d6c80018758e68ef190b5a5 -
Branch / Tag:
refs/tags/v1.1.1 - Owner: https://github.com/AxiomMath
-
Access:
public
-
Token Issuer:
https://token.actions.githubusercontent.com -
Runner Environment:
github-hosted -
Publication workflow:
publish-pypi.yml@c8b3fa239e74f0d29d6c80018758e68ef190b5a5 -
Trigger Event:
release
-
Statement type:
File details
Details for the file axiom_axle-1.1.1-py3-none-any.whl.
File metadata
- Download URL: axiom_axle-1.1.1-py3-none-any.whl
- Upload date:
- Size: 39.5 kB
- Tags: Python 3
- Uploaded using Trusted Publishing? Yes
- Uploaded via: twine/6.1.0 CPython/3.13.12
File hashes
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 |
2e795fb2fa25c41d742342777bf6a64e699eb46f4c847d0e4cb33b186e3312eb
|
|
| MD5 |
30981c82ab467ef8506d343b05ef0421
|
|
| BLAKE2b-256 |
d36f3de736ec61b35f9f7fafe96425d329fd82896129f57243beff39e6d076b0
|
Provenance
The following attestation bundles were made for axiom_axle-1.1.1-py3-none-any.whl:
Publisher:
publish-pypi.yml on AxiomMath/axiom-lean-engine
-
Statement:
-
Statement type:
https://in-toto.io/Statement/v1 -
Predicate type:
https://docs.pypi.org/attestations/publish/v1 -
Subject name:
axiom_axle-1.1.1-py3-none-any.whl -
Subject digest:
2e795fb2fa25c41d742342777bf6a64e699eb46f4c847d0e4cb33b186e3312eb - Sigstore transparency entry: 1256246108
- Sigstore integration time:
-
Permalink:
AxiomMath/axiom-lean-engine@c8b3fa239e74f0d29d6c80018758e68ef190b5a5 -
Branch / Tag:
refs/tags/v1.1.1 - Owner: https://github.com/AxiomMath
-
Access:
public
-
Token Issuer:
https://token.actions.githubusercontent.com -
Runner Environment:
github-hosted -
Publication workflow:
publish-pypi.yml@c8b3fa239e74f0d29d6c80018758e68ef190b5a5 -
Trigger Event:
release
-
Statement type: