Research Seminar on Formal Mathematics
Heidelberg University - Winter semester 2024-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 4 (SR 4, INF 205).
Schedule
| Date | Speaker | Institution |
|---|---|---|
| 22.10.2024 | María Inés de Frutos Fernández | Universität Bonn |
| 05.11.2024 | Riccardo Brasca | Université Paris-Cité |
| 17.12.2024 | Jannis Limperg | LMU München |
| 21.01.2025 | Nirvana Coppola | Università di Padova |
| 04.02.2025 | Matthieu Piquerez | Université de Nantes |
Titles and abstracts
María Inés de Frutos Fernández (Bonn) - 22.10.2024
Formalizing the divided power envelope in Lean.
Given an ideal \(I\) in a commutative ring \(A\), a divided power structure on I is a collection of maps \(\gamma_n : I \to I\) indexed by \(\mathbb{N}\) which behave like the family \(x^n/n!\), but which can be defined even if the characteristic of A is positive. From a divided power structure on \(I\) and an ideal \(J\) in an \(A\)-algebra \(B\), one can construct the “divided power envelope” \(D_B(J)\), consisting of a \(B\)-algebra \(D\) with a given ideal \(J_D\) and a divided power structure satisfying a universal property and a compatibility condition. The divided power envelope is needed for the highly technical definition of the Fontaine period ring \(B_{cris}\), which is used to identify crystalline Galois representations and in the comparison theorem between étale and crystalline cohomology.
In this talk I will describe ongoing joint work with Antoine Chambert-Loir towards formalizing the divided power envelope in the Lean 4 theorem prover. This project has already resulted in numerous contributions to the Mathlib library, including in particular the theory of weighted polynomial rings, and substitution of power series.
Riccardo Brasca (Paris) - 05.11.2024
Formalization of Fermat’s Last Theorem for regular primes and algebraic number theory in Lean.
I will describe a recently finished project whose goal was to formalize, in the Lean4 theorem prover, the regular case of Fermat’s Last Theorem. This is an important 19th century result that motivated the development of modern algebraic number theory. Our formalization includes a proof of Kummer’s lemma, which is the main obstruction to this theorem. Rather than following the modern proof of Kummer’s lemma via class field theory, we prove it by using Hilbert’s Theorems 90-94 in a way that is more amenable to formalization. We will also explain how our work has improved the situation of formalized algebraic number theory in general.
Jannis Limperg (München) - 17.12.2024
Aesop: White-Box Proof Search for Lean.
I will present Aesop, a pragmatic, highly customisable proof search tactic for Lean that is used extensively in Mathlib and other Lean projects. We will first consider Aesop from a user’s perspective, discussing how Aesop searches for proofs and how it can be customised to find proofs in specific problem domains. Afterwards (time permitting) we will discuss a recently completed, substantially faster reimplementation of Aesop’s forward reasoning.