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é |
Outside these dates, we meet in SR 3 during seminar hours, to discuss and work on Lean projects. Feel free to join if you are interested!
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
HoTT and HoTTLean.
In this talk, I will speak about homotopy type theory (HoTT), a proof system that is motivated by topological intuition and has practical convenience, and the HoTTLean project. The aim of HoTTLean is to build a theorem prover for HoTT in the existing theorem prover Lean, by combining formalization and meta-programming features. Motivated by a philosophical discussion, I will introduce the necessary HoTT prerequisites for understanding the idea of the HoTTLean project. I will then present the problem we are attacking and explain our solution via the so-called synthetic approach. After that, I present the construction of the groupoid model of type theory, which plays a central role in our project. By discussing specific issues arising in the formalization of the groupoid model, I address possible ways to tackle the general problem of dependent rewriting in Lean.
Sára Juhošová (Delft) - 13.01.2026
The Human Side of Interactive Theorem Provers.
Interactive theorem provers (ITPs) such as Agda, Coq/Rocq, and Lean are currently being used by mathematicians to formalise their proofs, by developers to verify parts of their programs, and by computer science researchers to better understand type theory and ITPs themselves. ITPs promise strong correctness guarantees and can even help developers reason about how to design their programs. Unfortunately, they are also notorious for their steep learning curves and poor usability, effectively preventing them from spreading to a wider userbase and making them difficult to teach in courses. I will talk about the current obstacles that new and experienced users of ITPs face, but also discuss how the different user bases of individual ITPs can affect their design and focus. I will also compare ITPs to other, more mainstream programming languages and reflect on how their ecosystems affect their usability.
Anatole Dedecker (Paris) - 03.02.2026
TBA.