Published: January 1, 2025
27
188
1.3k

I've recently been talking a bit about how difficult it is to carefully check even well-written mathematics. I want to try to explain something about this by telling the story of some errors in the literature that (in part) led to the two papers below. 1/n

Image in tweet by Daniel Litt
Image in tweet by Daniel Litt

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.

(This thread meant in part as an explanation of my tweet here: https://x.com/littmath/status/... )

@littmath Time to start using Lean

@Autoparallel Much more practical in some fields than others, though hopefully this situation will improve soon.

@littmath How common is this in pure math? Anecdotally, it seems to happen relatively often. Isn’t a similar episode that spurred Voedodsky to start the univalent foundations program? What can the remedies be?

@__paleologo I think pretty common. Remedies unclear, maybe eventually everything will be formalized and checked by a computer.

@littmath I wonder if, before generating new math, this is where AI will be able to help first - looking for possible errors, and not just in the current paper but all the references too

@EdgarsNemse Hopefully AI will soon help us with formalization! But I also suspect it will help generate an unbelievable pile of nonsense to wade through…

@littmath May I export this and cross post to Mathstodon? I'll credit the original, of course.

@ColinTheMathmo Maybe I’ll do it, if you don’t mind?

@littmath this summarizes one of the principal reasons i am bewildered about mathematicians’ failure to take up ai research

@__alpoge__ IMO whether AI primarily contributes to or solves this problem depends a lot on how far capabilities progress. But my answer is that I like AG/NT, not AI; happy to mostly leave the latter to you for now.

Share this thread

Read on Twitter

View original thread

Navigate thread

1/26