-
Axel Ljungström
A formalisation of the Serre finiteness theorem
20 novembre 2025 - 09:00Salle de séminaires IRMA
Martin-Löf's intensional type theory is a logical system which can function both as a foundation of mathematics and as a programming language. While the original motivations behind this system were arguably rooted in a desire to give constructive mathematics a more computational interpretation, it turns out that it also has deep links with a seemingly unrelated branch of mathematics: homotopy theory. By adding two features to (intensional) type theory – higher inductive types (roughly: cell complexes) and Voevodsky's univalence axiom (roughly: equality = isomorphism) – we obtain homotopy type theory (HoTT). This language allows us to use type theory to talk about concepts from homotopy theory/algebraic topology such as spaces, paths, homotopies, and so on. Because type theory also functions as a programming language, HoTT is ideal for translating (formalising) proofs from homotopy theory into code which can be formally verified using so-called proof assistants.
In this talk, I will present a recently finished formalisation project of a cornerstone result from homotopy theory: the Serre finiteness theorem. This theorem, which in its simplest form states that homotopy groups of spheres are finitely presented, was recently given a proof entirely in the language of HoTT by Barton and Campion. It is this proof that we have formalised in the HoTT-based proof assistant Cubical Agda. Because HoTT is a constructive language and Cubical Agda is fully computational, our formalised proof of the Serre finiteness theorem can be viewed as an (executable) algorithm which takes as input any homotopy group of any sphere and returns a finite presentation of it. I plan on giving a rough outline of the proof and its formalisation. I will also discuss what problems we run into when actually trying to run our proof/algorithm on a computer. Before doing any of this, however, I will give a quick recap of the very basics of (homotopy) type theory and (Cubical) Agda.
This talk is based on joint work with Reid Barton, Owen Milner, Anders Mörtberg, and Loïc Pujet.
About the speaker : Axel Ljungström is a postdoc at the School of Computer Science at the University of Nottingham working with Ulrik Buchholtz. The position is funded by a scholarship he was awarded from the Knut and Alice Wallenberg foundation. Recently, he was a Ph.D. student in the computational mathematics division of the department of mathematics at Stockholm University. There, he was working on a project on homotopy type theory under the supervision of Anders Mörtberg.
His primary research interests are synthetic homotopy theory and computer formalisation, primarily in (Cubical) Agda. His thesis was mainly concerned the formalisation of cohomology theories and Guillaume Brunerie’s Ph.D. thesis.