Proof correctness problem

Question

I was watching this talk by Vladimir Voevodsky which was given at the Institute of Advanced Study in 2006.

In his talk the first slide he shows has the following written on it:

             We need to look at the foundations again because of the 
                         Proof correctness problem

Two components:

$1.$ There is an accumulation of results whose proofs the math community cannot fully verify

$2.$ There are more and more examples of proofs which have been accepted and later found to be incorrect

This is a much more serious problem for math than it would be for any science because the main strength of mathematics is in its ability to build on multiple layers of previous constructions.

Here is what he says while presenting the slide:

"......As mathematics gets more and more complex, there is an accumulation of results whose correctness becomes more and more uncertain. We don't know about certain things, whether they have been proved or not. ..... every Mathematician has experienced on both sides how terrible it is nowadays to be a referee. I have a paper which is about 10 pages long and it has been lying in a journal for about 10 years now because the referee can't get through ( ? Not sure about if I understood him correctly there). I have not been much better as a referee myself. The problem is mathematics is very complex and if one wants to be responsible for a paper one referees, it takes an enormous amount of effort. It really slows things down. We do have to do something about it. From my point of view there is only one solution.... "

He then goes on to talk about foundations of mathematics, automated proof verification, and so on. My question is only about the statements $1.$ and $2.$ made in the slide.

Q1. I am looking for examples of such results and proofs. What evidence (if any) is there that shows the problem is on the rise?

Q2. Is there a blog, article, essay, etc., which goes through or lists such results and proofs, where there is a discussion about these things ?

Answer 1

If we interpret Voevodsky's first claim broadly, there have been several high-profile results that the mathematical community has had great difficulty verifying, e.g., Perelman's proof of the geometrization conjecture, the classification of finite simple groups, Hales and Ferguson's proof of the Kepler conjecture, and Mochizuki's proof of the abc conjecture.

Perelman's proof is now accepted but it took years for the community to validate it.

The classification of finite simple groups is now regarded as not having been completely proved until Aschbacher and Smith's work in 2004, but for many years the generally accepted date for the completion of the proof was 1983 and it took a while for the quasithin case to be generally acknowledged as a serious gap.

Hales is working on the Flyspeck project, which is a tacit acknowledgment that the original proof was too hard for the community to independently verify and that formal mechanized proofs are the way to go.

Mochizuki's proof is still in the process of being verified almost two years after he made the proof public, with no closure yet on the horizon.

This is already an impressive list in my opinion and does not even touch on less famous results, or results that generated controversy such as Hsiang's proof of the Kepler conjecture or the original proof of the four-color theorem. (Ironically, of course, many people initially were uncomfortable with the proof of the four-color theorem because computers were involved, whereas today Voevodsky is uncomfortable unless computers are involved—albeit in a different way.)

Answer 2

The Finnish mathematician Pertti Lounesto produced, with computer aid, a series of counterexamples to published and accepted theorems on Clifford algebras. He recorded his findings in the following two articles:

P. Lounesto: Counterexamples in Clifford algebras with CLICAL, pp. 3-30 in R. Ablamowicz et al. (eds.): Clifford Algebras with Numeric and Symbolic Computations. Birkh\"auser, Boston, 1996.

P. Lounesto: Counterexamples in Clifford algebras. Advances in Applied Clifford Algebras 6 (1996), 69-104.

He set up a webpage where he exhibits a few of these counterexamples and offers some explanations of how these errors could arise and how he went about to find the counterexamples. After Lounesto's death the webpage was mirrored here.

Answer 3

First comment: see https://en.wikipedia.org/wiki/List_of_incomplete_proofs

Second comment: That page is probably enough to convince anyone that the problem as posed is not a new one. Assertion of a trend is a statement about history. Surely the publication of false proofs (of the different kinds the Wikipedia article deals with) is nothing new.

Third comment: So what is the history?

(A) There was Euclid, which contains a fair amount of fairly rigorous mathematics, some of which stood up to scrutiny to the 1890s, though the status of the axioms had shifted a couple of generations before that. Anyway, after Euclid and before say Weierstrass there was a good deal of less rigorous mathematics published, including therefore much of the mathematics used for applications.

(B) Axiomatic mathematics was refounded in the decades on either side of 1900, leading to a famous definition in terms of predicate calculus of (pure) mathematics, by Bertrand Russell. Logic, as part of this development, became absorbed into mathematics, except for the part that wasn't (this statement does have some actual content), which was then called philosophy.

(C) As part of axiomatisation, by around 1950 almost all of mathematics had become absorbed into the kind of mathematics you could call axiomatic proved professional mathematics. Except for the part that wasn't, which was mostly then called physics.

(D) In this post-1950 context, a purported proof that was a non-proof became a "scandal". It has been noted that this was to do with the standards from analytic number theory becoming universal. About the only thing that Nicolas Bourbaki would have as a topic of conversation with, say, Harold Davenport, would be that non-proofs should die.

(E) It was assumed (i) that journals would apply those standards in peer review, which was pretty much true, and (ii) that only publication in journals counted, which rather quickly turned out not to be true.

(F) Quite a lot of pushback against the "unholy alliance" represented by Bourbaki+Davenport occurred, for the sake of geometry, being able to talk to physicists, use of computers and some other factors, I think. The "Italian geometers" were a scandal in spades, but the content of their work was a good quarry. Grothendieck's bypassing of the journal system was accepted by most (probably too easily). In other words mathematics grew out a Procrustean bed again.

Sort of summation

(G) One assertion seems to be that a morass such as "Italian geometry" could be quite possible under current conditions. It is hard to know how one could be in a position to contradict that.

(H) Another is that peer review is harder than it used to be. I can't comment there. If though the basic expository effort has not been made to get older results out of journal papers and into textbook form, that is another kind of "crisis". I think it started around 1960, and is reinforced in mathematics by the paucity of survey articles.