Individual skill
lean-check
Formalize a self-authored lemma or theorem in Lean 4/mathlib and require a clean `lake build` without `sorry`. Use when the mathematical claim can be stated faithfully and machine-checked. For numerical falsification or symbolic algebra, use $numerical-check or $symbolic-check.
skills/lean-check/SKILL.md
Source commit 08dd9bdf9367f7321c27b7db8c08a125598a613f
What was checked
- Matches the observed repository HEAD
- Yes
- Scanner rules are current
- No
- Repository scan complete
- No
- Skill scan complete
- No
- Observed behavior
- Not checked yet
- Last checked
- Nov 6, 2026
These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.
Install this skill
Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.
An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.
Repository context
- Repository stars (not skill ratings)
- 150
- Repository last updated
- Nov 3, 2026
- License
- MIT
Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.
- academic-research Repository topic
- ai-tools Repository topic
- claude Repository topic
- claude-code Repository topic
- latex Repository topic
- phd Repository topic
- research-workflow Repository topic
- codex Repository topic
- engineering Derived category
Files and excerpt
File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.
Read excerpt
# 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-check` fails to falsify a claim and it's important enough to *prove*.
## When NOT to Use
| Situation | Use instead |
|---|---|