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.10.2025 | Artie Khovanov | University of Edinburgh |
| 18.11.2025 | Christian Merten | Utrecht University |
| 09.12.2025 | Yiming Xu | Ludwig-Maximilians-Universität München |
| 13.01.2026 | Sára Juhošová | Technische Universiteit Delft |
| 03.02.2026 | Anatole Dedecker | Université Paris-Cité |
Titles and abstracts
Artie Khovanov (Edinburgh) - 21.10.2025
Formalising Real Algebra in Isabelle/HOL and Lean.
Real algebraic geometry studies the sets cut out by polynomial inequalities over ordered fields. It is underpinned by real algebra, the study of real closed fields (RCFs), which share many of the algebraic properties of real numbers. The theory has a rich computational component, applied in fields such as robotics. However, little real algebra, let alone any such algorithm, has been formalised in the proof assistants Lean and Isabelle. In this talk, I will discuss and compare my experiences formalising real algebra in two very different contexts: the Archive of Formal Proofs (written in Isabelle/HOL), and Mathlib (written in Lean 4).
Christian Merten (Utrecht) - 18.11.2025
(combined with the 2025 Heidelberg Lean Workshop on Formalising algebraic geometry, 19-21.11.2025)Formalising étale fundamental groups.
When encoding a mathematical concept in a formal language such as Lean, a balance must be struck between following the pen-and-paper presentation, ensuring reusability, and maintaining feasibility. In this talk, after giving a brief introduction to Lean and its mathematical library Mathlib, I will explain how we maintain this balance in Mathlib’s algebraic geometry library through the example of formalising the étale fundamental group of a scheme. This group serves as the starting point for establishing a Galois theory for algebro-geometric objects, building on the framework of Galois categories. I will close with giving some pointers to possible future projects in this area. No prior knowledge of algebraic geometry will be assumed.
Yiming Xu (Munich) - 09.12.2025
TBA.
Sára Juhošová (Delft) - 13.01.2026
TBA.
Anatole Dedecker (Paris) - 03.02.2026
TBA.