  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" $\beta$ 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 $\beta$ 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
$\pi_4(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$.
