一句话：在 Cubical Agda 中完全形式化 π₄(S³)≅Z/2Z，并通过计算简化后的 Brunerie 数完成计算机辅助证明。
Brunerie 2016 年的博士论文给出了同伦类型论中 3 球第四同伦群为 Z/2Z 的首个合成证明，该证明完全构造性，可归约为判断特定 Brunerie 数 β 是否能归一化为 ±2；但其能否在证明助手中形式化一直未决。本文在 Cubical Agda 中给出完整形式化：通过修改 Brunerie 的证明，避开其论文中仅草稿说明的关键技术结果；并形式化一个新的、更简单的 β=±2 证明。该形式化产生一系列更简单的 Brunerie 数，其中一个在 Cubical Agda 中快速归一化为 −2，从而得到 π₄(S³)≅Z/2Z 的完全形式化计算机辅助证明。
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 ℤ/2ℤ. 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 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 β is ±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}$.