axiom-axle 1.3.0

Python client for AXLE (Axiom Lean Engine) API

AXLE

Axiom Lean Engine - Python client and CLI for the AXLE Lean verification API.

Homepage: https://axle.axiommath.ai/

Recent Announcements

June 3, 2026 - v1.3.0

Support for all declaration kinds, a reworked repair_proofs, link shortening, and broader MCP support. See the changelog for details and other changes.

Highlights:

• All declaration kinds: A new theorems_only option lets most tools select over every declaration kind — definitions, opaques, instances, and more — not just theorems and lemmas. Set it to false to opt in.
• Reworked repair_proofs: New passes, stacked repairs, and clearer messages for failed repairs.
• Tool updates: Changes and new options for verify_proof, merge, extract_decls, and sorry2lemma.
• Link shortening: Short, shareable links to requests.
• MCP web support: The axiom-axle-mcp server now works with Claude web, desktop, and mobile.

April 15, 2026 - v1.2.0

New extract_decls tool for extracting all declaration kinds, and corresponding updates to extract_theorems. Users using extract_theorems (which will be deprecated in a future update) should migrate to extract_decls. See the changelog for details.

April 8, 2026 - v1.1.1

Default option changes, a Lean version bump, and bug fixes.

Highlights:

• Default options changed: autoImplicit is now set to true by 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.

Past announcements

Documentation

• Installation Guide
• Python API Reference
• CLI Reference
• Examples

Past Announcements

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_messages has been removed from extract_theorems. To replicate old behavior, run the content field of the resulting documents through the check tool.
• 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 | [e-mail]