用 Codex 或 Claude 帮你安装 复制这段 Prompt,粘贴到 Codex、Claude 或其他助手里,让它检查 Skill 页面并帮你完成安装。
直接命令不会经过审查 Prompt;运行前请先检查来源。
npx skills add https://github.com/project-numina/numina-lean-agent --skill code-transform命令会保持在同一行。复制前请横向滚动并检查完整内容。
想先保存到本地?可下载 SkillsMP 当前能够提供的文件。
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
基于 SOC 职业分类
正在显示 SKILL.md
| 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.