Mathlib Reviewer Bootcamp 2026 (MRB2026)
The first ever edition of the Mathlib Reviewer Bootcamp will be a four days workshop hosted at Stockholm University in Stockholm, Sweden on 30th March-2nd April 2026.
Its goal is to make existing Lean experts proficient at reviewing pull requests to Mathlib, the mathematics library of Lean 4.
Why
The growth of Mathlib is currently bottlenecked by the slowness of the review process. It can take upwards to months for some contributors’ work to even be looked at.
The Mathlib Initiative is one answer to this problem, by allowing existing reviewers to spend more time reviewing. However, this doesn’t solve the underlying problem of the imbalance of our community towards newcomers created by the huge rise of interest in formalisation in recent years.
We must also strengthen the newcomer-to-contributor-to-reviewer pipeline. The first step of this pipeline is now widely ensured through both in-person mentoring at universities and online through the review process. The second step of this pipeline, however, currently is a solitary process of learning by doing with no mentoring nor learning resources available.
We are a small group of expert reviewers who want to divert the trend by passing on our hard-learned reviewing knowledge and skills
What
The workshop will consist of lectures on reviewing practices (style, etiquette…) and tool proficiency (vscode, github), followed by practice sessions in small groups of mentees/mentors.
The mentorship started then is planned to continue over several months.
Schedule
All activities take place at Stockholm University in Albano. The Cramér room is in House 1, Floor 3, outside the maths department. The Mittag-Leffler room is in House 1, Floor 3, inside the maths department. Lärosal 25 and 26 are in House 4, Floor 2. Hörsal 6 is in House 4, Floor 3.
| Time | Monday | Tuesday | Wednesday | Thursday |
|---|---|---|---|---|
| 09:00-11:45 | Arrival Cramér room |
Lectures Lärosal 25 |
Group session Mittag-Leffler room |
Group session Lärosal 26 |
| 11:45-13:15 | Lunch | Lunch & Group photo | Lunch | Lunch |
| 13:15-17:00 | Lectures Cramér room |
Group session x SLUG Mittag-Leffler room |
Lectures Hörsal 6 |
Departure |
The three sets of lectures will be as follows:
| Speaker | Monday | Tuesday | Wednesday |
|---|---|---|---|
| Andrew | The six stages of reviewing Overview of the various considerations that go into accepting a PR |
How to fool authors into writing lemmas they need Using the right lemmas and tactics, identifying missing API, splitting off lemmas |
How to fool authors into writing lemmas they don’t need Normal forms, syntactic generality, fintype vs finite; implicit arguments, naming convention, imports, file structures |
| Michael | Behind the scenes: orchestrating the review load The purpose of code review; organisation into reviewers and maintainers; some current challenges; auto-assignment; the queueboard; triage |
Tooling for reviewers; review etiquette The different kinds of linters (and how to deal with them); CI checks; tracking tech debt; the summary comment to surface such changes; labels; benchmarking bot. Dependent issues; deprecations. (if time permits) Principles for refactoring, clean-up and tech debt changes, review etiquette (“how to be the minimally nice reviewer”) |
Code style and golfing advice |
| Yaël | Git concepts, VSCode practice Mental model for how git works and useful commands to know; relevant VSCode extensions and how to use them |
Style theory Syntactic vs semantic naming, constructor vs inheritance, argument implicitness, reducibility, visibility |
Prestodigitation Advanced VSCode shortcuts |
Organisers
This event is organised by Yaël Dillies and Andrew Yang, with additional help from Michael Rothgang.
Participants
The current list of confirmed participants is as follows:
| Participant | Affiliation |
|---|---|
| Fernando Chu | Utrecht University |
| William Coram | University of East Anglia |
| Raphael Douglas Giles | Utrecht University |
| Rida Hamadani | Université de Pau et des Pays de l’Adour |
| Christopher Henson | Drexel University |
| Michail Karatarakis | Radboud University Nijmegen |
| Arend Mellendijk | Rheinische Friedrich-Wilhelms-Universität Bonn |
| Hampus Nyberg | Stockholm Universitet |
| Felix Pernegger | Rheinische Friedrich-Wilhelms-Universität Bonn |
| Wrenna Robson | University of Bristol |
| Olivia Röhrig | Technische Universität Berlin |
| Hannah Scholz | Rheinische Friedrich-Wilhelms-Universität Bonn |
| Kexing Ying | École Polytechnique Fédérale de Lausanne |
| Wenrong Zou | Rheinische Friedrich-Wilhelms-Universität Bonn |
Applications
The ideal applicant should have a solid knowledge of Lean and a track record of contributions to Mathlib (at least 10 PRs merged, as a rule of thumb). They should furthermore be motivated to advance the community through reviewing and in particular be ready to dedicate time to it in the future. To ensure appropriate mentoring, we will prioritise applicants interested in combinatorics, order theory, convex analysis, commutative algebra, algebraic geometry, category theory, differential geometry, topology, metaprogramming.
Applications are now closed.
Funding
This event is made possible by the funding from Kungliga Vetenskapsakademien (KVA) and the Mathlib Initiative (a program of Renaissance Philanthropy).