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, Brunerie's 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 $\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 $\beta$ 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}/2\mathbb{Z}$.

翻译：Brunerie 2016年的博士论文首次在同伦类型论（Homotopy Type Theory, HoTT）中给出了关于三维球面的第四同伦群为 $\mathbb{Z}/2\mathbb{Z}$ 这一经典结果的合成证明。该证明是迄今为止最令人瞩目的合成同伦理论成果之一，大量使用了以合成形式重述的经典代数拓扑高级内容。此外，Brunerie的证明是完全构造性的，其核心结论可归结为对某个特定的“Brunerie”数 $\beta$ 能否归一化为 $\pm 2$ 的判定。此后，Brunerie的证明能否在证明助手中实现形式化——无论是通过计算该数，还是形式化其手写证明——一直是个悬而未决的问题。本文中，我们遵循Brunerie的手写证明，在立方Agda系统中给出完整的、可直接运行的形式化版本。为此，我们修改了Brunerie的证明，从而避开了其论文中仅作略述的一项关键技术结果。同时，我们还给出了一种全新且更为简洁的证明的形式化，证明 $\beta$ 等于 $\pm 2$。这一形式化提供了一系列更简单的Brunerie数，其中某个数能在立方Agda中极快地归一化为 $-2$，从而为 $\pi_4(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$ 给出一个完全形式化的计算机辅助证明。