Mathlib Reviewer Bootcamp 2026 (MRB2026)
The first ever edition of the Mathlib Reviewer Bootcamp will be a week-long workshop hosted at Stockholm University in Stockholm, Sweden on 30th March-3rd 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.
Tentative schedule
| Time | Monday | Tuesday | Wednesday | Thursday | Friday |
|---|---|---|---|---|---|
| 09:00-09:45 | Lecture | Lecture | Lecture | Lecture | |
| 09:45-10:00 | Break | Break | Break | Break | |
| 10:00-10:45 | Arrival | Lecture | Lecture | Lecture | Lecture |
| 10:45-11:45 | Lecture | Lecture | Lecture | Lecture | Lecture |
| 11:45-13:15 | Lunch | Lunch | Lunch | Lunch | Lunch |
| 13:15-17:00 | Group session | Group session x SLUG | Excursion | Group session |
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.
To apply, please send an email to yael.dillies@math.su.se with subject MRB 2026 - Applicant name by 28th February 2026 containing:
- your review and mathematical interests,
- a short summary of your experience with Lean/Mathlib,
- a few sentences about your motivation.
Once you have been accepted, we will need the following information for the hotel booking:
- your email address
- your date of birth
- your mobile phone number
If you need a visa to visit Sweden, please indicate so in your email. We encourage you to provide all the above information at once so that we can swiftly book your hotel room as support to your visa application.
We will cover accommodation costs for four nights as well as food expenses. The amount of money available to cover travel expenses is limited and we encourage you to seek funding from your home institution. Please let us know in your application if you wish to make use of this money, in particular how much your travels would cost.
Organisers
This event is organised by Yaël Dillies and Andrew Yang, with additional help from Michael Rothgang.
Funding
This event is made possible by the funding from Kungliga Vetenskapsakademien (KVA) and the Mathlib Initiative (a program of Renaissance Philanthropy).