3 ms·

Empirically, proofs with bugs get ironed out into proofs with less bugs, and the results almost always end up standing. Why mathematical proof seems to be as go

Empirically, proofs with bugs get ironed out into proofs with less bugs, and the results almost always end up standing. Why mathematical proof seems to be as good as it is at avoiding proving false statements is a matter of contention, but practically speaking it works. There's very little incentive to computer check proofs because, as a practical matter, mathematics is not plagued with false "theorems." Computing, on the other hand, is plagued with broken programs, and formal methods are still a very specialized area, even though the potential benefits are much greater in computing than mathematics.

lostmsu 5y ago
> mathematics is not plagued with false "theorems." But you don't know that. There certainly were precedents: https://mathoverflow.net/questions/291158/proofs-shown-to-be-wrong-after-formalization-with-proof-assistant https://mathoverflow.net/questions/291158/proofs-shown-to-be...
- roywiggins 5y ago
  The answer given there by Manuel Eberl is more or less what I was trying to get at (and he is far more knowledgeable about it than I am). Lots of mathematicians find that the existing level of rigor in the field is enough. Obviously the people who like proof assistants disagree, and they may be right. It could be that modern theorems are just too complicated to be adequately evaluated by unassisted humans. But mathematicians have been getting along just fine without them for a long time, so "why aren't we requiring computer-checked proofs of everything" has a very straightforward answer: mathematicians writ large aren't convinced of the benefit yet.
  - Jweb_Guru 5y ago
    This is largely because in modern mathematics, people ignore or won't build on proofs that are too complicated for them to follow, and rely heavily on trust and networking effects for the remaining proofs that are too useful to ignore. Plenty of results (including big results) are published in mathematical journals each year, which are "known" to be flawed or sketchy, but never have a formal rebuttal, and if you want to build on a proof that doesn't have much followup work, and are having trouble understanding its argument, you're expected to ask around and find out whether the proof is worth pursuing or not. Proof assistants would enable people to trust much more complex proofs from much more junior mathematicians, rather than essentially requiring the community to reprove the same results over and over until they're satisfied, and IMO this is holding back mathematics more than many mathematicians realize.
deleted 5y ago
[deleted]

lostmsu 5y ago

> mathematics is not plagued with false "theorems." But you don't know that. There certainly were precedents: https://mathoverflow.net/questions/291158/proofs-shown-to-be-wrong-after-formalization-with-proof-assistant https://mathoverflow.net/questions/291158/proofs-shown-to-be...

roywiggins 5y ago
The answer given there by Manuel Eberl is more or less what I was trying to get at (and he is far more knowledgeable about it than I am). Lots of mathematicians find that the existing level of rigor in the field is enough. Obviously the people who like proof assistants disagree, and they may be right. It could be that modern theorems are just too complicated to be adequately evaluated by unassisted humans. But mathematicians have been getting along just fine without them for a long time, so "why aren't we requiring computer-checked proofs of everything" has a very straightforward answer: mathematicians writ large aren't convinced of the benefit yet.
- Jweb_Guru 5y ago
  This is largely because in modern mathematics, people ignore or won't build on proofs that are too complicated for them to follow, and rely heavily on trust and networking effects for the remaining proofs that are too useful to ignore. Plenty of results (including big results) are published in mathematical journals each year, which are "known" to be flawed or sketchy, but never have a formal rebuttal, and if you want to build on a proof that doesn't have much followup work, and are having trouble understanding its argument, you're expected to ask around and find out whether the proof is worth pursuing or not. Proof assistants would enable people to trust much more complex proofs from much more junior mathematicians, rather than essentially requiring the community to reprove the same results over and over until they're satisfied, and IMO this is holding back mathematics more than many mathematicians realize.

deleted 5y ago

[deleted]