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) |
| 12.05.2026 | Andrés Goens | TU Darmstadt |
| 16.06.2026 | Yannick Forster | 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.
Andrés Goens (Darmstadt) - 12.05.2026
Towards Blackboard-Style Reasoning in Interactive Theorem Provers
Reasoning in mathematical proofs needs high-level abstractions. When used to communicate between experts, arguments often take advantage of intuitions, shared context and experience. This often means leaving out many details that are unimportant to communicate effectively, but would be necessary for a machine-checked proof. In this talk I will lay out a vision for diminishing this gap and reconstructing machine-checkable proofs from high-level arguments. We will focus concretely on equational reasoning, informally, when reasoning about large chains of equations. I will present an approach that lets us write high-level proof sketches, and reconstruct missing assumptions and steps, in the Lean proof assistant.