Comment by williamstein

I did a Ph.D. in number theory, published a few dozen research papers, and have programmed a lot and this post sounds about right to me. I did CS as an undergrad, before doing a math Ph.D., and remember being very surprised that math papers weren't a lot more wrong than they actually are (since computer software is so often full of bugs, and all it takes is one single bug to completely invalidate an entire paper). When I was a grad student at Berkeley, I once asked Serge Lang (who I think wrote the most advanced math textbooks of anybody who ever lived) why mathematics research papers don't have a lot more incorrect results in them. He responded that it was because people secretly "proved" everything to themselves in multiple ways, but only wrote up one proof, and it was unlikely that multiple very different reasons for something being true would all be wrong. Of course, there are serious mistakes and gaps in the literature, though what one person considers a gap, somebody else who knows more might not consider a gap. For example, I remember once that Ernst Kani was complaining to me about a big gap in a paper by Ribet; I didn't believe it, so I read the relevant section and was able to fill in the gap in a few hours sufficiently to satisfy him. In any case, I've spent decades both programming and doing number theory, and despite some similarities, they are very different things. Another related way these threads come together is with Kevin Buzzard's big project to formalize mathematics using LEAN; he's another number theorist, and he told me that a few years ago he started really worrying about the correctness of a lot of number theory papers, and that strongly motivated his interest in LEAN.