ICMS 2024 - Session 2: Novel Formalisations of Mathematics in Lean


Aim and Scope

Interactive theorem provers are pieces of software that allow one to express mathematical constructs and arguments and check them interactively. Formalisation, the process of writing mathematical proofs in these systems, is becoming increasingly popular amongst mathematicians. In this session, we will be focusing on the Lean4 theorem prover and exhibit recent novel formalisation projects.


All talks in this session will take place on Thursday, July 25 in MCS3052 at the Department of Mathematical Sciences. The schedule is as follows:

Time Title Speaker
09.00 - 10.00 Plenary talk in MCS0001
10.00 - 10.30 Coffee in front of MCS0001
10.30 - 11.00 Towards a formal proof of the Freyd-Mitchell embedding theorem Markus Himmel
11.00 - 11.30 Formalising Analysis in Lean: Compactness and Dimensionality Dawid Lipinski
11.30 - 12.00 Formalising Families of `l`-adic Galois Representations in Lean 4 Ivan Farabella
12.00 - 12.30 Formalisation of the Category of Hopf Algebras in Lean 4 Yunzhou Xie, Yichen Feng, Yanqiao Zhou
12.30 - 13.30 Lunch in front of MCS0001
13.30 - 14.00 Protein folding by recursive backtracking Bjørn Kjos-Hanssen
14.00 - 14.30 Stacks in Lean Calle Sonne, Paul Lezeau
14.30 - 15.00 Groups of order `p * q` Peiran Wu
15.00 - 15.30 Formalization of the Existence of Frobenius Elements Jou Glasheen
15.30 - 16.00 Coffee in front of MCS0001

Titles and Abstracts

Towards a formal proof of the Freyd-Mitchell embedding theorem

Lean’s mathlib currently provides several tools to facilitate diagram chasing in general abelian categories, but they suffer from deficiencies which make their application less straightforward than simply adapting an elementwise proof in a category of modules.

I will report on an ongoing project to formalize a proof of the Freyd-Mitchell embedding theorem, which states that every small abelian category can be embedded into a category of modules. This theorem vastly strengthens the existing diagram chasing techniques.

The project has several interesting properties: it is being carried out entirely in the form of pull requests to mathlib, with only minimal amounts of code that is not merged at any time. We carefully selected a proof strategy that works well for mathlib, deducing the embedding theorem from various general theories that are useful outside of the embedding theorem. In set-based mathematics, the embedding theorem is accompanied by a “meta-theorem” explaining how the embedding theorem can be applied. I will explain how Lean’s universes alleviate the need for such a meta-theorem in the formal setting.

Formalising Analysis in Lean: Compactness and Dimensionality

The theorem that a closed unit ball is compact if, and only if, its vector space is finite-dimensional showcases how unintuitive infinite dimensional spaces can be. Many proofs skip over what’s considered obvious, leaving readers unaware of the underlying assumptions until they attempt formalization. We will begin the talk by proving a particular formulation of Riesz’s lemma in Lean. We will then use it to construct a sequence in the unit ball where the distance between all elements is 1 and show that such a sequence cannot contain a convergent subsequence. Subsequently, we’ll establish that a closed unit ball is not sequentially compact. A significant challenge we encountered during this proof was the necessity to define the sequence through strong recursion, which posed some difficulties in its formalisation. We hope this talk will showcase Lean’s role in enhancing understanding and generalization of proofs by prompting us to explore broader definitions and theorems within the Mathlib library.

Formalising Families of l-adic Galois Representations in Lean 4

Families of l-adic Galois representations are an important tool in modern algebraic number theory. Andrew Wiles used families of representations associated with elliptic curves to prove Fermat’s Last Theorem and the Langlands philosophy conjectures a deep connection to the theory of automorphic forms. We formalise of the definition of families of l-adic Galois representations as well as the definition of compatibility on them for the first time in an interactive theorem prover and discuss the formalisation process.

Formalisation of the Category of Hopf Algebras in Lean 4

This project delves into the progression of algebraic structures from coalgebra and bialgebra to Hopf algebra, with a special focus on affine group schemes. A key aspect of our study is the group structure that arises from Hopf algebra homomorphisms and the categorization of Hopf algebra, particularly their role within monoidal categories. Additionally, we aim to thoroughly investigate affine group schemes, examining their categorical representation and the implications of their anti-equivalence with commutative Hopf algebra, employing the Lean theorem prover for all formalizations.

  1. Coalgebraic and Bialgebraic Foundations:
    1. To explore and formalize Coalgebra and Bialgebra within Lean, detailing their foundational properties, homomorphisms, and equivalence relations, setting the stage for the progression to more complex algebraic structures.
    2. This exploration naturally extends to Hopf algebra, illustrating the seamless progression within the algebraic hierarchy from coalgebra and Bialgebra to Hopf algebra.
  2. Group Structure in Hopf Algebra Homomorphisms:
    1. To rigorously investigate the group structure that emerges from algebra homomorphisms between Hopf algebra and algebra, emphasizing its pivotal role in algebraic studies.
    2. To formalize the conditions that allow these homomorphisms to form a group, particularly focusing on the existence of inverses and the identity element.
  3. Formalization and Extension of Hopf Algebra Categorization:
    1. To initiate the categorization of Hopf algebra in Lean, focusing on the defining categorical structures, objects, and morphisms, and their intrinsic properties.
    2. To extend this categorization, illustrating how Hopf Algebra Category evolves into a monoidal category.
  4. Exploration of Affine Group Schemes and Their Anti-Equivalence:
    1. To articulate the sophisticated representation of affine group schemes through corepresentable functors and the application of group axioms, setting the foundation for their algebraic and categorical analysis.
    2. To conclusively demonstrate the anti-equivalence between the category of affine group schemes and the category of commutative Hopf algebra, showcasing the culmination of this algebraic exploration and its implications for the broader mathematical landscape.

Protein folding by recursive backtracking

The hydrophobic-polar (HP) protein folding model was introduced by Ken A. Gill in 1985. It attracted a great deal of attention, at least until the advent of Google’s AlphaFold in 2018.

In this model, a binary string like 0110 is interpreted as a polymer, a sequence HPPH of amino acids of two types. The string is embedded in an ambient space, and this embedding is called a fold. Some folds are better than others and this is quantified by the score of the fold.

In this project I formalize basic definitions and facts for the HP model in such a way that Lean can automatically calculate optimal scores. To speed up the calculation I use recursive backtracking. For good measure, I prove in Lean that my implementation of recursive backtracking and its application are correct.

A critical issue when formalizing the HP model seems to be the choice of definition for the path induced by a sequence of folding moves (like up, down, left, right). I will present a couple of approaches used with varying success.

Stacks in Lean

In this talk, we plan to explain some of our work that has led to defining Stacks in Lean. We will introduce some of the basic mathematical theory around this topic (categories fibered in groupoids, etc) and explain the various challenges that arise when formalising this. Finally, we will discuss our more recent efforts to redefine these notions using structures and data types that are more adapted to Lean, and advertise our upcoming project to use this work as a basis to formalize some basic deformation theory (Schlessinger’s criterion, etc) for Kevin Buzzard’s FLT project.

Groups of order p * q

We formalise in Lean a proof that any finite group of order p q with p and q distinct prime numbers is isomorphic to the semidirect product of a cyclic group of order p and one of order q. We apply the result to classify groups of certain small orders in Lean. Joint work with Scott Harper.

Formalization of the Existence of Frobenius Elements

I will present a formalization in Lean 4 of exists_frobenius, a proof of the existence of the Frobenius element for finite Galois extensions L / K of number fields. This formalization constitutes some of the groundwork for Kevin Buzzard’s project to formalize the proof of Fermat’s Last Theorem. In terms of methodology, I will highlight the following components of exists_frobenius:

  1. firstly, application of the `A K L B` setup to:
    1. define a finite extension `L / K` of number fields, with `B`, `A` respective rings of integers;
    2. construct the transitive action of the Galois group `L ≃a[K] L` on the set of non-zero prime ideals which lie above a certain non-zero prime ideal `P ⊂ A`;
    3. define the decomposition subgroup of a nonzero prime ideal `Q` lying over `P`; and
    4. in combination with the orbit-stabilizer and Chinese remainder theorems, to characterize the orbit of `Q` under the action of `L ≃a[K] L`;
  2. secondly, synthesis of the characteristic, exponential characteristic, and Frobenius endomorphism of finite fields; the Galois correspondence; and integrality; to show that a polynomial `(F : B[X])` which is a product of linear factors `(X - C (galRestrict A K L B τ α))`, `(τ : L ≃a[K] L)`, `(α : B)` algebraic over K; has coefficients in A, the ring of integers of the base field of the extension.

© 2024. All rights reserved.