# Changelog All notable changes to this project will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ## [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`](https://axle.axiommath.ai/v1/docs/tools/check) and [`extract_decls`](https://axle.axiommath.ai/v1/docs/tools/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](https://axle.axiommath.ai/v1/docs/tools/extract_decls) 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](https://axle.axiommath.ai/v1/docs/#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](https://axle.axiommath.ai/sorry2lemma#r=604f708c-99f1-49f0-9c4a-dd987d2ad024) 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](https://arxiv.org/abs/2606.26442). ### 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](https://axle.axiommath.ai/v1/docs/troubleshooting/#import-mismatches) for details. - Reworked the `tool_messages` and `okay` fields for a few tools. See [Interpreting the `okay` field](https://axle.axiommath.ai/v1/docs/troubleshooting/#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](https://axle.axiommath.ai/v1/docs/tools/extract_decls) 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](https://axle.axiommath.ai/check#r=7d70453f-813f-4d19-8de9-44793dafa835). - Added Claude web, desktop, and mobile support to the [`axiom-axle-mcp`](https://pypi.org/project/axiom-axle-mcp/) MCP server via a hosted endpoint. See the [Quick Start](https://axle.axiommath.ai/v1/docs/quickstart/#mcp-server) 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](https://axle.axiommath.ai/v1/docs/changelog/) and [Troubleshooting](https://axle.axiommath.ai/v1/docs/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