The Serre finiteness theorem in Cubical Agda

Add to your list(s) Download to your calendar using vCal

• Axel Ljungström (University of Nottingham)
• Thursday 26 February 2026, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

In this talk, I will present a recently finished computer 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 homotopy type theory (HoTT) by Barton and Campion. We have formalised this proof 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.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• Martin's interesting talks
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk449

Note that ex-directory lists are not shown.