// PR conventions for leanprover-community/mathlib4. Use when creating pull requests, writing commit messages, or managing labels for Mathlib contributions.
Use when asked to prove something in Lean. Covers one-step-at-a-time proving, error priority, working on the hardest case first, proof cleanup, and handling dependent type rewriting issues.
Bisect Lean toolchain versions to find where behavior changes. Use when trying to identify which Lean 4 commit caused a regression or behavior change.
Create minimal working examples (MWEs) from Lean errors for bug reports. Use when minimizing a Lean error, creating an MWE, or preparing a bug report for lean4 or mathlib4.
PR conventions for the leanprover/lean4 repository. Use when creating pull requests, writing commit messages, or following project conventions for Lean contributions.
Set up a lean4 repository clone with proper elan toolchains.
Building Mathlib
| name | mathlib-pr |
| description | PR conventions for leanprover-community/mathlib4. Use when creating pull requests, writing commit messages, or managing labels for Mathlib contributions. |
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: