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
Students
Students supervised within the formalized mathematics group:
- Izabela Mandla (master)
- 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)
Student research assistants:
- Leo Diedering (master)
- Hannah Scholz (master)
Seminar
In SuSe 25 the seminar will be Mondays 10:15-12:00 in seminar room 0.003.
Schedule:
- 07.4. No seminar
- 14.4. Hannah Scholz: Formalizing CW Complexes
- 21.4. No seminar (Easter Monday)
- 28.4. Michael Rothgang: Formalising bordism theory: a test of mathlib’s differential geometry library and Johannes Folttmann: internal language of a topos
- 05.5. Jim Portegies (Eindhoven University of Technology): The real interpolation theorem for the Carleson project
- 12.5. Wenrong Zou: Formalizing one-dimensional formal group laws and Izabela Mandla: Formalization of Walsh-Fourier series’ analogue of Carleson’s theorem
- 19.5. María Inés de Frutos Fernández: The Carleson project and Felix Pernegger: Formalization of the Calderón Transference principle
- 26.5. No seminar
- 02.6. Sam Lindauer (Utrecht University): The Formalisation of Differential Forms
- 09.6. No seminar (Pentecost break)
- 16.6. No seminar
- 23.6. Izabela Mandla: TBD
- 30.6. TBD
- 07.7. TBD
- 14.7. Wenrong Zou: TBD
Lean hacking session
The Lean hacking session is a weekly informal meeting on Fridays 14:15-16:00 in seminar room 0.006. There will be cookies! You are welcome to join, independent of your experience with Lean, to ask questions or for support needed during a difficult formalization.
- There will be no hacking session on 13.6.
Courses
Papers/preprints
- 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:
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