The second edition of the Mathlib Reviewer Bootcamp will be a five days workshop hosted at Alanus Werkhaus in Alfter, Germany (near Bonn) on 18th-22nd January 2027.

Its goal is to make existing Lean experts proficient at reviewing pull requests to Mathlib, the mathematics library of Lean 4.

See information about the first edition here.

Why

The growth of Mathlib is currently bottlenecked by the slowness of the review process. It can take more than a month 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 Alanus Werkhaus.

Rooms and timetable to be announced.

Organisers

This event is organised by Yaël Dillies, Arend Mellendijk and Dr. Michael Rothgang, with additional mentorship provided by Monica Omar and Christian Merten.

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, analytic number theory, differential geometry, topology, metaprogramming, functional analysis, algebra, algebraic geometry.

Applications are open until 31st October 2026 Anywhere on Earth. Please fill in this form. If you need a visa for Germany, please contact one of the organisers directly (as well as filling in the form) so that we prioritise providing you with an invitation to the workshop and travel funding.

Funding

This event is funded by the University of Bonn as a Junior Research Retreat.

We will cover accommodation costs and meals taken during the retreat. We are expecting to be able to cover travel costs as well, but the funding for this has yet to be confirmed.