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.

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

Team

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

In SuSe 25 the seminar will be Mondays 10-12 in room 0.003.

The Lean hacking session is also planned in the summer semester.

Schedule:

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

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

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