菜单
Verification tools for compiling, validating, and disproving Lean theorems
用 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
Code transformation tools for repairing, simplifying, and extracting Lean proofs
Isolates failing proof steps by replacing them with `sorry` and extracting them into standalone lemmas to modularize and decouple complex Lean 4 proofs.
基于 SOC 职业分类
| name | verification |
| description | Verification tools for compiling, validating, and disproving Lean theorems |
Tools for verifying Lean code correctness.
| Tool | Purpose | When to use |
|---|---|---|
| lean-check | Compile a Lean file and report errors (local, no API key) | First step to validate any proof attempt |
| axle verify-proof | Validate a proof matches a formal statement | When you need to confirm a proof proves exactly the right theorem |
| axle disprove | Attempt to disprove theorems by proving negation | Before investing effort in a proof, check if the conjecture is false |
For full parameters and examples, read the corresponding reference-<tool>.md file in this directory.
