Guillaume proved that there is some $n$ such that $\pi_4(S^3)$ is $\mathbb{Z}/n\mathbb{Z}$. With a computational interpretation, we could run this proof and check that $n=2$.
On 14 February 2016 Guillaume announced a proof that $n=2$, via a proof involving the Thom construction and Gysin sequences.
$\pi_3(S^2)$
Peter’s construction of the Hopf fibration as a dependent type. Lots of people around know the construction, but I don’t know anywhere it’s written up. Here’s some Agda code with it in it.
Guillaume’s proof that the total space of the Hopf fibration is $S^3$, together with $\pi_n(S^n)$, imply this by a long-exact-sequence argument, but this hasn’t been formalized.
Cohomology
To do cohomology with finite coefficients, all we need is the boring work of defining $\mathbb{Z}/p\mathbb{Z}$ as an explicit group.
Calculate some more cohomology groups.
Compute the loop space of this construction and use it to define spectra.
Peter’s encode/decode-style proof, formalized by Dan, using a clever lemma about maps out of 2 n-connected types. This is the “95%” version, which shows that the relevant map is an equivalence on truncations.
The full “100%” version, formalized by Dan, which shows that the relevant map is $2n$-connected.