Axiom Lean Engine Files

This update reworks how global Lean options are handled in the (new) global_options, delab_options, mathlib_options, and verbosity fields. It also comes with new machine-readable docs endpoints under /v1/docs, which the MCP server uses to pull instructions for tools before using them.

Removed

• Removed Lean 4.32.0 due to a kernel soundness bug in Lean and replaced with Lean 4.32.2, which patches the bug. Note that although we only remove Lean 4.32.0, this bug affects all prior versions as well.

Added

• Added Lean 4.33.0, and added Lean 4.32.2 as a replacement for Lean 4.32.0.

• Various additions to options configurations across all tools:

  • The mathlib_options field (previously only on check, verify_proof, and highlight) is now accepted by every tool. It applies to everything the request elaborates. Note that this can change tool behavior; for example, the enable_autoImplicit pass in repair_proofs is mostly inert with Lean's defaults, but relevant with Mathlib options enabled.
  • The pretty-printing tools (normalize, extract_decls, extract_theorems, have2lemma, sorry2lemma, disprove) now accept a delab_options field: Lean pretty-printer options, e.g. {"pp.fieldNotation": false}, applied on top of the options that tool pretty-prints with. Only pp.* options are accepted. See the delab_options and verbosity field documentation for each tool for more details.
  • Every tool now accepts a global_options field: Lean options, e.g. {"maxHeartbeats": 400000}, applied to everything the request parses and elaborates, on top of the defaults and the mathlib_options preset. The format is the same as delab_options, but any registered option can be set, and values may be booleans, integers, or strings to match the type the option was declared with.

• This documentation is now also served in machine-readable form under /v1/docs: pages.json (a page manifest in navigation order), all.json (the manifest with each page's source markdown inlined), and raw/{slug}.md (one page's source markdown). See the documentation homepage for examples.

Fixed

• verify_proof with mathlib_options enabled now parses formal_statement with Mathlib settings as well; previously they only applied to content.
• repair_proofs now properly counts all time dedicated to file elaboration in the parse_ms timing field, not just the initial parse.
• Stray, ambiguous warnings are no longer emitted when a simplify_theorems iteration fails and falls back to the last stable version of the file.
• Fixed a rare case in simplify_theorems where removing an entire unused tactic sequence could cause the simplification pass to fail in older Lean versions. For example, this request used to fail and return the original content unchanged, because removing norm_num is invalid. Now, a synthetic skip tactic is inserted to ensure the content re-elaborates cleanly.
• Fixed a set of redundant reparses in extract_decls when computing each document's content field. Files containing many declarations should now expect a significant speed increase. (Up to 10x faster!)