القائمة
Code transformation tools for repairing, simplifying, and extracting Lean proofs
التثبيت باستخدام Codex أو Claude انسخ هذا Prompt والصقه في Codex أو Claude أو مساعد آخر ليراجع صفحة Skill ويثبّتها لك.
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.
Verification tools for compiling, validating, and disproving Lean theorems
استنادا إلى تصنيف SOC المهني
| 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 python 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.
