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

1. •Reviewer approves and adds maintainer-merge
2. •Maintainer adds ready-to-merge
3. •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