Menú
Code transformation tools for repairing, simplifying, and extracting Lean proofs
Instalar con Codex o Claude Copia este prompt, pégalo en Codex, Claude u otro asistente, y deja que revise la página de la skill y la instale por ti.
Basado en la clasificación ocupacional SOC
A no-op skill used only by the agent-capability tests to confirm a harness can mount and invoke a skill. Has no real behavior; invoke it when asked to during a capability probe.
Use when editing .lean files, debugging Lean 4 builds (type mismatch, sorry, failed to synthesize instance, axiom warnings, lake build errors), searching mathlib for lemmas, formalizing mathematics in Lean, or learning Lean 4 concepts. Also trigger when the user asks for help with Lean 4, mathlib, or lakefile. Do NOT trigger for Coq/Rocq, Agda, Isabelle, HOL4, Mizar, Idris, Megalodon, or other non-Lean theorem provers.
Lean 4 theorem proving toolkit: search lemmas, verify proofs, repair/simplify code, and get LLM-assisted informal proofs
LLM-assisted tools for informal proofs, proof strategy discussion, and code simplification
Search tools for finding Lean theorems, lemmas, and definitions in Mathlib
Isolates failing proof steps by replacing them with `sorry` and extracting them into standalone lemmas to modularize and decouple complex Lean 4 proofs.
| name | code-transform |
| description | Code transformation tools for repairing, simplifying, and extracting Lean proofs |
Tools for automatically transforming and improving Lean proof code. All scripts use uv run --no-project .claude/skills/cli/axle.py <subcommand>.
| Tool | Purpose | When to use |
|---|---|---|
| axle repair-proofs | Auto-fix broken proofs using configurable repair strategies | When a proof fails and you want automated repair before manual editing |
| axle simplify-theorems | Clean up proofs by removing unused tactics and bindings | As a final cleanup step after a proof is verified |
| axle sorry2lemma | Lift sorry placeholders into standalone named lemmas | When a proof has multiple sorry sub-goals you want to tackle independently |
| axle extract-theorems | Split a Lean file into structured per-theorem records | For analysis, dataset construction, or understanding file structure |
For full parameters and examples, read the corresponding reference-<tool>.md file in this directory.
