# Proof correctness problem

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 ?

-
I have also posted this question on math.stackexchange.com/questions/869493/… Is the question more appropriate here ? Should I delete one of the two posts ? – The very fluffy Panda Jul 17 '14 at 10:54
Question 1 is tricky from a meta perspective because there is danger of it being mostly opinion-based, or subjective (at least regarding the second half of the question). Proceeding with fingers crossed... – Todd Trimble Jul 17 '14 at 11:56
There is also the meta-question about the true function of the "referee". For some, this exists to ensure at a broad level that maths is done not gibberish, with the ultimate onus of correctness on the author. For others, this referee is a inquisitor of highest rank, viewing the author as a mortal enemy in the combat of proof (OK, maybe I exaggerate). Again it will vary a lot among mathematicians and specialty areas. (And again on the interest level of the result, and inevitably the author.) – NAME_IN_CAPS Jul 17 '14 at 12:31
It might be amusing to look at these slides from a more recent talk of Voevodsky's – he gives some examples. – Zhen Lin Jul 17 '14 at 13:07
@NAME_IN_CAPS Regarding first proofs that are flawed but reasonably fixable, I think that is inevitable. I am more concerned about the latter two. Though interested in all three. – The very fluffy Panda Jul 17 '14 at 15:22

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.)

-
I always feel strange when people say things like "Perelman's proof is now accepted but it took years for the community to validate it." It took nearly 100 years to solve this problem. Why do people expect that the proof will be so immediate that everyone reading it couple of times will find it clear enough to judge its content? Difficult proofs take time to analyze. There's nothing wrong with that, and we need to stop qualifying these sentences with "but" which make it seem apologetic. – Asaf Karagila Jul 17 '14 at 22:24
The classification of finite simple groups is very interesting for a couple of reasons at least. The formulation required the list of sporadic groups to be complete; and the empirical approach of the discoverers of sporadic groups was important to the acceptance that the list was right. I remember the champagne for J4 ... – Charles Matthews Jul 18 '14 at 4:00
@AsafKaragila: This is getting off-topic, but Perelman's was a special case in many ways. The preprints were extremely terse, and did contain non-trivial (though fixable) errors. Mathematicians typically make themselves highly available for clarifications, but Perelman limited his access. In Jan 2005 I had an email exchange with an expert, and at that time he went as far as to say, "It is unclear if anyone will ever publicly announce that the proof is correct.' A more likely scenario is that various readers will make nuanced statements describing the status of the verification process." – Timothy Chow Jul 18 '14 at 19:04
@AsafKaragila: I don't understand why you sense an undertone of apology or bad feeling. A neutral reading of Voevodsky's point is that mathematical proofs are generally increasing in complexity, to the point where it is advisable to consider seriously integrating proof assistants into mathematical practice. The purpose of listing some examples is to give some anecdotal evidence for this claim. I don't see the purpose of attacking the example on the grounds of some perceived slight. – Timothy Chow Jul 18 '14 at 20:09
I think that the situation regarding quasithin groups is a little more complex than briefly indicated here. There are people more expert than I on the precise history, but as I understand it, there was a very long unpublished manuscript about quasithin groups written by G. Mason. Apart from its unpublished status, one important issue was that the people who were (in the early 80s) wrapping up the last stages of the classification had assumed a starting point which was apparently different from that which Mason's manuscript had actually reached. – Geoff Robinson Jan 21 '15 at 22:48

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.

-
Holy cow, that is amazing. "Such groups of mathematicians had a collective cognitive illusion about the mathematical reality' ... Sometimes such groups defended their cognitive bugs vigorously." – Nik Weaver Jul 18 '14 at 1:52
This was a really interesting read. Such an example is what I am looking for. – The very fluffy Panda Jul 18 '14 at 10:26

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.

-
That certainly lends some perspective ! Now more than ever the work of expositors is important. – The very fluffy Panda Jul 17 '14 at 15:57
– jeq Jul 17 '14 at 19:42
"It has been noted that this was to do with the standards from analytic number theory becoming universal." Citation? – Gerry Myerson Jul 17 '14 at 23:57
@jeq books.google.co.uk/… explains something about a famous example, and Severi's general shamelessness. – Charles Matthews Jul 18 '14 at 3:45
@Gerry Myerson An early example is Jacobi saying that Dirichlet is the only really rigorous mathematician around; and juxtaposing that with his use of Fourier series in prime number theory (books.google.co.uk/books?id=tqaWlHIsZXAC&pg=PA29). By the time you have G. H. Hardy commenting on Ramanujan and the complex zeroes of the Riemann zeta function, I believe the thought had become a commonplace. – Charles Matthews Jul 18 '14 at 3:52