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.
Yannick Forster (Paris) - 16.06.2026
Using proof assistants as more than checkers, and how to write papers about it
I will give a personally biased overview of projects where proof assistants were used as more than proof checkers, covering amongst others results around Hilbert’s tenth problem, the fifth busy beaver value, and computability. I will try to complement this by some general observations how to write up results of research projects involving proof assistants and start a conversation about how this differs from traditional publication processes in maths.
Hannah Scholz (Bonn) - 23.06.2026
Formalising CW-complexes in Lean
CW complexes are a class of topological spaces that are of particular importance in algebraic topology. Intuitively, they are the result of glueing continuous images of discs together along their boundaries. My talk will concern the classical way of defining them, close to Whitehead’s original definition. I will first discuss the definition and give some intuition. Afterwards, I will go into formalising the definition in Lean and technical challenges of the implementation. For example, I will talk about how we manage the interplay between a general and a less-general but significantly simpler definition, specifically with regards to typeclass inference. All the work that I will be presenting was done together with and supervised by Prof. Floris van Doorn.