[marta_morena_25]

Interesting. I hope what the author says isn't actually done. So the computers generated a proof nobody can understand, but fret not, a second computer program can assure us of its validity. Well that's heartwarming. I hope they are not building the foundations of future math on this house of cards.

[plafl]

I don't share your pessimism.

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.

[MaxBarraclough]

> fret not, a second computer program can assure us of its validity

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.

[throwaway_pdp09]

Perhaps you can offer something better?

[Joker_vD]

How about: a group of highly sophisticated and very skilled mathematicians generate a proof no mere mortals (and lesser mathematicians) can understand, but fret not: another genius mathematician can assure us of its validity.

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