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 | Goethe-Universität Frankfurt |
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.
Nirvana Coppola (Padova) - 21.01.2025
Formalisation of mathematics and number theory in Lean.
In this talk, I will give some motivation on the usefulness of formalisation of mathematics, focusing on the strength of the proof assistant Lean 4, and in particular its logic, dependent type theory. I will then present a current project I am involved in, the formalisation of Ostrowski’s theorem (a classical result in number theory), showing both the mathematical and the formalisation sides of this work. The project is in collaboration with David Kurniadi Angdinata, Fabrizio Barroero, Laura Capuano, María Inés de Frutos-Fernández, Sam van Gool, Silvain Rideau-Kikuchi, Amos Turchet, Francesco Veneziano.
Matthieu Piquerez (Frankfurt) - 04.02.2025
Formalization of diagram chasing as a first-order logic in proof assistants.
I will present a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language, which features dedicated proof commands to automate the synthesis, and the verification, of the technical parts often eluded in the literature. We aim to build a tool which can be used for a wide variety of formalization projects and which is easy to use (with, e.g., an interactive interface, some automations, and the formalization of some useful helping lemmas, one of them having, up to now and to our knowledge, no formal proof in the litterature). Joint work with Benoît Guillement, Ambroise Lafont and Assia Mahboubi.