4 ms·
And even then, which do you find more convincing, the fact that there is an argument - which you have never read, and have no intention of reading - for which n
by merraksh 17y ago
And even then, which do you find more convincing, the fact that there is an argument - which you have never read, and have no intention of reading - for which none of the hundred or so errors found so far have proved to be fatal, or the fact that the hypothesis has been verified computationally (and, we shall assume, with total certainty) for 10 trillion cases?
What is more likely, a fatal error in the proof or a bug in the program? Proving (computationally or not) correctness of a program (or a proof) is not easy.
- Herring 17y agoProofs are hard. False positives in programs are very unlikely. It's usually a matter of verifying a few examples by hand because it's really hard to have isolated false positives.
- roundsquare 17y agoI don't really agree with that. Two examples come to mind: 1) Four color map theorem. I wouldn't have been horribly surprised if the code used to prove this made a mistake in 1,936 maps it had to check. Give that a second program verified it, I'd be more surprised now, but at the time, I would have been most worried about how to input the 1,936 maps. (I have no idea how this was done, if even generating them was programmatic, errors would have been less likely). 2) Automated symbolic logic programs are probably easy to make mistakes with. You need to have perfect parsing logic on the strings of each theorem and generate the new strings perfectly. I'm not saying its impossible, but mistakes are probably easy to make.
- Herring 17y agoIt occurs to me that the author & I are sort of making the same point: checking a bunch of points gives you a degree of confidence in the general case. I think the only way to settle it is to quantify it.