在立方 Agda 中形式化并计算 3-球面的第四同伦群

Brunerie 2016 年的博士论文包含了同伦类型论（HoTT）中首个关于经典结果“3-球面的第四同伦群为 $\mathbb{Z}/2\mathbb{Z}$”的综合证明。该证明是迄今最令人瞩目的综合同伦理论成果之一，并使用了大量被综合重述的进阶经典代数拓扑。此外，该证明完全构造性，且主要结果可归约为一个特定的“Brunerie 数” $\beta$ 能否规范化为 $\pm 2$ 的问题。自那时起，Brunerie 的证明能否在证明助手中形式化（或通过计算该数，或通过形式化笔纸证明）一直悬而未决。本文中，我们给出在 Cubical Agda 中的完整形式化。为此我们修改了 Brunerie 的证明，从而避开一项关键技术结果——Brunerie 仅在其论文中勾勒了该项结果的证明。我们还形式化了一个全新且简单得多的证明，表明 $\beta$ 为 $\pm 2$。该形式化提供了一列更简单的 Brunerie 数，其中之一在 Cubical Agda 中极快地规范化为 $-2$，从而得到完全形式化的计算机辅助证明 $\pi_4(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$。