Skip to main content
To KTH's start page To KTH's start page

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

Time: Wed 2022-03-02 10.00 - 12.00

Location: Kräftriket, House 5, Room 31

Participating: Axel Ljungström (Stockholm University)

Export to calendar


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).