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 |
|---|---|---|
| 21.04.2026 | Joël Riou | Université Paris-Saclay (Orsay) |
| 16.06.2026 | Yannick Forster (tbc) | Inria Paris |
| 23.06.2026 | Hannah Scholz | Universität Bonn |
| 07.07.2026 | Irene Garnelo Abellanas | Universität Paderborn |
Titles and abstracts
Joël Riou (Orsay) - 21.04.2026
Formalization of homotopy theory with Lean
In this talk, I will discuss certain aspects of my formalization in Lean of the verification of Quillen’s axioms of model categories for the category of topological spaces and simplicial sets.