Axiom provides cloud-based Lean 4 proof verification through the Axle API. It compiles and checks Lean code against a full Mathlib environment without requiring a local Lean installation -- verification results come back in seconds rather than the minutes it takes to build locally.
Reference Files
Read these as needed based on the task:
references/axiom-configuration.md
-- Setup, authentication, environment selection. Read this first if the user hasn't configured Axiom yet.
references/axiom-api-reference.md
-- All 14 API endpoints with parameters and response formats. Read when you need exact parameter names or response fields.
references/axiom-cli-reference.md
-- CLI commands and options. Read for exact flags and usage details when working with local files.
references/axiom-best-practices.md
-- Workflow guidance, scope limitations, and tips. Read when planning a multi-step workflow or hitting unexpected behavior.
Workflow
Step 1: Select the Right Tool
Match the user's intent to the appropriate endpoint:
User wants to...
Endpoint
Notes
Verify a proof is correct
verify_proof
Checks candidate proof against a formal statement
Check if code compiles
check
Quick syntax and type checking
Understand proof structure
extract_theorems
Splits file into self-contained theorem units
Rename declarations
rename
Automatic reference updates throughout
Convert theorem/lemma
theorem2lemma
Switch between
theorem
and
lemma
keywords
Stub out proofs
theorem2sorry
Replace proofs with
sorry
for scaffolding
Combine files
merge
Intelligent deduplication across files
Remove no-op tactics/haves
simplify_theorems
Tactics that don't change proof state, unused haves
Remove post-completion tactics
repair_proofs
Tactics after proof is done, replace sorry, fix unsafe tactics
Extract have statements
have2lemma
Promote inline
have
to standalone lemma
Stub have bodies
have2sorry
Replace
have
bodies with
sorry
Extract sorry placeholders
sorry2lemma
Turn
sorry
into lemma stubs
Test if statement is false
disprove
Attempts counterexample via Plausible
Standardize formatting
normalize
Clean up sections, namespaces, comments
When unsure which tool to use:
Start with
check
to see if the code compiles at all
Use
extract_theorems
to understand what's in the file
Use
normalize
first if the file uses
section
/
namespace
blocks (these can cause issues with other tools)
Step 2: Execute
When working with local files
, prefer the
axle
CLI -- it reads files directly from disk, has simpler syntax, and can write output to files with
-o
. The CLI reads
AXLE_API_KEY
from the environment automatically. Note: CLI commands use hyphens (e.g.,
verify-proof
), while the HTTP API uses underscores (
verify_proof
). All code is sent to
axle.axiommath.ai
for compilation against a full Mathlib environment -- the CLI is not local verification.
When constructing Lean code dynamically
(generating content in scripts, CI/CD pipelines, or building code strings programmatically), use the HTTP API via curl or the Python client (
pip install axiom-axle
). The API accepts content as JSON strings, which is better suited for generated or in-memory code.
is empty. This is the only state that means the proof is both compilable and complete.
For transformation tools
(
repair_proofs
,
simplify_theorems
,
normalize
, etc.): These do not return
okay
or
failed_declarations
. Check that
lean_messages.errors
is empty and inspect the
content
field for the transformed result.
For
disprove
:
Check
disproved_theorems
(list of refuted names) and
results
(dict mapping each theorem name to a human-readable outcome string). If a counterexample is found, the name appears in
disproved_theorems
and the
results
entry contains the counterexample. If disprove fails (the theorem may be true),
disproved_theorems
is empty and the
results
entry describes why the negation could not be proven.
Import handling:
Always use
--ignore-imports
(CLI) or
"ignore_imports": true
(API) unless you have a specific reason not to (e.g., testing that exact imports are correct). Without this flag, import mismatches return a
user_error
string instead of the standard response format, which breaks JSON parsing and hides the actual verification result. Code snippets, code from different Lean/Mathlib versions, and proof-logic checks all require this flag.
user_error
responses:
Several error conditions return
{"user_error": "...", "info": {...}}
instead of the standard response format. This includes import mismatches (when
ignore_imports
is false), unrecognized declaration names in
rename
, and other request-level validation failures. Always check for a
user_error
field before parsing
lean_messages
/
tool_messages
.
Common Multi-Step Workflows
Verify and fix a proof:
check
-- see if it compiles
If errors:
repair_proofs
-- attempt automatic fix
check
again -- verify the repair worked
verify_proof
-- confirm it proves the intended statement
Analyze and clean a file:
normalize
-- standardize formatting first (flatten sections/namespaces)
extract_theorems
-- understand the structure
repair_proofs
with
remove_extraneous_tactics
-- remove tactics after proof is already complete
simplify_theorems
-- remove unused haves and no-op tactics
check
-- verify nothing broke
Scaffold a proof development:
Write formal statements
theorem2sorry
-- stub out proofs with
sorry
(use
names
parameter to target specific theorems)
Fill in proofs incrementally
check
after each proof to verify progress
sorry2lemma
-- track remaining obligations (generates
{name}.sorried
lemma stubs inserted before each sorry'd theorem)
verify_proof
for final verification
Test a conjecture:
disprove
-- look for counterexamples first
If no counterexample found, attempt the proof
check
incrementally as you build the proof
verify_proof
when complete
Common Pitfalls
Custom project attributes and constructs.
Files from Lean projects often define custom attributes (e.g.,
@[category research open, AMS 11]
) and helper constructs (e.g.,
answer(sorry)
) via project-specific imports. When
ignore_imports: true
replaces those imports with standard Mathlib, these custom constructs become unresolvable and produce compilation errors.
Before submitting
, strip custom attributes and project-specific constructs using sed or similar:
sed 's/@[category [^]]*]//' file.lean
removes
@[category ...]
blocks; replace
answer(sorry)
with
True
or remove it entirely. Note:
@[category ... open ...]
triggers a misleading "Candidate uses banned 'open private' command" tool error because the parser misinterprets the word
open
inside the attribute as the
open private
command -- this is a false positive that disappears once the attribute is stripped.
autoImplicit
is off in Mathlib environments.
Always declare type variables explicitly (e.g.,
variable
or
(α : Type*)
). Implicit variables like
List α
without declaring
α
will fail.
Mathlib name shadowing.
If your theorem names match existing Mathlib declarations (e.g.,
add_zero
,
add_comm
,
mul_comm
), you'll get "already declared" errors and all transformation tools will silently return unchanged content with zero stats. The error appears only in
lean_messages.errors
, not
tool_messages
-- you must inspect
lean_messages
to notice the problem. Use
rename
to give theorems unique names, or prefix with a namespace.
omega
cannot see through opaque definitions.
The
omega
tactic works on linear arithmetic over
Nat
and
Int
, but it treats user-defined functions as opaque. If you define
def my_double (n : Nat) := n + n
and try to prove
my_double n = 2 * n
with
omega
, it will fail because
omega
doesn't know what
my_double
computes. Use
unfold my_double
(or
simp [my_double]
) before
omega
to expose the definition.
simplify_theorems
vs
repair_proofs
for cleanup.
These serve different purposes:
simplify_theorems
with
remove_unused_tactics
removes tactics that are no-ops (don't change the proof state at all)
repair_proofs
with
remove_extraneous_tactics
removes tactics that appear
after
the proof is already complete
For cleaning up redundant tactics, you usually want
repair_proofs
first, then
simplify_theorems
.
Sections and namespaces.
extract_theorems
,
theorem2sorry
, and other transformation tools may produce non-compilable output when sections/namespaces are present because extracted names won't be fully qualified. Always run
normalize
first to flatten these constructs. Note that
normalize
preserves the original indentation from inside flattened blocks -- the output may look oddly indented but still compiles correctly.
Caveat:
normalize
may not update all references inside theorem bodies when flattening namespaces (e.g.,
p k
may not become
Namespace.p k
). Always
check
the normalized output and fix any unresolved references manually.
rename
requires fully-qualified names.
The
declarations
parameter must use fully-qualified names including namespace prefixes. For example, if
my_thm
is inside
namespace Foo
, use
{"Foo.my_thm": "Foo.new_name"}
, not
{"my_thm": "new_name"}
. Using an unqualified name returns a
user_error
("Source name not found").
Non-theorem commands in
extract_theorems
.
The
extract_theorems
tool warns about any non-theorem command it encounters with
"Unsupported command kind ..."
. This includes
variable
,
open
,
notation
,
set_option
, and other non-declaration commands. These warnings are informational -- the tool still correctly extracts all theorem declarations and includes dependencies (including
variable
bindings,
open
statements, etc.) in each theorem's standalone
content
block.
Always check both message types.
Transformation tools can "succeed" (return content with zero
tool_messages
errors) while the underlying code has compilation errors visible only in
lean_messages.errors
. Always inspect
lean_messages.errors
even when
tool_messages
is clean. This silent failure mode applies broadly:
any
compilation error (custom attributes, missing imports, syntax issues, name shadowing) causes transformation tools to return unchanged content with zero stats. The only signal is non-empty
lean_messages.errors
.
The environments endpoint
uses
/v1/environments
(no
/api/
prefix), while all tool endpoints use
/api/v1/{tool_name}
.