Verify and repair Lean 4 proofs with Axiom
Run /spec:axiom to verify, check, transform, and repair Lean 4 proofs using the cloud-based Axiom API — no local Lean installation required.
What it does
- Verify proofs against formal statements
- Check syntax and type errors instantly
- Extract and analyze theorems from files
- Repair broken proofs after version upgrades
- Simplify, normalize, and transform code
- Disprove false conjectures via counterexample
How it works
- Select the endpoint matching your intent (14 available)
- Execute via the axle CLI against the Axle API
- Interpret lean_messages and tool_messages from the response
- Iterate — check, repair, verify until the proof is sound
Output
Verification results, repaired code, extracted theorems, or transformation output — all with detailed error diagnostics from the Lean compiler and Axle tool messages.
> Verify my Lean 4 proof of list_reverse_involutive
◆ I'll verify your proof using the Axiom API. Let me read the references and check the code.
Read .claude/skills/axiom-verify/references/axiom-api-reference.md
Read .claude/skills/axiom-verify/references/axiom-best-practices.md
Read Reverse.lean
◆ File has 4 declarations including list_reverse_involutive. Sending to Axiom for compilation check.
Run curl -s -X POST .../api/v1/check -d '{"content": "...", "environment": "lean-4.28.0", "ignore_imports": true}' | jq '{okay, failed_declarations, lean_errors: .lean_messages.errors}'
{
"okay": false,
"failed_declarations": [],
"lean_errors": ["unknown identifier 'List.reverseAux_eq'"]
}
◆ Compilation fails — okay is false with a lean_messages error. List.reverseAux_eq was renamed in recent Mathlib. I'll run repair_proofs to fix the broken tactics.
Run curl -s -X POST .../api/v1/repair_proofs -d '{"content": "...", "environment": "lean-4.28.0", "ignore_imports": true, "repairs": ["remove_extraneous_tactics", "apply_terminal_tactics"]}' | jq '{repair_stats, lean_errors: .lean_messages.errors}'
{
"repair_stats": { "apply_terminal_tactics": 2, "remove_extraneous_tactics": 1 }
"lean_errors": []
}
Edit Reverse.lean 3 hunks, +6 -4 lines
◆ Repair succeeded — 2 tactics replaced via grind, 1 extraneous tactic removed. lean_errors is empty. Now verifying against the formal statement.
Run curl -s -X POST .../api/v1/verify_proof -d '{"formal_statement": "...", "content": "...", "environment": "lean-4.28.0", "ignore_imports": true}' | jq '{okay, failed_declarations, tool_errors: .tool_messages.errors}'
{
"okay": true,
"failed_declarations": [],
"tool_errors": []
}
okay: true, failed_declarations: [] — proof is valid
✓ reverse_nil : ([] : List α).reverse = []
✓ reverse_cons : (a :: l).reverse = l.reverse ++ [a]
✓ reverse_append : (l₁ ++ l₂).reverse = l₂.reverse ++ l₁.reverse
✓ list_reverse_involutive : l.reverse.reverse = l
✓ Proof verified — 4 declarations checked, 2 tactics repaired, 0 failures
API: verify_proof (lean-4.28.0, ignore_imports: true)
File: Reverse.lean (repaired, verified)