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 and improving the ergonomics of formalisation. Fortunately, Lean can be extended using *metaprogramming*: this can be used to recognise and fix problematic patterns in code (linter) or to automate constructions currently done by hand.
This school offers an introduction to metaprogramming, allowing you to get hands-on experience under the guidance of expert tutors. A series of lectures will explain the topic systematically, with plenty of time left for problem-solving and first small projects. You can suggest your own project topic if you like.
Participants are expected to have experience with Lean; no metaprogramming experience is required.
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.
Lecture series by:
- Anne Baanen (Mathlib Initiative)
- Mario Carneiro (Chalmers University of Technology)
- Jovan Gerbscheid (Cambridge)
- Thomas Murrills (Mathlib Initiative)
- Damiano Testa (U Warwick)
- Eric Wieser (Google Deepmind)
Scientific Organizers:
- Floris van Doorn (University of Bonn)
- Michael Rothgang (University of Bonn)