Back

These papers began with an attempt to prove an open conjecture in surface topology—the Putman-Wieland conjecture. At some point in mid-2021 Aaron and I were pretty convinced we had a proof, and began writing up the details. 2/n

After writing 20 or so pages, I started to get worried. We were in fact proving something stronger than the Putman-Wieland conjecture—something to which there was a counterexample in the literature. There had to be an error somewhere. 3/n

After studying the counterexample for some time, I concluded that there was an error, in one of the last couple of paragraphs of the paper that claimed to produce it (error 1). The proof was back on! But something was still bothering me. 4/n

As I mentioned earlier, we actually seemed to be proving something much stronger than the conjecture we set out to prove. After optimizing the argument a bit further, it seemed to me that we were proving something (still!) that couldn’t be true. 5/n

We started carefully rechecking the papers we were using, and eventually found an error, in a reasonably well-cited paper published in 2016. 6/n

Incidentally, a similar erroneous lemma appeared in 4 different papers, with 3 distinct wrong proofs. (My favorite was of the form “the following (giant) diagram commutes.” Reader, it did not commute.) That’s errors 2-5. 7/n

We contacted the authors, who promised to get back to us; they were confident the issue could be repaired. But eventually we found a counterexample to the main theorem of the papers in question; the authors graciously agreed. 8/n

The ideas behind that counterexample led to the first of the two papers in the OP, which had nothing to do with the Putman-Wieland conjecture. Back to the grind. 9/n

In late 2021 I went to a workshop at the Mittag-Leffler institute in Sweden, where I spoke about our ongoing work. One of the other talks seemed to contain the key ingredient we were missing. 10/n

I printed out the relevant paper and read it on the flight home. Again, the paper was proving too much, and there was an error in a key lemma (error 6). 11/n

So, the Putman-Wieland conjecture is still open (and perhaps is cursed). That said, the ideas we were working on led to a proof of something I’d been thinking about on and off since ~2015 (the second paper above). 12/n

Ultimately this has a happy ending; a lot of errors in the literature were found and fixed, and in all cases the authors were very gracious about admitting the errors. All the wrong papers are either retracted or have the error explained in one of my papers. 13/n

That said, I think something about this story should worry you (and it worries me). Most of these errors were found because the theorem being proved was wrong. In all cases, the proofs as written were very plausible. 14/n

How many *true* theorems have plausibly written but erroneous proofs? These are much, much harder to catch. My guess is that it is a not insubstantial portion of the literature. 15/n, n=15.

@littmath I realise this is hopelessly naive, what with all the different branches of mathematics, different axiomatic bases, Godel etc, but has the idea of an "if this, then that" type database ever been tried, where you can flag up theorem X as being false and then see all of the resulting theorems that may be effected?

@_thegeoff seems very hard to implement! AFAIK no one has tried.

@littmath Maybe just a tree of citations in the literature to start with then ;)

@jannem I think formal verification is ultimately where we’re heading!

@littmath

your story reminds my of this lecture by Voedovsky where he explains his motivations for developing Univalent Foundations

Errors exist in accepted mathematics. Computer assisted proof could prevent this, but foundational maths didn't provide a formal way of expressing theorems that could be used in every day mathematics.

https://www.youtube.com/watch?v=E9RiR9AcXeE

@jannem

@littmath

screen shot of final slide in the lecture

@jannem

@henryseg More the latter but the theorem turns out to be true when the numbers involved are small, which is some sense in which there are "many confirming examples."

@henryseg (This is re: errors 2-5.)