  
  
Stat 
Members: 3652 Articles: 2'545'386 Articles rated: 2609
24 June 2024 

   

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  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 3sphere 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 penandpaper proof, has since remained open. In this paper, we
present a complete formalization in the Cubical Agda system, following
Brunerie’s penandpaper 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 


No review found.
Did you like this article?
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.

 


