This. Mathematics is not really the study of what is the case, it’s the study of why. Even if this was accompanied by a full Coq proof it would be unsatisfactory because absolutely no insight is being provided.
https://mathoverflow.net/questions/116627/useless-math-that-...
I'm not saying that this is the same of Mochizuki's work, but I would not dismiss it solely on the basis that it's "useles".
Anyway, I'm basically repeating what people have already said. So I'll stop.
However generating a proof like that in the first place is a really tough task involving searches and codification of advanced known mathematics in Coq proof way.
In this way, semi auto prover like Isabelke are nicer fort mathematicians as they will ask about holes...