forgot password?
register here
Research articles
  search articles
  reviews guidelines
  articles index
My Pages
my alerts
  my messages
  my reviews
  my favorites
Members: 3652
Articles: 2'545'386
Articles rated: 2609

24 June 2024
  » arxiv » 2302.00151

 Article overview

Formalizing $π_4(mathbb{S}^3) cong mathbb{Z}/2mathbb{Z}$ and Computing a Brunerie Number in Cubical Agda
Axel Ljungström ; Anders Mörtberg ;
Date 1 Feb 2023
AbstractBrunerie’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}/2mathbb{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 $eta$ 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 $eta$ 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}/2mathbb{Z}$.
Source arXiv, 2302.00151
Services Forum | Review | PDF | Favorites   
Visitor rating: did you like this article? no 1   2   3   4   5   yes

No review found.
 Did you like this article?

This article or document is ...
of broad interest:
Global appreciation:

  Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
» my Online CV
» Free

home  |  contact  |  terms of use  |  sitemap
Copyright © 2005-2024 - Scimetrica