| > In contrast mathematical proofs tend to be absolutely bullet proof. They really, really do not. It's why an initial proof of the four coloring theorem was believed for a decade before a flaw was discovered. History has quite a few examples of proofs believed to be correct for years that turned out to be flawed. Read the quotes from William Thurston's essay in the comment I linked to. I've spent time with professional mathematicians, and they say that finding errors in papers is not at all unusual - I've seen estimates as high as a third of papers have an error.[1] This doesn't concern them as even though there are errors, they have good reasons to believe the correctness of the theorems and freely will use them as references to their own work. Thurston's essay goes into detail as to why that is. > I can only assume that the mathematician who wrote the quote in your footnote was talking about maths notation vs computer language syntax. While the quote I supplied was in the context of notation, the essay addresses the wider issue. > But software doesn't need to be anywhere near logically correct to run Indeed, and his analogous statement is that proofs don't need to be completely correct to believed :-) I believe he cites Wile's proof of Fermat's theorem. At the time of writing, he had presented his proof and a flaw had been found - the fixes came after his essay. So at that time, he knew the proof had problems. Yet he points out most people believed that Wile's approach was correct, and resolving the problems in his proof were a matter of detail.
This wasn't a matter of faith. Those mathematicians understood the theory Wiles used well enough to have a good intuition that the reasoning was sound. It was certainly challenging to resolve the bug(s) in his proof - the Wikipedia page indicates he almost gave up. But I suspect that had this been a less dramatic theorem, the pressure to fix the flaws would not really be there. Of course, at times that intuition turns out to be surprisingly wrong. But those tend to be the exceptions. [1] This link points out that about 1.4% of published papers have corrections: https://mathoverflow.net/questions/291890/what-percentage-of... However, I believe that most flaws that are found are not corrected (i.e. the author doesn't bother sending in a correction). Here is an anecdote from Kevin Buzzard, who is a proponent of formalizing proofs using computers: > It is true that there are holes in some proofs. There are plenty of false lemmas in papers. But mathematics is robust in this extraordinary way. More than once in my life I have said to the author of a paper "this proof doesn't work" and their response is "oh I have 3 other proofs, one is bound to work" -- and they're right. ... > But until then I think we should remember that there's a distinction between "results for which humanity hasn't written down the proof very well, but the experts know how to fill in all of the holes" and "important results which humanity believes and are not actually proved". Taken from https://mathoverflow.net/questions/351640/extent-of-unscient... |
>>> I've seen estimates as high as a third of papers have an error.
That is pretty much what I meant by "tend" to be right. If only a third of all the software out there had "an error" that would be a dramatic improvement.