Science-advisor
REGISTER info/FAQ
Login
username
password
     
forgot password?
register here
 
Research articles
  search articles
  reviews guidelines
  reviews
  articles index
My Pages
my alerts
  my messages
  my reviews
  my favorites
 
 
Stat
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 ...
important:
of broad interest:
readable:
new:
correct:
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.






ScienXe.org
» my Online CV
» Free

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