If you think a shorter elegant proof is more desirable, well, I totally agree with you. I think math is more about the proofs than the results. On the other hand I have zero problems trusting a proof checked by a computer. I don't know you but I usually trust much more computers with tedious computations than myself.

Formal methods are rigorous enough and mature enough to be helpful in avionics software development, why not in research mathematics?

> I hope they are not building the foundations of future math on this house of cards.

Mathematics is always a house of cards, and human mathematicians will always be fallible. It's already possible for a published result to later turn out to be invalid, in turn invalidating papers that relied on it.

Hmmmmmmm. Yeah, that sounds much better. What do you think?