Stats
Actions
Tags
Help us improve
Share bugs, ideas, or general feedback.
From lean
Guides Mathlib4 pull request conventions for leanprover-community/mathlib4, covering commit messages, workflows, labels, merge processes, and style rules. Use for PR creation and management.
npx claudepluginhub leanprover/skills --plugin leanHow this skill is triggered — by the user, by Claude, or both
Slash command
/lean:mathlib-prThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
PR titles follow `<type>(<scope>): <subject>`.
Enforces PR conventions for leanprover/lean4 including commit message formats, changelog labels, module declarations, copyright headers, and description guidelines. Use for Lean contributions.
Provides Git workflow standards including branch naming, conventional commits, and PR guidelines. Use when creating branches, writing commits, or preparing PRs.
Enforces commit message formats, PR descriptions, and branch naming conventions to maintain a clean and traceable git history.
Share bugs, ideas, or general feedback.
PR titles follow <type>(<scope>): <subject>.
Types: feat, fix, doc, style, refactor, test, chore, perf, ci
Scope is the module path with the Mathlib/ prefix stripped — e.g. Data/Nat/Basic, Topology/Constructions.
Subject uses imperative present tense, no capitalized first letter, no trailing period.
Full conventions: https://leanprover-community.github.io/contribute/commit.html
lake exe mk_all when adding or removing files (updates the import root).- [ ] depends on: #XXXX!bench on a PR to trigger performance benchmarking.Labels are added/removed via GitHub comments.
Author-managed:
awaiting-author — reviewer feedback needs addressingWIP — work in progresseasy — trivial PRs (single lemma, typo fix, <25 line diff)help-wanted, please-adopt — requesting helpTopic: t-topology, t-algebra, t-combinatorics, etc.
Downstream projects: carleson, FLT, etc.
Automated: merge-conflict is added/removed automatically when conflicts are detected or resolved.
maintainer-mergeready-to-mergeFor delegated PRs (maintainer trusts author to finalize): the author comments bors merge to trigger the merge.
The review queue is at https://leanprover-community.github.io/queueboard/ — PRs with merge conflicts or pending CI don't appear there.
Before submitting, read the relevant guides — these are the authoritative references: