We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Mathematics > Algebraic Topology

Title: Formalizing $π_4(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$ and Computing a Brunerie Number in Cubical Agda

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, Brunerie's proof is fully constructive and the main result can be reduced to the question of whether a particular ``Brunerie'' number $\beta$ can be normalized to $\pm 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 $\beta$ is $\pm 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 $\pi_4(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$.
Subjects: Algebraic Topology (math.AT); Logic in Computer Science (cs.LO)
Cite as: arXiv:2302.00151 [math.AT]
  (or arXiv:2302.00151v1 [math.AT] for this version)

Submission history

From: Axel Ljungström [view email]
[v1] Wed, 1 Feb 2023 00:11:00 GMT (877kb)

Link back to: arXiv, form interface, contact.