Next seminar | Future seminars | Past seminars
Assia Mahboubi (Inria/VU Amsterdam), Machine-checked diagram chasing
Abstract: Diagrams play a central role in category theory, for they provide such an efficient way of delivering convincing enough proofs. For instance, chasing commutative sub-diagrams in a larger diagram provides an elegant alternative to overly technical equational reasoning. Diagram chasing actually refers to a central technique in homological algebra. In this context, diagram chases over Abelian categories are used for proving the existence, injectivity, surjectivity of certain morphisms, the exactness of some sequences, etc. However, complex diagram chases only remain readable at the price of hiding non-trivial technical arguments and are, in practice, challenging to rigorously verify by hand. In this talk, we will present a work in progress towards building a computer-aided tool for writing and for verifying proofs by diagram chasing. It is based on the deep-embedding of a simple first-order language into the dependent type theory rooting proof assistants like Coq/Rocq or Lean. This is a joint work with Ambroise Lafont (École polytechnique, France) and Matthieu Piquerez (Goethe-Universität, Frankfort, Germany).
Short break
María Inés de Frutos-Fernández (University of Bonn), Formalizing the divided power envelope in Lean
Abstract: 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.
Coffee break
Andrew Yang (Imperial College London), Towards R = T in Lean 4: Patching
Abstract: Patching (or "Taylor-Wiles systems") is one of the many ingenious ideas introduced in Wiles' and Taylor-Wiles' groundbreaking papers on the modularity of elliptic curves. This technique was later refined by Diamond, Fujiwara, and Kisin to simplify proofs and relax conditions on inputs. In this talk, we will outline how patching is formalized in Lean 4, building on Scholze's reformulation using ultraproducts. We will also discuss its role in the ongoing effort to formalize Fermat's Last Theorem.
Jiang Jiedong (Peking University + Utrecht University), The Formalization of Fontaine-Wintenberger Theorem in Lean 4
Abstract: The Fontaine-Wintenberger theorem is a cornerstone in p-adic Hodge theory. Recently, Scholze’s perfectoid theory has provided a new interpretation and a new approach to proving the FW theorem. In this talk, I will outline the key components of this modern proof, and explain the role of almost mathematics, perfectoid fields and other ingredients in the proof. Meanwhile, I will discuss the (ongoing) implementation of each part in Lean.
Coffee break
Jim Portegies (TU Eindhoven), The real interpolation theorem for the Carleson project
Abstract: In this talk I will report on my first steps in lean: For the Carleson project I proved a version of the Marcinkiewicz real interpolation theorem. I will talk both about process and content: I will share some of my struggles, but also how some detours eventually led to a proof of a more general version of the theorem.
Christian Merten (Heidelberg University), Towards étale fundamental groups - Galois categories in Lean4
Abstract: The étale fundamental group of a scheme is an important tool in algebraic geometry and its underlying categorical framework is the notion of a Galois category. In my talk I will discuss the setup that is implemented in Mathlib and give an overview on the recently completed formalization of the main theorem on Galois categories. I will also give an outline on the next steps towards a formal proof of the fundamental exact sequence on arithmetic and geometric fundamental groups.
Short break
Paige North (Utrecht University), Perspectives on the univalence principle
Abstract:
Formalizing mathematics in UniMath (a Coq library based on univalent foundations
/ homotopy type theory) has one important advantage in particular: mathematical
structures often automatically validate the "Univalence Principle" and thus also
the “Equivalence Principle”. This gives formalizing categorical concepts in
UniMath at least one advantage over developing them in classical mathematics.
The Equivalence Principle is an informal principle asserting that equivalent
mathematical objects have the same properties. For example, group theory has
been developed so that isomorphic groups have the same group-theoretic
properties, and category theory has been developed so that equivalent categories
have the same category-theoretic properties (though sometimes other, ‘evil’
properties are considered). Vladimir Voevodsky established Univalent Foundations
as a foundation of mathematics (based on dependent type theory) in which the
Equivalence Principle for types (the basic objects of type theory) is a theorem.
Later, versions of the Equivalence Principle for set-based structures such as
groups and categories were shown to be theorems in Univalent Foundations. In
[1], we formulate and prove versions of the Equivalence Principle for a large
class of categorical and higher categorical structures in Univalent Foundations.
In [2] and [3], we take a different perspective on the same phenomenon.
Motivated by a desire to organize the zoo of mathematical notions related to
double categories, we show that the different notions of double categories
present in the classical literature correspond to different notions of
equivalence between double categories. We illustrate that one can first write
down a definition of a categorical structure and then ask what the corresponding
equivalences are, as done in [1], or one can start with the desired notion
equivalence and design a corresponding categorical structure.
Coffee break
Floris van Doorn (University of Bonn), The Sobolev inequality in Lean
Abstract: When solving partial differential equations, it is easier to find so-called weak solutions, and then one can later prove that a weak solution is in fact an actual solution to the PDE. A key ingredient in this process is the Sobolev inequality. Heather Macbeth and I have formalized a version of the Sobolev inequality, namely the Gagliardo–Nirenberg–Sobolev inequality. In the formalization we have developed a nice technique of working conveniently with iterated integrals and Fubini's theorem in a product of more than two spaces, greatly simplifying some existing formalizations that involve Fubini's theorem in such product spaces.
Kevin Buzzard (Imperial College London), How to prove Fermat's last theorem
Abstract: Fermat's Last Theorem was proved by Wiles and Taylor in the 1990s, and now there are several known routes to the summit. The question of teaching the proof to a computer proof assistant was raised in the 1990s but back then the technology was not mature enough. I now believe that it is, and in 2024 I will be leading a project to formalise the proof in the Lean proof assistant. In my talk I will explain what the landscape of computer proof assistants looks like in 2024, and I will say something about the route we'll be taking and the practicalities involved in such a large project. The talk will be a general audience talk -- no background in either the theory of proof assistants or the mathematics behind Fermat's last theorem will be assumed.
Oliver Nash (Imperial College London), Toward the classification of semisimple Lie algebras in Lean
Abstract: I will discuss the theory of Lie algebras as formalised in Lean's mathematics library, Mathlib. As often in formal mathematics, it has proved worthwhile to develop the theory at a level of generality beyond what is found in standard foundational texts. I will share some examples of the impact this has had on Mathlib. I will also outline approximately how much work remains until we can add a complete formal proof of the Cartan-Killing classification to the library.
Coffee break
Alain Chavarri Villarello (Vrije Universiteit Amsterdam), Formally certifying rings of integers in Lean
Abstract: The ring of integers of a number field K is the subring consisting of elements in K that are zeros of monic polynomials with integer coefficients. It is a central object in algebraic number theory and its explicit determination is relevant for numerous applications. Multiple algorithms exist to compute this ring, including the so-called Round 2 algorithm. In this talk, we will look into the formalization in the Lean theorem prover of the theoretical foundations for this algorithm. This includes the Pohst-Zassenhaus theorem and Dedekind's criterion, which, as we will see, also hold in a more general setting. We will then discuss a formal certificate for the ring of integers based on these results, which works locally prime-by-prime and only requires the verification of simple equalities.