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.

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.

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.

> 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-o...

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.