[q-big]

> Doing actual rigorous proofs a computer can verify is enormously tedious and many Mathematicians dislike it for that reason, because the inherently subjective "elegance" and "beauty" gets lost in translation.

Couldn't we also interpret this fact that computerized proofs are currently often very unelegant as strong evidence that not a lot is understood about this topic and thus doing such "ugly" computerized proofs is the best we can (in most cases) currently do?

Science at the boundary of human knowledge is often quite ugly; as our understanding of it grows, it often becomes more beautiful and elegant.