16

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 ?

Todd Trimble
  • 52,336
The very fluffy Panda
  • 111
  • 1
    I have also posted this question on http://math.stackexchange.com/questions/869493/proof-correctness-problem Is the question more appropriate here ? Should I delete one of the two posts ? – The very fluffy Panda Jul 17 '14 at 10:54
  • 2
    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
  • Re Q1: I don't think there is a "community" sense on the whole. There are some who feel quite strongly (eg Hales), and others who do not. Serre for a long time was pestering about ClassifyFiniteSimpleGroups, and whether every iota had been dotted. Another anecdote: with Perelman, various topologists talked about the years delay in checking the details, saying that for anything other than Poincare, it would have been accepted a lot time before. That is typical in many math areas, only the really significant results are combed over. Whether it is a problem is a diff matter, as TT says, opinion. – NAME_IN_CAPS Jul 17 '14 at 12:28
  • 1
    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
  • Coming back to the second (interrogative) sentence of Question 1: would it distort the meaning or intent if it were replaced by "What evidence (if any) is there that shows the problem is on the rise?", or something similar? I'm thinking this reformulation would encourage a more fact-based approach. Regarding Panda Bear's question in the first comment: I think it's okay for MO, provided we can ameliorate the potential of this being too subjective. – Todd Trimble Jul 17 '14 at 12:58
  • No, that won't distort its meaning. This question is not intended to ask for opinion. I don't know why I phrased it like that. Something along the lines of what @NAME_IN_CAPS posted (A family of Calabi-Yau varieties and potential automorphy II.) is what I am looking for. I don't understand the paper at all, but I think that was a minor error, I maybe wrong. Also, please don't water it down for me ( I am not saying anybody has done that). I may understand it in a few years time. – The very fluffy Panda Jul 17 '14 at 13:07
  • 11
    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
  • @ZhenLin brilliant, that what's I am looking for. Such Examples. – The very fluffy Panda Jul 17 '14 at 13:19
  • The CY varieties context: this Taylor "school" has produced many long papers at the very forefront of their subject, the biggest recent result (2005-present) is Sato-Tate in various cases. They typically use technical work of others (eg Arthur trace formula), and are quite clear about this. Furthermore, these papers mention (to some degree) errors noted from their previous work. Fortunately they are technically competent enough to get around any flaws, some of which are not always minor. To me, this is "best case", others would not be so meticulous. (And as I say, they are very prominent.) – NAME_IN_CAPS Jul 17 '14 at 14:18
  • I think you should distinguish between the following. First proofs that are flawed but reasonably fixable, then proofs that are incorrect and there's no light in the tunnel, and finally theorems that are themselves actually incorrect. The latter two cases do occur, but the common case is by far the first, and the author usually decides whether the "reasonably fixability" merits writing an erratum, or mentioning the problem in a future work, etc. PS. There are two maths papers with "Zaphod Beeblebrox" in the title, one the paper, and the second the correction to the paper. – NAME_IN_CAPS Jul 17 '14 at 14:22
  • 1
    @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
  • I am not sure I understand the new paradigm being suggested. Are proofs no longer to be learnt studied and simplified, but rather just computer checked and we will just take the results as given. – Rene Schipperus Jul 17 '14 at 22:38
  • @ReneSchipperus I think you misunderstood him, he is not suggesting that proofs should no longer be studied and simplified rather making sure that one is not hitting his head against the wall. Whether automated proof verification will lead to what you are suggesting(as I understood your comment) is I think open for discussion. – The very fluffy Panda Jul 17 '14 at 23:15
  • I think he is right that math has become complicated, but I feel that exposition and simplification of existing results should be more highly valued , and will lead to some ameleoration of the problem. – Rene Schipperus Jul 17 '14 at 23:37
  • There was a fairly recent example of someone randomly generating a math paper which was accepted for publication. The stunt was to show that pay-to-publish journals were terrible and incentivized to get anything published, rather than good things. But I think it fits into the wider spectrum of the growing inadequacies and flaws with the current journal system. In my own research I have gotten papers published before a paper it references has even gotten a response from a referee. And my field can take a long time to get things published. They're overwhelmed on all counts. – zibadawa timmy Jul 18 '14 at 01:19
  • The author's second item is of course trivial. For any type of event, the accumulat6ed number of such events is nondecreasing over time. – Hagen von Eitzen Jul 18 '14 at 10:15
  • 1
    In mathematics, do we have something like post publication-peer review. Do we have a PubPeer 'equivalent' ? I know among colleagues, there is always a discussion about a paper when it's published, but that's internal. I am looking for where such discussions are done in public. Maybe there is an online commenting system. I do worry that may lead to spam comments or would be a distraction. – The very fluffy Panda Jul 18 '14 at 10:35
  • @Hagen, that was my suggested edit. Let's try to be more generous in interpretation. Instead of "on the rise", you could substitute "accelerating" perhaps. – Todd Trimble Jul 18 '14 at 10:59
  • There is a big list for question 2: http://mathoverflow.net/questions/35468/widely-accepted-mathematical-results-that-were-later-shown-wrong – Peter Arndt Jul 22 '14 at 00:09

3 Answers3

16

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

Dirk
  • 12,325
Timothy Chow
  • 78,129
  • 5
    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
  • This was quite interesting, but as Asaf points out, this does not really surprise me. I think it is very normal. Mathematics is a very difficult subject. Should it surprise me though ? How about adding some less high profile subtle results ? I hope I am not asking too much. I am also not sure exactly what I am expecting, because I have very little knowledge. – The very fluffy Panda Jul 17 '14 at 23:09
  • 1
    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 04:00
  • 2
    @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
  • Timothy, I apologize for starting this off-topic chain of comments. Perhaps Perelman was an exception because he posted the proof and pretty much vanished back into himself. But I still hear these apologetic tones often, e.g. about Wiles "But it took him seven years", but it took 300 years of mathematical progress, what's seven years for writing a proof, and what's four years for checking it? Yes. Mathematics is difficult. Everyone knows that. We need to stop feeling bad for that. – Asaf Karagila Jul 18 '14 at 19:08
  • 2
    @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
  • What? No, I didn't talk about Voevodsky's point. I was talking about your phrasing (which is not uncommon) regarding proofs that it take years to review and verify. In particular the usual phrasing of "This and that proof ... but it took many years to ...", which has an apologetic undertones, at least to my ears. – Asaf Karagila Jul 18 '14 at 20:17
  • @AsafKaragila: I know that you did not talk about Voevodsky's point, and that is my point. I did not make my remark out of the blue. It was in the context of Voevodsky's claim that "There is an accumulation of results whose proofs the math community cannot fully verify." In that context, I believe my phrasing is natural. Do you think that Voevodsky's remark is apologetic? Would you retort to Voevodsky that "Math is difficult"? If not, what is it about my phrasing that causes you to react differently? – Timothy Chow Jul 20 '14 at 20:34
  • @Asaf: coming up with proofs is hard, yes. Verifying proofs can and should be trivial. Formal proof systems demonstrate that this is the case. The only reason why verification might not be trivial is because standard proofs are vague informal sentences and indeed, sometimes it is found the claimed proofs (and even propositions) are wrong! So you're right, it's not surprising that verifying such claims takes years in the current practice, but there's no a priori reason why that should be so. And let's hope it won't be so in the years to come. – Marek Jan 21 '15 at 20:49
  • @Marek: I don't want to get into a discussion which is over six months old. But let me say that expecting that seems to me equivalent to expecting miracle drugs that cure your sickness in minutes. Things just don't work that way. – Asaf Karagila Jan 21 '15 at 21:05
  • @AsafKaragila Fair enough, I didn't notice the discussion was old, although I think it's no less relevant today. Anyway, nobody is expecting miracles, writing formal proofs is hard. Point is, it's the only way forward, given the ever-growing body of vaguely-stated & vaguely-checked knowledge. – Marek Jan 21 '15 at 21:24
  • 1
    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
12

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.

Peter Arndt
  • 12,033
  • 3
    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 01: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
8

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.

Charles Matthews
  • 12,415
  • 34
  • 63