Formalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical Agda
Axel Ljungström, Anders Mörtberg
TL;DR
This work provides the first computer-checked formalisation, in Cubical Agda, of Brunerie's synthetic proof that $\pi_4(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$, underscoring the constructive nature of Homotopy Type Theory (HoTT). It introduces a streamlined route that avoids a delicate Proposition 4.1.2 and yields a sequence of simpler Brunerie numbers $\beta_1,\beta_2,\beta_3$, with $\beta_3$ quickly normalising to $-2$, enabling a partially computer-assisted proof. The formalisation also offers a stand-alone, join-based approach to determine $\pi_4(§^3)$ and demonstrates a direct calculation of the Brunerie number via joins, the Hopf invariant, and the Gysin sequence. Overall, the work demonstrates the feasibility of machine-checked synthetic homotopy proofs and provides benchmarks and techniques for future formalisations in Cubical Agda and related systems.
Abstract
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 $\mathbb{Z}/2\mathbb{Z}$. 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 $\pm 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 $\pm 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(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$.