> It would be good to have a formalised proof of the o(n log n) result, for example in Lean. As far as I can tell, one does not yet exist.

The result is fully formalized in Lean by @platypii and myself (on Mathlib's TM2 machine), with ongoing improvements to the exponent (currently at 1-2^-14.38): https://github.com/platypii/integer-mult-bounds-lean

Contributions are welcome!