On the subject of formalization and the syllepsis, has it ever been formalized that Eckman-Hilton gives the generator of \pi_3(S^2)? That is, we can build a 3-loop for S^2 by refl_refl_base --> surf \circ surf^{-1} --EH--> surf^{-1} \circ surf --> refl_refl_base, and we want to show that under the equivalence \pi_3(S^2) --> Z constructed in the book that this 3-loop maps to \pm 1 (which sign you end up getting will depend on conventions).
There's another explicit way to construct a generating a 3-loop on S^2, namely refl_refl_base --> surf \circ surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl refl--> surf \circ surf \circ surf^-1 \circ surf^-1 --> refl_refl_base, where I've suppressed a lot of associators and other details. One could also ask whether this generator is the same as the one in my first paragraph. This should be of comparable difficulty to the syllepsis (perhaps easier), but is another good example of something that's "easy" with string diagrams but a lot of work to translate into formalized HoTT.
Best,
Noah