Informal Formalization Seminar

The Informal Formalization Seminar is a quasi-regular seminar on formalization of mathematics and adjacent subjects. It is organized by Sander Dahmen (VU) and Johan Commelin (UU).

Next seminar | Future seminars | Past seminars

# Next seminar

08 Mar 2024, VU Amsterdam

Location: New University Building (NU), room 09A46

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.

  1. The Univalence Principle (2022). Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis. To appear in Memoirs of the AMS (arXiv:2102.06275).
  2. Univalent Double Categories (2023). Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North. To appear in the proceedings of CPP 2024 (arXiv:2310.09220)
  3. Insights From Univalent Foundations: A Case Study Using Double Categories (2024). Nima Rasekh, Niels van der Weide, Benedikt Ahrens, Paige Randall North. (arXiv:2402.05265)

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.

# Future seminars

Session in the fall of 2024 will be announced in due time.

# Past seminars

29 Jan 2024, VU Amsterdam

Special session at the occasion of the PhD defense of Anne Baanen

Location (only for the talk below): Main Building (HG), room 09A33

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.

19 Jan 2024, Utrecht

Location: Minnaert, Room 2.02

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.