Abstract

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