Topics of interest
- Machine-checked mathematics.
- Proof assistants (Agda, Coq, Lean, etc).
- Type theory.
- Univalent foundations.
- Functional programming languages.
Time and place
The Formal Mathematics seminar meets once a month, on Tuesday from 4:15 to 5:45 PM in Seminar Room TBA (SR 3, INF 205).
Schedule
| Date | Speaker | Institution |
|---|---|---|
| 20.10.2026 | Loïc Pujet | Université de Strasbourg |
| 24.11.2026 | Pim Otte | Utrecht University |
| 19.01.2027 (TBC) |
Titles and abstracts
Loïc Pujet (Strasbourg) - 20.10.2026
Revisiting CW complexes in Homotopy Type Theory
CW complexes are spaces which can be built up inductively by gluing together cells of increasing dimension. Due to their good categorical properties, CW complexes have become one of the main objects of interest in algebraic topology. In this talk, I will revisit CW complexes in Homotopy Type Theory (HoTT), a language for higher-dimensional mathematics and synthetic homotopy theory. I will start with a brief introduction to HoTT for the working mathematician, then I will present some joint work with Ljungström on CW complexes in HoTT, and I will conclude with an application of these results in Barton and Campion’s proof of the Serre finiteness theorem.
Pim Otte (Utrecht) - 24.11.2026
Waterproof: An educational proof assistant
Waterproof is an educational proof assistant, built on Rocq and (Verbose) Lean, that we built with the goal to help mathematics students learn the skill of writing mathematical proofs. Through a more approachable interface and the use of controlled natural language, we try to make the feedback a proof assistant provides more accessible for mathematics students. In the first half of this talk, I will briefly demonstrate Waterproof, then discuss the key technical infrastructure and design decisions that drive it. In the second half, I will discuss the educational embedding: How we use it in courses and our observations of students’ proof writing skills with pen and paper following use of Waterproof.