Changelog

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

[Releases]

v1.5.0 - July 15, 2026

Added

• Added LeanResourceExceeded and LeanTimeout exceptions. The Lean worker exceeding its memory cap or time budget now raises a distinct, non-retryable exception instead of the generic AxleRuntimeError, so callers can record it as a deterministic outcome rather than retrying.
• check, extract_decls, and extract_theorems now accept optional names and indices arguments to select which declarations to process. The returned documents / messages are restricted to them, and elaboration is skipped for the proofs of unselected declarations. This is a speed feature and should be used when elaborating the whole file is too slow. Note that this changes the behavior of the tool: the returned Lean messages will be incomplete, and the per-document content field for extract_decls and extract_theorems is returned empty. See the check and extract_decls pages for more details. Regular users with no speed concerns can disregard these options.
• extract_decls documents now include an unfolded_type_hash field: the type hash after unfolding module-local elaboration auxiliaries. This way, types differing only by such an auto-generated name deduplicate where type_hash would not. See the extract_decls page for details. The behavior of the base type_hash field is unchanged.
• verify_proof now accepts a verify_negation option (default false). When set, verify_proof additionally checks whether content proves the negation of formal_statement and reports the result in a new negation field, which carries the same okay, tool_messages, and failed_declarations as the top-level result. The field is omitted unless verify_negation is set. Regular users can ignore this option.
• disprove and extract_decls now accept a verbosity parameter (0=default, 1=robust, 2=extra robust), affecting the pretty-printed types output by the tools. Higher verbosity levels make the pretty-printer more explicit, which helps when the default output re-elaborates ambiguously.
• Added AxleClient.get_latest_environment(), which fetches the available Lean+Mathlib environments and returns the latest one.
• Added instructions for citing AXLE in the documentation. See Citing AXLE.
• Added Lean 4.32.0 support.

Fixed

• Fixed a bug in tools that analyze term-mode goals causing goal extraction to silently fail with include_whole_context=false. For example, this request failed in previous versions, leaving the content unchanged.
• verify_proof is now module-aware. Previously, module dependencies would be treated as disallowed axioms when not using the default header.

Changed

• Various tools now skip proof elaboration for unselected declarations when names or indices is provided. This is a speed change; however, any outputs pertaining to the unselected declarations are unreliable and should not be used.

v1.4.0 - July 1, 2026

AXLE will be presented at the 3rd AI for Math Workshop at ICML 2026 as a contributed talk! Read the technical report on arXiv.

Changed

• ignore_imports now defaults to true. When your code's imports don't match the environment's default header, AXLE substitutes the default header instead of raising an error. See Import Mismatches for details.
• Reworked the tool_messages and okay fields for a few tools. See Interpreting the okay field for details.

Added

• Added Lean 4.30.0 and 4.31.0 support.
• Added a relax_defeq_transparency repair pass to repair_proofs. On environments without the option, the repair is a no-op.
• extract_decls and extract_theorems report four new per-declaration fields: type_depth, term_depth, wall_ms, and heartbeats. See the extract_decls page for more details.

Removed

• Removed the http2 parameter from the AxleClient constructor, which was slowing the client down.

Fixed

• Fixed extract_decls bug for opaques where value dependencies were misclassified as type dependencies.

v1.3.0 - June 3, 2026

Added

• Added link shortening to the gateway. Try it out: https://axle.axiommath.ai/check#r=7d70453f-813f-4d19-8de9-44793dafa835.
• Added Claude web, desktop, and mobile support to the axiom-axle-mcp MCP server via a hosted endpoint. See the Quick Start for details.

Changed

• Added a new option theorems_only (default true) to all tools that select over theorems/lemmas. These tools can now select over all declaration kinds.

Fixed

• Added faster, more graceful retries on certain classes of connection errors. Minor change.

v1.2.1 - April 29, 2026

Deprecated

• extract_theorems has been deprecated and will no longer be updated. Please use extract_decls instead.

Changed

• The AXLE client now uses HTTP/2 by default. Users may set the http2 parameter to false in the client constructor to revert back to HTTP/1.1.

Added

• Added a new option expand_scoped_notations to the normalize tool.

Fixed

• Fixed a bug in the executors causing requests to hang, occasionally resulting in abnormally high latencies.

v1.2.0 - April 15, 2026

Added

• Added two new fields in extract_theorems to be consistent with extract_decls.
• Added extract_decls, an upgraded version of extract_theorems that extracts all declaration kinds.

Fixed

• Added "Last Used" and "Requests (24h)" columns to the API key console page for better visibility into API key usage.

v1.1.1 - April 8, 2026

Changed

• [!] We are turning on the autoImplicit and turning off the pp.unicode.fun Lean options. AXLE will now automatically insert implicit variables when they are missing.
• [!] We have renamed mathlib_linter to mathlib_options.

Added

• Added Lean 4.29.0 support.
• Added support for glob patterns in the permitted_sorries field for verify_proof.

Fixed

• Fixed a bug causing timeouts to be capped at 10 minutes.

v1.1.0 - April 1, 2026

Changed

• [!] Removed document_messages from the response of extract_theorems.
• [!] includeEndPos has been turned on for Lean messages.

Fixed

• Removed redundant parsing resulting in occasional speedups in repair_proofs, normalize, etc.

v1.0.2 - March 18, 2026

Added

• Added explicit okay return value to repair_proofs

Changed

• Improved error messages for unknown options in simplify_theorems, repair_proofs, normalize.

v1.0.1 - March 11, 2026

Added

• Added Changelog and Troubleshooting to the documentation pages.

Fixed

• Increased request limits and fixed a typo in the documentation.

v1.0.0 - March 4, 2026

Added

• Initial release of AXLE Python client
• Async client (AxleClient) with all 14 API tools:
  • verify_proof
  • check
  • extract_theorems
  • rename
  • theorem2lemma
  • theorem2sorry
  • merge
  • simplify_theorems
  • repair_proofs
  • have2lemma
  • have2sorry
  • sorry2lemma
  • disprove
  • normalize
• CLI tool with commands for all tools
• Helper functions for string manipulation
• Configuration via environment variables
• Type hints and PEP 561 compliance
• Comprehensive documentation