Formalizing π_4(𝕊^3) ≅ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda
share
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, Brunerie's proof is fully constructive and the main result can be reduced to the question of whether a particular “Brunerie” number β can be normalized to ± 2. The question of whether Brunerie's proof could be formalized in a proof assistant, either by computing this number or by formalizing the pen-and-paper proof, has since remained open. In this paper, we present a complete formalization in the Cubical Agda system, following Brunerie's pen-and-paper proof. 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 formalization of a new and much simpler proof that β is ± 2. This formalization provides us with a sequence of simpler Brunerie numbers, one of which normalizes very quickly to -2 in Cubical Agda, resulting in a fully formalized computer assisted proof that π_4(𝕊^3) ≅ℤ/2ℤ.
READ FULL TEXT