4 ms·

> As this incident demonstrates, errors can easily creep into mathematical proofs, even those written by experts. The only way to mitigate this is to use comput

> As this incident demonstrates, errors can easily creep into mathematical proofs, even those written by experts. The only way to mitigate this is to use computer-readable proofs, (...) Ironically, computer programs seem to be a lot more error prone than mathematical proofs. Yes, errors in mathematical proofs happen, but they're rare enough that the they're widely reported in the (mathematical) community. Errors in computer programs on the other hand are a virtual guarantee.

hgsgm 4y ago
Ironically, emails and essays seem to be out more error prone than mathematical proofs... 1. Proofs are intended to be correct. The vast majority of computer programs are intended to be practical, and are far far larger than the largest math proofs. Where correctness matters, computer programs have fewer bugs. 2. Nearly every non-computerized mathematical proof is not even a proof, it is a sketch that requires a lot of hand waving and logical jumps to be interpreted. Likewise, specs have fewer bugs than concrete program, because they aren't complete.
Jeff_Brown 4y ago
A math professors blew my mind once by telling me that a paper full of errors was still good work and could be salvaged. He went on to say that most good work was like that. In the worst case you end up proving something else, but typically you can prove what you initially set out for. I found that so strange I had to confirm it with another, who concurred.
- dzdt 4y ago
  The reason for this is that mathematical papers are fundamentally about an insight about mathematical objects. The insight typically comes from the mathematician having a deep understanding of the mathematical objects. The theorems are some formalised statement that should be true based on the deep understanding. The proofs are something else entirely, a sequence of steps which combine to verify the theorem but where many steps may result from trial-and-error searching for a path forward. Coming from a good mathemematician, the original insights are much more likely to be correct than the details of the proof steps.
BeetleB 4y ago
> but they're rare enough that the they're widely reported in the (mathematical) community. You should ask math professors how often there are errors in papers. Every one has their own ratio, but I've heard numbers as high as 30%. However, the general belief is the results are still correct, so few are worried about building with a pile of cards. See https://academia.stackexchange.com/questions/143374/extent-of-unscientific-or-wrong-papers-in-research-mathematics https://academia.stackexchange.com/questions/143374/extent-o...
ogogmad 4y ago
A computerised proof checker is much less likely to have a mistake than a typical computer program - or a mathematical proof - because it's extremely simple.

hgsgm 4y ago

Ironically, emails and essays seem to be out more error prone than mathematical proofs... 1. Proofs are intended to be correct. The vast majority of computer programs are intended to be practical, and are far far larger than the largest math proofs. Where correctness matters, computer programs have fewer bugs. 2. Nearly every non-computerized mathematical proof is not even a proof, it is a sketch that requires a lot of hand waving and logical jumps to be interpreted. Likewise, specs have fewer bugs than concrete program, because they aren't complete.

Jeff_Brown 4y ago

A math professors blew my mind once by telling me that a paper full of errors was still good work and could be salvaged. He went on to say that most good work was like that. In the worst case you end up proving something else, but typically you can prove what you initially set out for. I found that so strange I had to confirm it with another, who concurred.

dzdt 4y ago
The reason for this is that mathematical papers are fundamentally about an insight about mathematical objects. The insight typically comes from the mathematician having a deep understanding of the mathematical objects. The theorems are some formalised statement that should be true based on the deep understanding. The proofs are something else entirely, a sequence of steps which combine to verify the theorem but where many steps may result from trial-and-error searching for a path forward. Coming from a good mathemematician, the original insights are much more likely to be correct than the details of the proof steps.

BeetleB 4y ago

> but they're rare enough that the they're widely reported in the (mathematical) community. You should ask math professors how often there are errors in papers. Every one has their own ratio, but I've heard numbers as high as 30%. However, the general belief is the results are still correct, so few are worried about building with a pile of cards. See https://academia.stackexchange.com/questions/143374/extent-of-unscientific-or-wrong-papers-in-research-mathematics https://academia.stackexchange.com/questions/143374/extent-o...

ogogmad 4y ago

A computerised proof checker is much less likely to have a mistake than a typical computer program - or a mathematical proof - because it's extremely simple.