[Math] Proof correctness problem

foundationssoft-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 ?

Best Answer

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

Related Question