Axel Ljungström: The Fourth Homotopy Group of the 3-Sphere is Z/2Z: A Complete(ly Formalised) Proof

Abstract

In his PhD thesis, Guillaume Brunerie proved, in Homotopy Type Theory, that the fourth homotopy group of the 3-sphere is isomorphic to \(\mathbb{Z}/2\mathbb{Z}\). Despite being one of the most ambitious pieces of work in our field so far, Brunerie's proof has some relatively serious gaps. These gaps have, until recently, stood in the way of a fully formalised proof of the theorem in question. In this talk, I will give an overview of Brunerie's proof, tell you where the gaps are and, most importantly, tell you how to work around them (jww Anders Mörtberg).