Axel Ljungström: The Serre finiteness theorem in homotopy type theory

Abstract: In its most concise form, the Serre finiteness theorem states that homotopy groups of spheres are finitely presentable. Although the original proof of this theorem appears to make crucial use of classical methods, it turns out that it actually holds constructively. Working in the setting of homotopy type theory, Barton and Campion recently devised a remarkably simple and inherently `homotopy-theoretic' proof of the theorem, which was recently formalised by Barton, Milner, Mörtberg, and myself. The plan for this talk is simply to provide an overview of Barton and Campion's proof. If time permits, I might also say a few words about the formalisation and how it led to further simplifications of Barton and Campion's proof.