Pseudo-isotopies of 4-manifolds

One of the landmark results about the topology of 4-manifolds is Freedman’s proof of the 4-dimensional Poincaré conjecture. The problem with this result was that after some time people claiming to understand its proof disappeared, so that in the last decade the validity of this result was openly questioned (e.g., link). In the end, a new book was written on this topic and things seem to be fine now (link to an earlier post of mine about this).

Today I came across the following arXiv-preprint which gave this post its title: arXiv:2311.11196. The main goal of this paper is to correct the proof of another important result from the 80s about the differential topology of 4-manifolds. The error was unnoticed for almost four decades.

I do not want to discredit the 4-manifolds community here. There are plenty of similar examples in all other areas of mathematics (I am sure about this, though of course I can’t prove it). As time goes on, this bothers me more and more; each year a gazillion of mathematical papers is written and a non-negligible amount of them is wrong. Even important results sometimes, after several decades, turn out to be wrong (at least, turn out to have an erroneous proof).

So let me propose something here towards a solution of this problem: We should focus more on formal verification of the mathematical literature! (Say, in LEAN; link.) This is the only way that I see to end the uncertainty of contemporary mathematical results.