4 ms·

Many mathematicians seem to have an attitude that a well peer-reviewed proof is simply correct and etched in stone for good. This seems to me like publishing pr

Many mathematicians seem to have an attitude that a well peer-reviewed proof is simply correct and etched in stone for good. This seems to me like publishing programs - some of them thousands of lines long - and expecting them to be essentially bug-free without ever running them. Von Neumann is not exactly making the same point, but he is arguing against the sense that math is a kind of purely abstract discovery that has escaped from the messiness of day-to-day reality. One could ask: will we ever get to a point when all mathematical proofs are rigorously checked, so that we know they're correct? I hope we do get to a point when program-checked proofs are standard, but even then there's the possibility that a proof-checker itself is buggy. So, philosophically, it seems we may never justifiably feel certain beyond all doubt that any given proof is correct. But we can have greater confidence in a proof verified by both expert humans and by a trusted program than in a proof simply reviewed by humans. So the effort is meaningful and worthwhile - all in the context of seeing math as a field as fallible as any other.

tribe 11y ago
You might be interested in this article [1]. Basically, even if many proofs are incorrect, their results are almost always still true. Also, there have been many large changes in what counts as 'rigorous' over time. I agree with you that computer-checked proofs seem like a logical next step in the rigor of mathematics. [1] http://www.gwern.net/The%20Existential%20Risk%20of%20Mathematical%20Error http://www.gwern.net/The%20Existential%20Risk%20of%20Mathema...
JadeNB 11y ago
> Many mathematicians seem to have an attitude that a well peer-reviewed proof is simply correct and etched in stone for good. This seems to me like publishing programs - some of them thousands of lines long - and expecting them to be essentially bug-free without ever running them. I think that the important distinction is 'peer-reviewed'. A random programme published, even by a very good programmer, is indeed likely to have errors; but I think that one can have more confidence in a peer-reviewed programme (which is essentially why we trust open source over closed source, after all). Of course there are distinctions: software is automatically tested when used, whereas mathematics is not automatically tested when read, so that one might reasonably have more confidence in software purely on the basis of its longevity than one does in mathematics; but, on the other hand, although individual pieces of reasoning can be extremely arcane, 'flow control' in mathematical reasoning tends to be much more elementary than in software, so that one is unlikely to uncover the mathematical analogue of an infrequently visited branch in a code path going untested despite heavy use of the software.

tribe 11y ago

You might be interested in this article [1]. Basically, even if many proofs are incorrect, their results are almost always still true. Also, there have been many large changes in what counts as 'rigorous' over time. I agree with you that computer-checked proofs seem like a logical next step in the rigor of mathematics. [1] http://www.gwern.net/The%20Existential%20Risk%20of%20Mathematical%20Error http://www.gwern.net/The%20Existential%20Risk%20of%20Mathema...

JadeNB 11y ago

> Many mathematicians seem to have an attitude that a well peer-reviewed proof is simply correct and etched in stone for good. This seems to me like publishing programs - some of them thousands of lines long - and expecting them to be essentially bug-free without ever running them. I think that the important distinction is 'peer-reviewed'. A random programme published, even by a very good programmer, is indeed likely to have errors; but I think that one can have more confidence in a peer-reviewed programme (which is essentially why we trust open source over closed source, after all). Of course there are distinctions: software is automatically tested when used, whereas mathematics is not automatically tested when read, so that one might reasonably have more confidence in software purely on the basis of its longevity than one does in mathematics; but, on the other hand, although individual pieces of reasoning can be extremely arcane, 'flow control' in mathematical reasoning tends to be much more elementary than in software, so that one is unlikely to uncover the mathematical analogue of an infrequently visited branch in a code path going untested despite heavy use of the software.