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 the course repository. There are also other ways of learning Lean.
Mailing List
Subscribe to our mailing list here. We will send 1-2 emails per week about the activities of the formalization group, including the seminar schedule.
There is also a low-traffic private channel for Lean in Bonn on Lean’s Zulip Chat. Please send me a message to get access.
Team
Students
Students supervised within the formalized mathematics group:
- Samantha Naranjo Guevara (master, main supervisor: Michael Rothgang)
- Hannah Scholz (master, main supervisor: Michael Rothgang)
- Mara Silge (bachelor, main supervisor: Floris van Doorn)
- Shuhan Wang (master, main supervisor: Floris van Doorn)
- Joshua Wirtz (bachelor, main supervisor: Peter Koepke)
- Maša Žaucer (master, supervisors: Floris van Doorn and Giles Gardam)
- Wenrong Zou (master, main supervisor: María Inés de Frutos-Fernández)
Student research assistants:
- Alexander Brodbelt Lopez
- Leo Diedering
- Pan Lin
- Felix Pernegger
Seminar
In SuSe 26 the seminar will be Thursdays 10:15-12:00 in seminar room 0.007 at Endenicher Allee 60. Feel free to join, even if you’re not part of the formalization group!
- 16.4. Hacking session
- 23.4. Lua Viana Reis: An overview of Ergodic theory in Mathlib
- 30.4. Joshua Wirtz: Mathematical Text Correctness: Theory and Practical Verification
- 07.5. No seminar. Replacement: Floris van Doorn will give a job talk 9:00-10:00 in the Lipschitz Room.
- 14.5. No seminar (Ascension day)
- 21.5. Leo Diedering: TBD
- 28.5. No seminar (Pentecost)
- 04.6. No seminar (Corpus Christi)
- 11.6. TBD
- 18.6. TBD
- 25.6. Probably no seminar (part of the group is traveling)
- 2.7. Probably no seminar (part of the group is traveling)
- 9.7. Hannah Scholz: the
grind tactic
- 16.7. TBD
- 23.7. TBD
If you would like to get reminders about the seminar and other activities of the formalization group, you can subscribe to our mailing list here.
Lean hacking session
The Lean hacking session is a weekly informal meeting. There will be cookies! You are welcome to join, independent of your experience with Lean, to ask questions or for support needed during a formalization.
In SuSe 26 the time is Fridays 14:15-16:00 in seminar room 0.006, starting the second week of the semester.
Courses
Papers/preprints
- Sven Manthe A formalization of Borel determinacy in Lean, Annals of Formalized, Volume 2 (2026). arXiv
- María Inés de Frutos-Fernández, Daniel Macias Castillo and Daniel Martínez Marqués, The refined class number formula for Drinfeld modules, 2025. Accepted to Compositio Mathematica. arXiv
- Antoine Chambert-Loir and María Inés de Frutos-Fernández, Formalizing Polynomial Laws and the Universal Divided Power Algebra, 2025. Accepted to the 15th ACM SIGPLAN International
Conference on Certified Programs and Proofs (CPP ‘26). Online abstract, arXiv
- Anne Baanen, Matthew Robert Ballard, Bryan Gin-ge Chen, Johan Commelin, Michael Rothgang and Damiano Testa. Growing Mathlib: maintenance of a large scale mathematical library, 2025. 18th Conference on Intelligent Computer Mathematics (CICM ‘25). Journal version, arXiv
- Antoine Chambert-Loir and María Inés de Frutos-Fernández, A Formalization of Divided Powers in Lean, 2025. 16th International Conference on Interactive Theorem Proving (ITP ‘25). Conference proceedings, arXiv
- Lars Becker, María Inés de Frutos-Fernández, Leo Diedering, Floris van Doorn, Sébastien Gouëzel, Asgar Jamneshan, Evgenia Karunus, Edward van de Meent, Pietro Monticone, Jasper Mulder-Sohn, Jim Portegies, Joris Roos, Michael Rothgang, Rajula Srivastava, James Sundstrom, Jeremy Tan, Christoph Thiele, A blueprint for the formalization of Carleson’s theorem on convergence of Fourier series, 2025. arXiv
Past students
Students (co-)supervised within the formalized mathematics group or theses that include a Lean component. Between parentheses is the end date.
Master students:
- Henri Nikoleit, Using LLMs To Construct Adversarial Instances in Combinatorial Optimization (2025; supervisor: Heiko Röglin); GitHub (1, 2, 3), thesis
- Izabela Mandla, Formalisation of the Walsh-Carleson Theorem (2025; supervisors: Floris van Doorn and Christoph Thiele); GitHub, thesis
- Gabin Kolly, Fraïssé limits in Lean (2025; supervisor: Philipp Hieronymi); GitHub, thesis
- Kunhong Du, On the Formalization of the Simplicial Model of HoTT (2025; supervisor: Floris van Doorn); GitHub, thesis
- Tim Lichtnau†, Stacks in Synthetic Algebraic Geometry (2024; supervisor: Hugo Moeneclaey); GitHub
- Óscar Álvarez Sánchez, Demazure operators and Lean (2024; supervisor: Catharina Stroppel); GitHub, thesis
- Theofanis Chatzidiamantis Christoforidis, Formalizing Higher Categories (2024; supervisor: Nima Rasekh); GitHub, thesis
Bachelor students:
- Felix Pernegger, Formalisation of the Calderón Transference Principle in Ergodic Theory (2025; supervisor: Floris van Doorn); GitHub, thesis
- Johannes Folttmann, Formalization of the Internal Language of a Topos (2025; supervisor: Floris van Doorn); GitHub, thesis
- Ludwig Monnerjahn, Formalisation of constructable numbers (2024; supervisor: Floris van Doorn); GitHub, thesis
- Hannah Scholz, Formalisation of CW-complexes (2024; supervisor: Floris van Doorn); GitHub, thesis
- Leo Diedering, Contributing to the Formalization of Carleson’s Theorem (2024; supervisor: Floris van Doorn); GitHub, thesis
Past seminar sessions
WiSe 25/26
Time: Tuesdays 10:15-12:00 in seminar room 0.007.
- 14.10. Michael Rothgang: Growing mathlib: fostering the growth of a large formalised mathematics library
- 21.10. No seminar
- 28.10. Arend Mellendijk: Developing a Tactic for Algebraic Normalization
- 04.11. Henri Nikoleit: Using LLMs to construct adversarial instances in combinatorial optimization (master thesis defense)
- 11.11. Jovan Gerbscheid (Cambridge): Improving Lean by metaprogramming
- 18.11. Evgenia Karunus: Paperproof: Visualising Mathematical Proof
- 25.11. No seminar
- 02.12. Filippo Nuccio (U Jean Monnet): Formalising Condensed Mathematics
- 09.12. 9:00-10:15 in the common room of Villa Maria (Endenicher Allee 62) livestream of Leonardo de Moura’s talk The Making of Lean at ItaLean 2025
- 16.12. No seminar
- 23.12. No seminar
- 13.01. Hannah Scholz: CW Complexes in Lean and Wenrong Zou: Formalizing Formal Group Laws
- 20.01. Moritz Firsching (Basel, Google): Formal Conjectures, Autoformalisation & AlphaProof
- 27.01. Oliver Butterley (U Rome Tor Vergata): Large scale verification of production cryptography code using Lean
- 03.02. Christian Merten (U Utrecht): Cohomology theories in algebraic geometry in Lean’s mathematical library mathlib
SuSe 25
Time: Mondays 10:15-12:00 in seminar room 0.003.
- 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. No seminar
- 30.6. Henri Nikoleit: Finding new bounds for approximation-algorithms using LLMs and evolutionary search (starts 11:15)
- 07.7. No seminar
- 14.7. Wenrong Zou: A functional equation lemma for formal group laws. and Johannes Folttmann
- 21.7. No seminar
- 28.7. 14:15-16:00. Izabela Mandla: Properties of Walsh Functions in the Proof of a Carleson Theorem Analogue and Felix Pernegger: Layer cake overkill: Formalization of generalized independence systems
- 1.9. 10:15-11:00 Thesis defense Johannes Folttmann (in room 0.003 as usual)
- 15.9. 16:00-17:00 Thesis defense Izabela Mandla (in room 0.003 as usual)
- 17.9. 15:15-16:15 Thesis defense Felix Pernegger (in room 0.003 as usual)
WiSe 24/25
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