2023/02/01 by Axel Ljungström, Ljungström, Axel, Anders Mörtberg +1
Computer Science · Mathematics · #Algebraic Topology (math.AT) #FOS: Computer and information sciences #FOS: Mathematics #History and Theory of Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic in Computer Science (cs.LO) #Topological and Geometric Data Analysis
paper · pdf · doi:10.48550/arxiv.2302.00151
openalex publication_date 2023/02/01 · openalex created_date 2023/02/14 · openalex updated_date 2026/07/28
Brunerie's 2016 PhD thesis contains the first synthetic proof in Homotopy Type Theory (HoTT) of the classical result that the fourth homotopy group of the 3-sphere is ℤ/2ℤ. The proof is one of the most impressive pieces of synthetic homotopy theory to date and uses a lot of advanced classical algebraic topology rephrased synthetically. Furthermore, the proof is fully constructive and the main result can be reduced to the question of whether a particular "Brunerie number" β can be normalised to ± 2. The question of whether Brunerie's proof could be formalised in a proof assistant, either by computing this number or by formalising the pen-and-paper proof, has since remained open. In this paper, we present a complete formalisation in Cubical Agda. We do this by modifying Brunerie's proof so that a key technical result, whose proof Brunerie only sketched in his thesis, can be avoided. We also present a formalisation of a new and much simpler proof that β is ± 2. This formalisation provides us with a sequence of simpler Brunerie numbers, one of which normalises very quickly to -2 in Cubical Agda, resulting in a fully formalised computer-assisted proof that π4(\mathbbS3) ≅ ℤ/2ℤ.