Next seminar | Future seminars | Past seminars
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.