在 Cubical Agda 中形式化与计算三维球面的第四同伦群
Formalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical Agda
AI总结：
本文在 Cubical Agda 中完整形式化了三维球面第四同伦群为 $\mathbb{Z}/2\mathbb{Z}$ 的证明，通过修改Brunerie的证明避免关键技术难点，并提出新证明使特定数迅速归一化为 $-2$，实现了计算机辅助验证。
摘要：
Brunerie 2016年的博士论文包含了同伦类型论（HoTT）中关于三维球面第四同伦群为 $\mathbb{Z}/2\mathbb{Z}$ 这一经典结果的第一个综合证明。该证明是迄今为止最令人印象深刻的综合同伦论成果之一，使用了大量被综合重述的高级经典代数拓扑学。此外，该证明是完全构造性的，其主要结果可归约为特定“Brunerie数” $β$ 能否被归一化为 $\pm 2$ 的问题。Brunerie的证明能否在证明助手中形式化，无论是通过计算该数还是通过形式化纸笔证明，此后一直悬而未决。在本文中，我们提出了在 Cubical Agda 中的完整形式化。我们通过修改Brunerie的证明，使得Brunerie在论文中仅作概述的一个关键技术结果得以避免。我们还提出了 $β$ 为 $\pm 2$ 的全新且更简单证明的形式化。该形式化提供了一系列更简单的Brunerie数，其中一个在 Cubical Agda 中迅速归一化为 $-2$，从而产生了 $\pi_4(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$ 的完全形式化计算机辅助证明。
英文摘要：
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, the proof is fully constructive and the main result can be reduced to the question of whether a particular "Brunerie number" $β$ can be normalised to $\pm 2$. The question of whether Brunerie's proof could be formalised in a proof assistant, either by computing this number or by formalising the pen-and-paper proof, has since remained open. In this paper, we present a complete formalisation 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 formalisation of a new and much simpler proof that $β$ is $\pm 2$. This formalisation provides us with a sequence of simpler Brunerie numbers, one of which normalises very quickly to $-2$ in Cubical Agda, resulting in a fully formalised computer-assisted proof that $π_4(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
