Bonn Formalized Mathematics

offices: Endenicher Allee 62 (the building next to the Math department), rooms 1.001-1.002

This is the webpage for the group on formalized mathematics at the mathematical institute of the university of Bonn. We use the Lean Theorem Prover and its mathematical library to prove current mathematical research, see e.g. the Carleson project.

To learn Lean, try out the Natural Number Game, read the online book Mathematics in Lean or work through my course repository. There are also other ways of learning Lean.

Some communication happens within a private channel on Lean’s Zulip Chat. Please send me a message to get access.

Team

• Floris van Doorn
• María Inés de Frutos-Fernández (postdoc; main area: algebraic number theory)
• Michael Rothgang (postdoc; main area: simplectic geometry)
• Arend Mellendijk (PhD student; main area: analytic number theory)

Students

Students supervised within the formalized mathematics group or doing a Lean project.

• Hannah Scholz (master)
• Izabela Mandla (master, main supervisor: Christoph Thiele)
• Henri Nikoleit (master, main supervisor: Heiko Röglin)
• Wenrong Zou (master, main supervisor: María Inés de Frutos-Fernández)
• Felix Pernegger (bachelor)
• Johannes Folttmann (bachelor)

Ongoing seminar

The usual seminar time is Fridays 14:15-16:00 in room N0.003. There is also a Lean hacking session which is currently scheduled Wednesdays 18:15-20:00 in seminar room 0.006. There will be cookies!

• 18.02 (part of the logic seminar, 11:00 in room N0.003) Gabin Kolly master thesis defense: Fraïssé limits in Lean

Ongoing courses

• SuSe 25: The Logic of Proof Assistants (webpage TBD)

Papers/preprints

incomplete

• Sven Manthe A formalization of Borel determinacy in Lean, 2025. arXiv
• Lars Becker, Floris van Doorn, Asgar Jamneshan, Rajula Srivastava, Christoph Thiele, Carleson Operators on Doubling Metric Measure Spaces, 2024. arXiv

Past students

Students supervised within the formalized mathematics group or theses that include a Lean component. Between parentheses is the end date.

Master students:

• Gabin Kolly, Fraïssé limits in Lean (2025); Github
• Kunhong Du, On the Formalization of the Simplicial Model of HoTT (2025); Github, thesis
• Tim Lichtnau†, Stacks in Synthetic Algebraic Geometry (2024; main supervisor: Hugo Moeneclaey); Github
• Óscar Álvarez Sánchez, Demazure operators and Lean (2024; main supervisor: Catharina Stroppel); Github, thesis
• Theofanis Chatzidiamantis Christoforidis, Formalizing Higher Categories (2024; main supervisor: Nima Rasekh); Github, thesis

Bachelor students:

• Ludwig Monnerjahn, Formalisation of constructable numbers (2024); Github , thesis
• Hannah Scholz, Formalisation of CW-complexes (2024); Github, thesis
• Leo Diedering, Contributing to the Formalization of Carleson’s Theorem (2024); Github, thesis

Past seminar sessions

Usual time: Fridays 14:15-16:00 in room N0.003.

• 18.10 Arend Mellendijk on monadic programming in Lean
• 25.10 Floris van Doorn on metaprogramming in Lean
• 01.11 No seminar
• 08.11 Floris van Doorn on metaprogramming in Lean
• 15.11 Floris van Doorn on metaprogramming in Lean and exercises
• 22.11 Jiang Jiedong: Formalizing the Fontaine-Wintenberger theorem
• 29.11 No seminar
• 06.12 No seminar
• 13.12 No seminar
• 20.12 No seminar
• 10.01 No seminar
• 17.01 No seminar
• 24.01 No seminar
• 31.01 Canceled
• 07.02 Kunhong Du: Formalization of type theory
• 14.02 unusual time and place: 12:15 in the CS Building (room 2.050). Henri Nikoleit on FunSearch
• 14.02 (usual time of 14:15 in room N0.003) Kunhong Du master thesis defense: On the Formalization of the Simplicial Model of HoTT
• 18.02 (part of the logic seminar, 11:00 in room N0.003) Gabin Kolly master thesis defense: Fraïssé limits in Lean

Metaprogramming repository HoTT repository

Past courses

• WiSe 24/25: Formalized Mathematics in Lean
• SuSe 24: Collaborative Formalization in Analysis
• WiSe 23/24: Formalized Mathematics in Lean