Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover-community/mathlib4/llms.txt

Use this file to discover all available pages before exploring further.

Mathlib4 is a collaborative, community-driven project and welcomes contributions of all kinds — new theorems, improved proofs, tactics, documentation, and infrastructure fixes. Whether you are formalizing a piece of undergraduate mathematics or a cutting-edge research result, the community is here to help you get your work merged. This page walks through everything you need to know before opening your first pull request.

​
Prerequisites

Before contributing you should have the following in place:
You do not need to build all of Mathlib from scratch. Running lake exe cache get downloads precompiled .olean files and will save many hours of compilation time.

​
Community and Support

The main communication hub for Mathlib development is the Zulip chat at leanprover.zulipchat.com. The #mathlib4 stream is the right place to:
  • Introduce yourself and your contribution plans.
  • Ask for guidance on whether a formalization fits Mathlib’s scope.
  • Get code review advice before opening a formal PR.
  • Discuss design questions about definitions and theorem names.
All questions — from beginner to expert — are welcomed. You can also browse the public Zulip archive without creating an account.

​
Code of Conduct

Mathlib follows the Contributor Covenant Code of Conduct. Participation in any community space — Zulip, GitHub issues, PRs, or elsewhere — requires:
  • Empathy and kindness toward all contributors, regardless of experience level.
  • Respect for differing opinions and the willingness to give and receive constructive feedback gracefully.
  • Constructive engagement: focus on what is best for the community, not just for the individual.
  • Zero tolerance for harassment, insulting comments, personal attacks, or the publication of others’ private information.
Violations can be reported through the reporting form or directly over Zulip to community leaders.

​
Pull Request Workflow

1
Fork the repository and create a branch
2
Fork leanprover-community/mathlib4 on GitHub, clone your fork locally, and create a feature branch with a descriptive name:
3
git clone https://github.com/<your-username>/mathlib4.git
cd mathlib4
git checkout -b feat/add-my-theorem
4
Fetch the precompiled .olean cache
5
Always do this before building. It downloads cached build artifacts from Mathlib’s CI servers and avoids recompiling the entire library from scratch:
6
lake exe cache get
7
If the cache download fails or produces unexpected results, try the force-refresh variant:
8
lake exe cache get!
9
Make your changes
10
Add new Lean files under the appropriate Mathlib/ subdirectory, or edit existing ones. Every new file must:
11
  • Begin with a copyright and author header.
  • Include a module docstring (/-! ... -/) describing its contents.
  • Be registered in the top-level import list (see Step 6).
    • 12
    See the Style Guide and Naming Conventions pages for the detailed rules that reviewers enforce.
    13
    Build and verify your changes
    14
    Build the specific file you modified to check for errors:
    15
    lake build Mathlib.Algebra.Group.Defs
    16
    Or build all of Mathlib (slower, but required before opening a PR):
    17
    lake build
    18
    Run the full test suite
    19
    lake test
    20
    This executes all tests defined under MathlibTest/. A clean run is required before requesting review.
    21
    Register any new files
    22
    If you added a new .lean file to the library, regenerate the top-level Mathlib.lean import file:
    23
    lake exe mk_all
    24
    Commit the updated Mathlib.lean alongside your new file.
    25
    Run the style linter
    26
    lake exe lint-style
    27
    This runs both the Python-based text linters and the Lean-based style linters. Fix all reported issues before opening a PR. See Building & Testing for a full reference of available linting commands.
    28
    Open a Pull Request
    29
    Push your branch to your fork and open a PR against the master branch of leanprover-community/mathlib4. The PR title must satisfy the format checked by check_title_labels — keep it concise, descriptive, and in the imperative mood (e.g., feat(Algebra.Group): add commutativity lemma for ...).
    30
    In the PR description, briefly explain:
    31
  • What mathematical content is being added or changed.
  • Why it belongs in Mathlib (scope justification).
  • Any open design questions you would like reviewers to weigh in on.
    • 32
    Address review feedback
    33
    Reviewers will comment directly on your diff. Address all requested changes by pushing additional commits to the same branch. The CI will re-run automatically on each push.
    34
    Bors merges approved PRs
    35
    Mathlib uses Bors as its merge bot. A reviewer with merge rights approves your PR by posting:
    36
    bors r+
    37
    Bors then adds the PR to the merge queue, runs a final CI build, and — if it passes — merges it into master. You do not merge your own PRs.

    ​
    Linter Options

    Mathlib enforces a standard set of linters via lakefile.lean. The most important options are listed below.
    OptionEffect
    linter.mathlibStandardSetEnables Mathlib’s full default set of linters
    linter.style.headerChecks that every file has a valid copyright/author header
    linter.style.longFileWarns when a file exceeds 1500 lines
    linter.checkInitImportsValidates imports in Mathlib.Init files
    linter.allScriptsDocumentedRequires all scripts to have documentation
    linter.pythonStyleEnforces Python-style indentation rules in scripts
    autoImplicitSet to false — all variables must be declared explicitly
    These options are applied via mathlibLeanOptions in lakefile.lean as weak options, meaning they apply to every lake build invocation across Mathlib, Archive, and Counterexamples.
    Never set autoImplicit := true in a Mathlib file. The library-wide default is false and undeclared variables will cause a build error.

    ​
    The autolabel Tool

    Mathlib uses a GitHub label system to categorize PRs by mathematical topic (e.g., t-algebra, t-topology, t-number-theory). The autolabel executable infers the correct label from the files your PR modifies. To preview labels without applying them: 
    lake exe autolabel
    To apply labels to a specific PR (requires the GitHub CLI gh to be installed): 
    lake exe autolabel <PR_number>
    For example: 
    lake exe autolabel 150100
    If your PR touches files in multiple topic areas, autolabel will only apply a label when there is a unique best match. Add labels manually when the tool cannot determine a unique choice.

    Style Guide

    File headers, line length, Unicode, indentation, and proof formatting rules.

    Naming Conventions

    How theorems, definitions, instances, and namespaces are named in Mathlib.

    Building & Testing

    Lake commands for building, testing, linting, and generating HTML docs.

    Build docs developers (and LLMs) love

    Get started for freeTalk to us