Formalisation of mathematics has seen a recent explosion of activity. The Lean proof assistant has been used to formalise Fields-medal winning mathematics and papers in the Annals of mathematics. Some papers have been formalised before their referee report arrived, or even before the final manuscript was submitted. Formalisation has great potential to change how mathematics is done. Scaling to "research papers can routinely be formalised" requires library building: adding key definitions and building supporting theory around them.
During this workshop, we will focus on advancing Mathlib, Lean's curated integrated library of formalized mathematics. Most of the time is reserved for working in small groups, on new or pre-existing projects adding to Mathlib. There will be time to discuss cross-cutting concerns, a social event and time to connect as a community. Participants are expected to have prior experience in contributing to Mathlib.
The deadline for the application for participation is December 18th, 2026.
Our Global Mobility Fellowships provide participation opportunities for selected researchers and PhD students from countries of the Global South in the Special Topic Schools of the Hausdorff School for Mathematics. For more information, please visit our website.
Scientific Organizers:
- Floris van Doorn (University of Bonn)
- Michael Rothgang (University of Bonn)