How to contribute to mathlib #

Here are some tips and tricks to make the process of contributing as smooth as possible.

What to contribute to mathlib #

Small fixes (for example fixes in docstrings) and single-lemma additions in already-existing theories are almost always welcome as contributions to mathlib. Longer PRs which extend existing theories are also almost always welcome.

But what about adding completely new theories to mathlib? Here, things can be more nuanced. The first question you will need to consider is whether the material you want to contribute is a good fit for mathlib. Whilst there is currently no formal description of exactly what mathlib's remit is, here are some questions which you can ask about your proposed contribution.

In particular the remit of mathlib should not be thought of as "all of mathematics and related areas". As the number of open PRs increases, the maintainers will sometimes need to make some hard decisions.

If you are not sure about whether your proposed topic is a good fit for mathlib, then please feel free to open a discussion in the #mathlib channel on the Lean Zulip.

An issue related to the fact that the expertise of the maintainers may not cover all of mathematics: you may want to think about who is going to review your potential PR. Contributors are encouraged to seek out reviewers for their PRs. A PR reviewer does not have to be a maintainer! This seems to be a common misconception by the community. Reviews of PRs, especially from new reviewers, are essentially always welcome.

Please also consider the possibility of creating a standalone repository, and adding mathlib as a dependency. There are many Lean repositories on github, indexed by reservoir. And here are those projects which have mathlib has a dependency. The solution of having a new project which depends on mathlib is a particularly good fit for projects in areas which do not align with the expertise of the mathlib maintainers. One example of such a repository is the combinatorial game theory repository. This solution is also a good fit for projects which would like to move quickly; at the time of writing (Sep 2025), mathlib has just under 2000 open PRs and it may take time for mathlib contributions to be reviewed and merged.

Working on mathlib #

We use git to manage and version control mathlib.

Please see the Git Guide for Mathlib4 Contributors for detailed instructions if you have not contributed to an open source project with git before.

The master branch is the "production" version of mathlib. It is essential that everything in the master branch compiles without errors, and there are no sorrys. To ensure this, we only commit changes to master that have passed automated Continuous Integration ("CI") tests, and have been approved by mathlib maintainers.

While you're working on a new contribution to mathlib, you should do this on a different branch. You should do this in your own fork of the mathlib repository.

Typical workflow:

Making a Pull Request (PR) #

Once you're happy with your local changes, it's time to make a pull request.

Moves:

Deletions:

Any other comments you want to keep out of the PR commit should go below the ---.

Lifecycle of a PR #

Many reviewers use the review queue to identify PRs that are ready for review. The instructions below will ensure that your PR appears on that queue; if it doesn't appear there it may not receive much attention. Everyone is also invited to regularly look at the queue (it is linkified as #queueboard on Zulip), and write reviews of PRs within their expertise. You can check if your PR is on the queue, and if not, what is needed to get it on.

The review queue is controlled by GitHub "labels". On the main page for a PR, on the right-hand side, there should be a sidebar with panels "reviewers", "assignees", "labels", etc. Click on the "labels" header to add or remove labels from the current project. Labels can only be edited directly by "GitHub collaborators", which is approximately the same as "people who have write access". However, anyone can add/remove the labels below by writing the following commands in a comment on the PR (each on its own line):

This list is exhaustive. If you would like to add a different label, please, bring it up on Zulip!

If your PR builds (has a green checkmark), someone will "review" it within a few weeks (depending on the size of the PR; smaller PRs will get quicker responses). They will probably leave comments and add the label "awaiting-author". You should address each comment, clicking the "resolve conversation" button once the problem is resolved. Ideally each problem is resolved with a new commit, but there is no hard rule here. Once all requested changes are implemented, you should remove the "awaiting-author" label to start the process over again.

There are different groups of people that can review your PR: anyone, reviewers and maintainers. Anyone who has something useful to say can review your PR. If they think your PR is ready to move to the next stage, they might leave an "approving" review on GitHub. These reviews are taken into account by reviewers. If a reviewer considers your PR ready to be merged, they will add the "maintainer-merge" label to your PR. These are used by maintainers to prioritize their review. Maintainers are always the ones to give final approval. Maintainers have reviewer rights, but also further powers (such as merging PRs). Depending on availability, a maintainer could be the first reviewer to look at your PR: in this case, your PR could get merged without being "maintainer merge"d first. Review times can vary depending on availability of our volunteers. To speed up the process, you can look at the review guidelines and try to make sure your PR adheres to them. If you want to explicitly ask for a review, please create a topic in the PR reviews stream on Zulip.

If a maintainer has approved your PR, a "ready-to-merge" label is automatically applied to the PR. A bot called bors will take it from here. (See here for more detail about bors.) The PR will get added to the "merge queue". The merge queue is processed automatically, but this takes some finite amount of time as it requires building branches of mathlib.

In some cases, a maintainer will "delegate" the PR. You'll see that your PR now has a "delegated" label. This either means that there are a few final changes requested, but that the maintainer trusts you to make these and send the PR to bors yourself, or that the maintainer wants to give you one final chance to look things over before the PR is merged. In either case, when you are ready, writing a comment containing the line "bors merge" will result in the PR being merged.

Here are some other frequently-used labels:

Dealing with merge conflicts #

Due to the fact that multiple people work on mathlib in parallel, someone might have introduced a change on master that conflicts with a change that you're proposing on your PR. If it happens with your PR, a bot will automatically add the "merge-conflict" label, and your PR will not appear on the review queue. Check this GitHub tutorial on how to resolve merge conflicts by using their online tool. Once the conflict has been resolved, the "merge-conflict" label will automatically be removed, and your PR will return to the review queue.