My problem with these massive / exhaustive proofs is they provide no insight. Sure, you can use them as a building block to prove something else, but they don’t uncover new tools and approaches to solve other problems.

Compare it to, say, Wiles’s proof of Fermat’s last theorem: I can’t understand that proof either, but there are many who can, and for them it teaches a bunch of things.