lean-check
Installation
SKILL.md
Lean Check: Machine-Prove a Self-Authored Lemma
Formalize a lemma/theorem in Lean 4 + mathlib and let the kernel check it. A lake build that succeeds with no sorry and no extra axioms is a machine-verified proof — the strongest guarantee available.
When to Use
- A critical lemma whose correctness you want beyond doubt (the load-bearing step of a theorem).
lean-check, "formalize this in Lean", "machine-check this lemma", "prove this in Lean 4".- After
numerical-checkfails to falsify a claim and it's important enough to prove.
When NOT to Use
| Situation | Use instead |
|---|---|
| Stress-test / hunt a counterexample to a distributional claim | numerical-check (R1) |
| Verify an algebra / derivative / limit / closed-form step | symbolic-check (R2) |
| A statement too rich to faithfully formalize in reasonable time (heavy measure theory, bespoke objects) | domain-reviewer — do NOT force a lossy Lean statement |