| name | axiom-lean-prover |
| description | Formally verify Lean 4 proofs against Mathlib using the hosted Axiom AXLE API — no local Lean toolchain. Use in the mathematics_lean domain, when a proof needs machine-checked verification but installing Lean/Mathlib locally is undesirable, or when translating informal proofs into formally verified Lean 4 code checked in the cloud. |
Axiom Lean Prover (AXLE)
Formal proof verification with Lean 4 + Mathlib, checked by the hosted Axiom AXLE
API (https://axle.axiommath.ai). There is no local Lean install, no lake, and
no Mathlib cache — .lean files are sent as text to AXLE, which checks them against
a preloaded full Mathlib and returns structured errors/warnings with source positions.
This is the cloud-verified counterpart of the lean-prover skill. If you want a local
lake build workflow instead, use lean-prover. Do not mix them in one workspace.
When to Use
- Working in the
mathematics_lean research domain
- Verifying proofs without provisioning a multi-GB local Lean/Mathlib toolchain
- Translating an informal proof into formally verified Lean 4 code
- Checking whether a mathematical statement is provable / type-checks
Setup
Almost none. You need:
AXLE_API_KEY in the environment (already passed through from the project .env).
Verify with: echo "${AXLE_API_KEY:0:6}..." (should print pk_...).- Python 3.10+ (already present). The verifier uses only the standard library.
Create a directory for your proof files (any name; proofs/ by convention):
mkdir -p proofs
That's it — no elan, no lake, no lake exe cache get, no initial build.
The Verifier: axle_check.py
lake build is replaced by this one script (the ground truth for this domain):
python .claude/skills/axiom-lean-prover/scripts/axle_check.py proofs/MyProof.lean
| Invocation | Meaning |
|---|
axle_check.py FILE.lean [FILE2 ...] | Check files, concatenated in the given order |
axle_check.py --dir proofs/ | Check every .lean under a directory (auto-ordered: Definitions → Lemmas → Theorems) |
axle_check.py --code "theorem t : 1=1 := rfl" | Check an inline snippet (great for #check-style lemma lookups) |
cat f.lean | axle_check.py - | Read from stdin |
... --statement-check | Treat sorry as success — for confirming a stub type-checks |
... --json | Also dump the raw API response |
... --environment lean-4.29.0 | Pin a Lean environment (default lean-4.29.0, or $AXLE_ENV) |
Exit codes (use them in loops)
| Code | Status | Meaning |
|---|
0 | COMPLETE | Compiles, no errors, no sorry → the proof is formally done ✓ |
2 | INCOMPLETE_SORRY | Compiles, but a declaration uses 'sorry' → statement OK, proof unfinished |
1 | ERROR | Compile / type / tactic error → read the messages and fix |
3 | TRANSPORT_ERROR | Network / auth / quota / usage error (e.g. missing AXLE_API_KEY) |
A sorry proof returns okay:true from the API — it compiles but is not proven.
The script catches this and reports INCOMPLETE_SORRY. Never report a sorry'd result
as complete. This is the exact analogue of the old "green build but grep finds sorry".
Error positions
On any non-trivial result the script writes the exact text it sent to AXLE to
.axle_last_check.lean in the current directory. Lean positions look like
-:7:12-7:18 (line:col); they refer to that normalized file, so open it to see
the offending line. (Line numbers differ from your source files because all import
lines are collapsed into a single import Mathlib at the top — see Imports below.)
Imports — IMPORTANT (different from the local lean-prover skill)
Always start a proof file with the full import:
import Mathlib
- The AXLE environment has all of Mathlib preloaded; the full import costs nothing
(it is checked remotely — there is no local cache to download or build).
- The default AXLE environment's import set is exactly
[Mathlib]. Sending
import Mathlib.Tactic or specific submodules triggers an "Imports mismatch".
axle_check.py strips every import line you write and prepends a single
import Mathlib (and sets ignore_imports), so submodule imports or local
cross-file imports (import Proofs.Definitions) are normalized away and never
break the check. You still write import Mathlib at the top of each file for
clean, human-readable Lean source.
This is the opposite of the lean-prover skill's "never use bare import Mathlib"
rule — that rule exists only to limit local cache size, which is irrelevant here.
Using lemmas that are NOT in Mathlib
Only Mathlib is available remotely — you cannot import an external Lean package
(an import SomeProject.Lemmas line is stripped and its names become unknown identifier).
When the resource finder surfaces a lemma that lives outside Mathlib (a paper's companion
formalization, a GitHub Lean project, or an informal result from the literature), you have
two honest options:
Option 1 (preferred) — inline and prove it
Copy the lemma's statement and Lean proof into your proofs/ files and let AXLE verify
it against Mathlib like any other declaration. If its proof only depends on Mathlib, this is
clean and gives a fully machine-checked result. Re-prove informal (paper) lemmas the same way.
Option 2 (escape hatch) — cite it as a named axiom
If proving a prerequisite would itself require proving a long chain of further non-Mathlib
lemmas (too costly for the session), you may assume it rather than re-prove it — but do
this with a named axiom, never with sorry:
/-- Assumed without proof; established in [Smith 2020, Theorem 3]. -/
axiom key_prerequisite (G : Type*) [Group G] : SomeProperty G
Then use key_prerequisite freely in downstream proofs. They will verify as
COMPLETE (CONDITIONAL on N assumed axiom(s)) — i.e. correct modulo the cited
assumption. axle_check.py detects every axiom you declare and lists it, so a conditional
result is never mistaken for a fully-closed one.
axiom vs sorry — they mean different things
| Meaning | Verifier status | Use when |
|---|
axiom L : … | Deliberately assumed, justified by a citation | COMPLETE (CONDITIONAL …), exit 0 | You are intentionally citing an external result and proceeding |
… := by sorry | Unfinished — a proof you still intend to write | INCOMPLETE_SORRY, exit 2 | A placeholder during development |
Never use sorry as a stand-in for a citation: sorry says "not done yet", a named
axiom says "assumed on purpose, here's the reference".
Audit what a result depends on
Lean tracks axiom dependence transitively. Confirm exactly which assumptions a theorem rests
on with #print axioms:
python .claude/skills/axiom-lean-prover/scripts/axle_check.py --code '#print axioms my_main_theorem' --json
propext, Classical.choice, Quot.sound are Mathlib's standard trusted axioms (expected —
ignore them). Any of your own axiom names appearing there are cited assumptions that
must be listed in REPORT.md's Verification Status, so the result is honestly reported as
"verified modulo {…}".
Project Structure (convention)
proofs/
├── Definitions.lean # types, structures, notation
├── Lemmas.lean # supporting lemmas
└── MainTheorem.lean # main results
axle_check.py --dir proofs/ checks them together in dependency order. Because files
are concatenated, use one namespace and close it, or keep everything in a single
file — repeated namespace Foo ... end Foo blocks across files are fine, but an
unclosed namespace will nest into the next file (a harmless linter warning).
For multi-file proofs, write each file's local import Proofs.X as usual; the verifier
strips them and concatenation supplies the actual definitions.
Verification Workflow (Per Proof)
python .claude/skills/axiom-lean-prover/scripts/axle_check.py proofs/MainTheorem.lean --statement-check
python .claude/skills/axiom-lean-prover/scripts/axle_check.py proofs/MainTheorem.lean
python .claude/skills/axiom-lean-prover/scripts/axle_check.py --dir proofs/
Looking up Mathlib lemmas without a local Lean
#check works through the API — submit it as a snippet:
python .claude/skills/axiom-lean-prover/scripts/axle_check.py --code '#check @Nat.add_comm'
Add --json to read the #check type from lean_messages.infos. Combine several
#check lines in one snippet to probe many names in a single request.
Writing Proofs
Theorem / Lemma syntax
import Mathlib
namespace Proofs
-- Statement only (use sorry to check the type compiles first)
theorem my_theorem (n : ℕ) (h : n > 0) : n * 2 > n := by
sorry
-- Full proof
theorem my_theorem (n : ℕ) (h : n > 0) : n * 2 > n := by
omega
end Proofs
Definitions
def MySet := Finset ℕ
structure MyGraph where
vertices : Finset ℕ
edges : Finset (ℕ × ℕ)
inductive Tree (α : Type) where
| leaf : Tree α
| node : α → Tree α → Tree α → Tree α
Core Tactic Reference
| Tactic | When to use |
|---|
ring | Equalities in commutative (semi)rings: a*(b+c) = a*b + a*c |
ring_nf | Normalize ring expressions without closing the goal |
norm_num | Concrete numerical facts: 2 + 2 = 4, Nat.Prime 7 |
omega | Linear arithmetic over ℤ/ℕ: n + 1 > n |
linarith | Linear arithmetic with hypotheses: h1 : a < b, h2 : b < c ⊢ a < c |
nlinarith | Nonlinear arithmetic (products of hypotheses) |
simp | Simplify with the simp set; simp [l1, l2] to add lemmas |
simp only [h] | Targeted rewrite using only h; safer than bare simp |
exact h | Close goal exactly with h or a term |
apply f | Apply function/lemma f, unifying conclusion with goal |
rw [h] / rw [← h] | Rewrite left-to-right / right-to-left using equation h |
constructor | Split an And / Iff goal |
intro h | Introduce hypothesis from ∀ or → |
obtain ⟨a, b, h⟩ := hx | Destructure existential / conjunction |
use x | Provide a witness for ∃ |
cases h / rcases | Case split on inductive type or Or |
induction n with | Structural induction |
by_contra h | Proof by contradiction |
push_neg | Push negation inward |
contrapose! | Switch to contrapositive and push negation |
gcongr | Congruence for monotone operations |
field_simp | Clear denominators in field goals |
positivity | Prove 0 < x or 0 ≤ x |
decide / native_decide | Close decidable props by computation (small / larger finite cases) |
tauto | Propositional tautologies |
aesop | Automated search combining many strategies |
Note: interactive tactics exact?, apply?, simp? are not useful through the
API (they need an editor). Use #check snippets and Mathlib naming conventions instead.
Searching Mathlib
Naming conventions (predict lemma names)
Nat.add_comm — commutativity of + on ℕInt.mul_neg — negation rule for * on ℤList.map_comp — map composed with comp- Type-namespaced:
Finset., Set., Matrix., Polynomial.
#check to confirm a name exists (via the API, see above)
Web search
leanprover-community.github.io/mathlib4_docs for the exact namespace.
Interpreting Lean Error Messages
(Identical to local Lean — same kernel, same Mathlib. These appear in
lean_messages.errors with a -:line:col position.)
| Error | Meaning |
|---|
unknown identifier 'foo' | foo not in scope — usually a wrong Mathlib name; check with #check |
type mismatch: expected X got Y | Wrong type — check the hypothesis you're applying |
unsolved goals: ⊢ P | Proof incomplete — P still needs proving |
application type mismatch | Applied a lemma to the wrong argument type |
failed to synthesize instance | Missing typeclass — may need [DecidableEq α] etc. |
declaration uses 'sorry' | Type-checks but NOT proven — replace every sorry (reported as INCOMPLETE_SORRY) |
Imports mismatch | You sent non-Mathlib imports without normalization — let axle_check.py handle imports |
Proof Skeleton Template
import Mathlib
namespace Proofs
/-- One-line description of what this proves. -/
theorem theorem_name
(param1 : Type1) (param2 : Type2)
(hyp1 : Condition1) (hyp2 : Condition2) :
Conclusion := by
sorry -- replace with the actual proof
/-- Supporting lemma used in the main theorem. -/
lemma lemma_name (n : ℕ) : n + 0 = n := by
simp
end Proofs
Tips
- State first, prove later. Stub every statement with
sorry, run with
--statement-check until all type-check, then fill in proofs bottom-up.
- Automation first. Try
omega, simp, ring, norm_num, linarith, aesop
before hand-writing tactic steps.
- Mind rate limits. AXLE allows ~20 concurrent requests per key. The check is fast
(~50–100 ms), but check meaningful units (a full file) rather than spamming
one-line edits.
- Pin the environment with
--environment (or $AXLE_ENV) and record it in your
report for reproducibility — it determines the Lean and Mathlib versions used.
