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 MCS3070 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 | Introduction to Lean | Jujian Zhang |
| 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 | Towards a formal proof of the Freyd-Mitchell embedding theorem | Markus Himmel |
| 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 |
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.
l-adic Galois Representations in Lean 4Families 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.
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.
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.
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.
p * qWe 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.
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:
© 2024. All rights reserved.