> An obvious question when formalising a maths paper is how much the proof needed to change to be formalised: in other words whether there were any flaws in the paper. This question is surprisingly subtle, but a simple summary is that most of the mistakes I identified were easily fixable. Importantly all mistakes were fixable in a way that preserved the spirit of the argument, so the Lean version of the proof can reasonably be said to be a translation of the informal proof.<p>> I like to consider certain such small mistakes “mathematical typos”. It’s fair to call them errors, and just like typos in English prose can confuse a non-native speaker, mathematical typos can impede meaning for a reader who isn’t familiar with mathematics. However, with a little experience, it’s not hard to see what the intended meaning was, and fixing it isn’t too bad. A mathematical typo certainly doesn’t constitute a flaw in the proof, and almost all the problems I found fall in this category.<p>If only we had better ways to distribute fixes to papers. These kind of issues happen all the time and unlike in code where someone can just come in and provide a fix, these usually remain forever in papers. Yes, some publish errata or upload a new version to the arxiv, but the majority remain as a form of horrendous "exercise for the reader".
If I'm an expert in a field I may quickly notice such issues, but more often than not I won't spend the time required to do so. And hence I probably propagate wrong information myself / wonder why my numerical calculations don't produce the correct result etc.<p>It is especially bad when branching out into areas somewhat out of your area. The amount of mistakes and utterly wrong information I had to deal with just in the last few months thanks to papers being sloppy is just sad. So much time wasted. :( (I'm a physicist)