Formalizing pi(4)(S-3) congruent to Z/2Z and Computing a Brunerie Number in Cubical Agda
2023 38TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, LICS(2023)
摘要
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 Z/2Z. 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" beta can be normalized to +/- 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 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 formalization of a new and much simpler proof that beta is +/- 2. This formalization provides us with a sequence of simpler Brunerie numbers, one of which normalizes very quickly to in Cubical Agda, resulting in a fully formalized computer-assisted proof that pi(4)(S-3) congruent to Z/2Z
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要