Research Seminar on Formal Mathematics
Heidelberg University - Summer semester 2025
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 3 (SR 3, INF 205).
Schedule
| Date | Speaker | Institution |
|---|---|---|
| 15.04.2025 | Filippo Nuccio | Université Jean Monnet (Saint-Étienne) |
| 13.05.2025 | Kevin Klinge | Karlsruher Institut für Technologie |
| 01.07.2025 | ||
| 15.07.2025 | Chelsea Edmonds | University of Sheffield |
Titles and abstracts
Filippo Nuccio (Saint-Étienne) - 15.04.2025
Formalizing local fields in Lean.
In this talk, I will start with a very gentle, and brief, introduction to Lean and to Mathlib, and then will move on to discuss a joint with M. I. de Frutos Fernández about the formalisation of the local fields. Although some basic results concerning general valuation rings and normed field have been in mathlib for a while, this work introduces for the first time the notion of discrete valuation and local fields, and connects them to the main results about discrete valuation rings. We rely crucially on recent works about completion of Dedekind Domains at prime ideals and, as an application, we formalise the proof that Laurent series are the completion of the field of the rational functions and we propose an equivalent definition of the p-adic numbers working directly with the p-adic valuation rather than starting from the R-valued p-adic metric.
Kevin Klinge (Karlsruhe) - 13.05.2025
Ore localisation.
The Ore localisation is a well established construction, which may be seen as the non-commutative analogue of the field of fractions. However, to my knowledge, until recently, there was no published written proof of it’s well-definedness, that is both complete and correct. In this talk, I will speak about my experience formalising the Ore localisation in Lean. After briefly discussing the subject itself, we will have a look at the proof and why it is so difficult for a human to get right. Along the way, I will share some of my insight gained during the project, as well as some practical tips, with which I hope to inspire you to also try your own formalisation projects. This talk is based on joint work with Jakob von Raumer.