Formalizing π₄(S³) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda

Proceedings of LICS 2023

Axel Ljungström, Anders Mörtberg https://arxiv.org/abs/2302.00151v2