3 ms·
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
by marta_morena_25 6y ago
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 6y agoI 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 6y ago> 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 6y agoPerhaps you can offer something better?
- Joker_vD 6y agoHow 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?