Skill

mathlib-pr

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.

Git

git-workflow

Install

npx claudepluginhub leanprover/skills --plugin lean

Tool Access

This skill uses the workspace's default tool permissions.

Preview

PR titles follow `<type>(<scope>): <subject>`.

SKILL.md

Similar Skills

skill-lookup

Searches, retrieves, and installs Agent Skills from prompts.chat registry using MCP tools like search_skills and get_skill. Activates for finding skills, browsing catalogs, or extending Claude.

prompts.chat

159.9k

prompt-lookup

Searches prompts.chat for AI prompt templates by keyword or category, retrieves by ID with variable handling, and improves prompts via AI. Use for discovering or enhancing prompts.

prompts.chat

159.9k

next-compile

1 file

Checks Next.js compilation errors using a running Turbopack dev server after code edits. Fixes actionable issues before reporting complete. Replaces `next build`.

vercel-next-js-2

139.2k

Stats

Stars38

Forks0

Last CommitFeb 20, 2026

Actions

View Source View Plugin View on GitHub View README

Mathlib PR Conventions

Commit Message Format

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

Workflow

PRs must come from forks, not branches on the main repo.
Run lake exe mk_all when adding or removing files (updates the import root).
PR dependencies use checkbox syntax in the description: - [ ] depends on: #XXXX
Comment !bench on a PR to trigger performance benchmarking.

Labels

Labels are added/removed via GitHub comments.

Author-managed:

awaiting-author — reviewer feedback needs addressing
WIP — work in progress
easy — trivial PRs (single lemma, typo fix, <25 line diff)
help-wanted, please-adopt — requesting help

Topic: 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.

Merge Process

Reviewer approves and adds maintainer-merge
Maintainer adds ready-to-merge
Bors bot merges the PR

For 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.

Style and Naming

Before submitting, read the relevant guides — these are the authoritative references:

Naming conventions: https://leanprover-community.github.io/contribute/naming.html
Code style: https://leanprover-community.github.io/contribute/style.html
Documentation style: https://leanprover-community.github.io/contribute/doc.html
PR lifecycle: https://leanprover-community.github.io/contribute/index.html