Stats
Actions
Tags
'%20stop-opacity%3D'0.16'%2F%3E%3Cstop%20offset%3D'1'%20stop-color%3D'rgb(200%2C90%2C60)'%20stop-opacity%3D'0.03'%2F%3E%3C%2FlinearGradient%3E%3C%2Fdefs%3E%3Crect%20width%3D'320'%20height%3D'200'%20fill%3D'url(%23g)'%2F%3E%3Ccircle%20cx%3D'250'%20cy%3D'56'%20r%3D'92'%20fill%3D'rgb(200%2C90%2C60)'%20fill-opacity%3D'0.06'%2F%3E%3Ccircle%20cx%3D'64'%20cy%3D'172'%20r%3D'58'%20fill%3D'rgb(200%2C90%2C60)'%20fill-opacity%3D'0.05'%2F%3E%3C%2Fsvg%3E)
From lean
Provides Mathlib PR review guidelines for Lean: attributes/API, style (simp squeezing, normal forms, transparency), file size tips, and reference links. Use for PR reviews and code quality checks.
How this skill is triggered — by the user, by Claude, or both
Slash command
/lean:mathlib-reviewThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
- New definitions should come with associated lemmas and appropriate attributes (`@[simp]`, `@[ext]`, etc.).
@[simp], @[ext], etc.).FunLike API for morphism classes, SetLike API for subobject classes.simp calls should NOT be squeezed (replaced with simp only [...]) unless there's a measured performance problem. Unsqueezed simp is more maintainable and doesn't break when lemmas are renamed.s.Nonempty over alternatives. Use hne : x ≠ ⊥ in hypotheses (easier to check), hlt : ⊥ < x in conclusions (more powerful).erw, or rfl after simp/rw usually means the API is missing lemmas.The full review guide and style references:
npx claudepluginhub leanprover/skills --plugin leanGuides Mathlib4 pull request conventions for leanprover-community/mathlib4, covering commit messages, workflows, labels, merge processes, and style rules. Use for PR creation and management.
Enforces mathlib code quality and style for Lean 4 projects. Helps with naming, documentation, proof golfing, and PR preparation.
Guides code review practices, highlighting common issues and areas for improvement. Activates when reviewing pull requests or code changes.