# 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. Is this really a problem faced by the mathematical community ?

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 ?

1) This refers to the issue that math proofs are becoming very long (some hundreds of pages, and even so there are many steps that are skipped because the author assumes them as trivial or as easily reproduced. That in practice not always happen. For instance, it took years to confirm Fermat's last theorem proof. There are only very few experts that can follow the demonstration in all detail and their available time is limited. 2) For the same reason, many of these proofs are checked and approved by such a small number of people that finding mistakes or oversights in their checks is not uncommon.

The short hanging fruit, that is, the short and easy theorems seem to have been already demonstrated, so most of the ones that remain are long and painful. As a physicist, I could say that the formal (and sometimes outrageous by their informality) theories of physics didn't reach yet this level of complexity. Much less the other sciences.

But I think the problem will be fixed not too long in the future. Once we can build trustable proof systems on fast enough computers, the correctness of most proof will not be decided by humans, but by very advanced AI math poof software.

Sorry about the fact that I didn't include specific examples because I am not a mathematician, but for what I have read recently, it is an important issue in current math.

• Thanks for elaborating on $1$ and $2$, good addition to the question. – The very fluffy Panda Jul 17 '14 at 10:44
• Go to math overflow – The very fluffy Panda Jul 17 '14 at 13:27