Contributing Workflow for mathlib

A guide for the contribution process to mathlib4, the standard library for Lean 4.

Quick Start

One-time Setup

# Fork and clone using GitHub CLI (recommended)
gh repo fork leanprover-community/mathlib4 --default-branch-only --clone
cd mathlib4

# Or manually:
# 1. Fork on GitHub
# 2. Clone your fork: git clone https://github.com/YOUR_USERNAME/mathlib4.git
# 3. Add upstream: git remote add upstream https://github.com/leanprover-community/mathlib4.git

Daily Workflow

# Update master
git switch master
git pull

# Create feature branch
git switch -c my-feature-branch

# Make changes, commit, push
git add .
git commit -m "feat: add theorem X"
git push

# Open PR on GitHub or via CLI
gh pr create --fill

What to Contribute

Welcome Contributions

Small fixes: docstring fixes, typo corrections
Single lemma additions: to existing theories
Extended theories: new theorems extending existing areas
New theories: if within mathlib's scope

Scope Check

Ask before contributing new theories:

Is this typically taught in a mathematics department?
Does it align with maintainers' mathematical interests?
Can you find a reviewer?

If unsure, ask on Zulip in #mathlib.

External Projects

Consider creating a standalone repository with mathlib as a dependency if your work is outside scope.

Communication

Use Zulip to discuss before and during work
Add GitHub username to Zulip profile
Set display name to real name

PR Conventions

Title Format

<type>(<optional-scope>): <subject>

Types: feat, fix, doc, style, refactor, test, chore, perf, ci

Examples:

feat(Data/Nat): add factorial function
fix(Algebra/Group): resolve instance synthesis issue
doc: improve module documentation

Description

Use imperative, present tense
Explain motivation and contrast with previous behavior
Include : for breaking changes

Dependencies

Depends on: #1234

Git Workflow

Setup Remotes

git remote -v
# Should show:
# origin    https://github.com/YOUR_USERNAME/mathlib4.git
# upstream  https://github.com/leanprover-community/mathlib4.git

Creating PRs

# Keep master updated
git switch master
git pull

# Create branch
git switch -c my-feature

# Push and create PR
git push
gh pr create --fill

Working on Others' PRs

# Via GitHub CLI
gh pr checkout 1234

# Manually
git remote add contributor https://github.com/USERNAME/mathlib4.git
git fetch contributor
git checkout contributor/branch-name

Review Process

Finding Reviewers

Anyone can review - not just maintainers
Seek out reviewers yourself
Partial reviews are helpful
History of reviews → eligibility for reviewer/maintainer teams

What Reviewers Check

Style - follows naming, formatting
Documentation - doc strings present
Location - correct file/module
Improvements - can be simplified
Library integration - fits with existing API

Being Reviewed

Be respectful and encouraging
Leave room for alternative approaches
Recognize you may be wrong
Helpful reviews criteria for maintainer eligibility

Performance

Benchmarking

Comment !bench on PR to trigger benchmarking
Significant changes need proactive benchmarking:
- New classes/instances
- New simp lemmas
- Changed imports
- New definitions

Avoiding Regressions

Profile before submitting
Check impact on compilation time

mathlib-workflow