"In Mathematics, Mistakes Aren’t What They Used To Be"

[Arsenic&Lace]

http://nautil.us/issue/24/error/in-mathematics-mistakes-arent-what-they-used-to-be

A very interesting article which I think furnishes a point I've been making for a while about mathematics: proofs are as eternal and infallible as the creatures which create them.

EDIT: But with a bit of optimism regarding computer assisted proofs.

 

[jedishrfu]

Interesting paper. It reminds me of the battle between John Henry and the steam drill:

http://americanfolklore.net/folklore/2010/07/john_henry.html

The real question is do we use our brains alone or our computers alone or do we use our computers to extend our brain's reach like we use a telescope or other scientific equipment? There's room for all of these views kind of like the back to nature vs modern technology debate.

Sometimes using a computer eliminates the search for a more creative way of solving the problem. In the end when the computer takes too long then we search for a faster way such as a faster computer or a faster algorithm whichever is more economically viable.

 

[gleem]

It is said that all computer programs have at least one bug. When the bug emerges how bad the bite will be is anybody's guess. Who will check the computer? Or will we just accept anything that it tells us?

 

[Arsenic&Lace]

^^Very good point. So mathematical proofs can never truly be infallible and eternal; just more infallible and eternal than they were before you fed them to your computer proof assistant.

 

[jedishrfu]

You can think of it like virus protection. There's always a new computer virus that will defeat the best virus scanner. The scanners can't scan everything that comes by. They look for signatures so new viruses are adapted to not be detected.

The same could be said of proofs. As we gain new insight, we may see a weakness in the proof's argument. The computer can only be as good as our understanding of a problem.

 

[gleem]

Do we believe that nothing can create something better than itself? After all we are human.

 

[SteamKing]

I think this episode illustrates why science and the scientific method are such handy tools.

A theory and a proof were published, and to most people, that would be the end of it. However, one intrepid soul, Carlos Simpson, did a little checking and found a mistake.
When Voevodsky heard about the mistake, he did the responsible thing and re-checked his work until he confirmed he was indeed in error.

Now, a less gracious man might have gotten defensive about having the veracity of his work doubted, but he did a classy thing and acknowledged that his colleague had indeed found an error in his work.

I think this is why science by consensus is to be avoided at all costs. Scientific theories and experimental results must constantly be checked against one another, especially when the theory may not be as fully developed as some would have us believe.

 

[micromass]

A very interesting article which I think furnishes a point I've been making for a while about mathematics: proofs are as eternal and infallible as the creatures which create them.

So your point is that humans make mistakes? You're obviously right.

 

[jedishrfu]

So your point is that humans make mistakes? You're obviously right.

I think Arsenic adjusted his view somewhat when he learned that programs are not infallible in post #4.

I like the quote that we all make mistakes but to really screw things up you need a computer which being a programmer is more true than you can imagine.

Always remember on a clear disk you can seek forever...

 

[gleem]

With regards to the statement that " to really screw things up you need a computer" reminds me of the Disney film " The Sorcerers Apprentice" in the hands of the wrong persons a wonderful power can cause unimaginable chaos.

 

[Arsenic&Lace]

So your point is that humans make mistakes? You're obviously right.

My point is clearly more than this, but to spell it out for you, I'm inferring from the fact that humans are infallible that one of the major selling points of pure theory in mathematics, that a proof is eternal, is rubbish, both due to the increasing probability of false results and the evolving standards of rigor which render previously satisfactory proofs false.

Now bad results can propagate in science as well, but one of the ways to get a sense of how bad things are is whether or not the results are connecting with results elsewhere in the field or in other fields entirely, so I would argue that once a mathematical result becomes sufficiently complex, its basic validity is suspect until it connects at least with other mathematics and preferably with applications.

 

[micromass]

one of the major selling points of pure theory in mathematics, that a proof is eternal

I'm sure some people say this, but I have never seen this claimed. Then again, this is philosophy which is hardly my strong point. But I would be really surprised if you could find many mathematicians who don't know by experience that proofs can be fallible since humans are fallible.

Now bad results can propagate in science as well, but one of the ways to get a sense of how bad things are is whether or not the results are connecting with results elsewhere in the field or in other fields entirely, so I would argue that once a mathematical result becomes sufficiently complex, its basic validity is suspect until it connects at least with other mathematics and preferably with applications.

There aren't many mathematical results that are not connected with other mathematics or (even very vaguely) to applications.

In my opinion, the validity of a result in science (such as an experiment) increases when it is checked by many people. If a lot of people repeat an experiment a lot of times with (roughly) the same outcome, then we trust the outcome of the experiment more. The same is true with mathematics. If a proof is checked by many people and they all see no flaw, then the probability of the correctness of the proof increases. For example, I don't think there should be any doubt that the Hahn-Banach theorem is true.

 

[micromass]

See also this interesting discussion: http://mathoverflow.net/questions/3...hematical-results-that-were-later-shown-wrong

 

[jedishrfu]

Have any of these wrong proofs been used to test the proof proving algorithm mentioned earlier?

 

[zoobyshoe]

My point is clearly more than this, but to spell it out for you, I'm inferring from the fact that humans are infallible...

Did you mean to use the word "infallible" here?

 

[jedishrfu]

Did you mean to use the word "infallible" here?

I always like how we tend to say "not infallible" over "fallible".

 

[micromass]

Have any of these wrong proofs been used to test the proof proving algorithm mentioned earlier?

There are issue with computarized proof checking. The most obvious issue is that translating a proof into something that a machine can check is difficult. Very difficult. It takes a lot of time and effort. I don't really see proofs like the Poincare conjecture being checked soon.
Furthermore, the reason that proofs are being accepted as right while they are wrong, has mostly to do that the way we write proofs is very informal and intuitive. Many math papers will take big leaps in their arguments, leaps which they find obvious since they work in the field. Sometimes, these leaps are wrong. The research mathematicians do not have the time nor patience to make a proof completely formal. That would completely halt mathematics. Instead, we rely on the power of numbers: many people checking the same proof. It is not infallible, but I don't think there is a better option.

See also: https://www.sciencenews.org/article/how-really-trust-mathematical-proof

 

[micromass]

In my opinion, one of the bigger issues concerning the validity of mathematics are the sometimes shaky foundations used in mathematics. Of course, simple things like finite group theory are not an issue. Even if ZFC were to be proved inconsistent, finite group theory would still be true and we would just search for other axioms.

But nowadays, we have seen the rise of category theory. And associated with it are many powerful assumptions on set theoretical level. Many of which could be inconsistent. I have little fear that ZFC is inconsistent. But the power of the assumptions nowadays can be very great. Inaccessible cardinals, measurable cardinals, etc. All of these are things I find a bit suspect.

A more thought-out point of view can be see in the works of Penelope Maddy. For example: http://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf

 

[jedishrfu]

There are issue with computarized proof checking. The most obvious issue is that translating a proof into something that a machine can check is difficult. Very difficult. It takes a lot of time and effort. I don't really see proofs like the Poincare conjecture being checked soon.
Furthermore, the reason that proofs are being accepted as right while they are wrong, has mostly to do that the way we write proofs is very informal and intuitive. Many math papers will take big leaps in their arguments, leaps which they find obvious since they work in the field. Sometimes, these leaps are wrong. The research mathematicians do not have the time nor patience to make a proof completely formal. That would completely halt mathematics. Instead, we rely on the power of numbers: many people checking the same proof. It is not infallible, but I don't think there is a better option.

See also: https://www.sciencenews.org/article/how-really-trust-mathematical-proof

Thanks Micro, its as I thought the proof checkers themselves are custom built for the proof and that means human error can be introduced as well. Originally, I thought that perhaps some new standardized technique like encoding a proof using prolog as used to test its validity.

Prolog has some limitations in the kinds of problems it can solve/prove:

http://www.cs.rochester.edu/~scott/173/notes/09_pred_logic

 

[micromass]

In my opinion, one of the bigger issues concerning the validity of mathematics are the sometimes shaky foundations used in mathematics. Of course, simple things like finite group theory are not an issue. Even if ZFC were to be proved inconsistent, finite group theory would still be true and we would just search for other axioms.

But nowadays, we have seen the rise of category theory. And associated with it are many powerful assumptions on set theoretical level. Many of which could be inconsistent. I have little fear that ZFC is inconsistent. But the power of the assumptions nowadays can be very great. Inaccessible cardinals, measurable cardinals, etc. All of these are things I find a bit suspect.

A more thought-out point of view can be see in the works of Penelope Maddy. For example: http://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf

In this case, the only way of judging consistency of an axiom system would be to look at the applications of mathematics. The physical universe is obviously consistent. So results proven in pure mathematics can be checked by checking some physical property that they imply. This is not a proof, but merely an experiment. And thus even pure mathematics has been reduced to experimentation. This is not a new point-of-view: many mathematicians such as Gauss held this view. Arnold is a more extreme version of this. More information on this can be found in Kline's http://en.wikipedia.org/wiki/Mathematics:_The_Loss_of_Certainty
See also Arnold's point of view with a very controversial (but in my opinion correct) first sentence: http://pauli.uni-muenster.de/~munsteg/arnold.html

 

[micromass]

Thanks Micro, its as I thought the proof checkers themselves are custom built for the proof and that means human error can be introduced as well. Originally, I thought that perhaps some new standardized technique like encoding a proof using prolog as used to test its validity.

Prolog has some limitations in the kinds of problems it can solve/prove:

http://www.cs.rochester.edu/~scott/173/notes/09_pred_logic

I guess there are two kinds of proof checkers really. For example, the original proof of the four colour theorem involved computers which check multiple cases. These kind of "proof checkers" were indeed built specifically for this theorem. It is indeed plausible that bugs could enter the program.
But there are also other proof checkers which can (in principle) check almost all of mathematics in existence. These universal proof checkers give a very big guarantee of the correctness of a result, because their code can be checked manually. Nevertheless, some things can still go wrong:

1) The axioms used in the proof checkers may be inconsistent.
2) The computer program might have a bug which everybody fails to see
3) Due to cosmic radiation, the computer program might malfunction and see a proof as correct while it is wrong. One of my favorite statements regarding this can be found in "Structure and Interpretation of computer programs" by Abelson and Sussman:

Numbers that fool the Fermat test are called Carmichael numbers, and little is known about them other than that they are extremely rare. There are 255 Carmichael numbers below 100,000,000. The smallest few are 561, 1105, 1729, 2465, 2821, and 6601. In testing primality of very large numbers chosen at random, the chance of stumbling upon a value that fools the Fermat test is less than the chance that cosmic radiation will cause the computer to make an error in carrying out a ``correct'' algorithm. Considering an algorithm to be inadequate for the first reason but not for the second illustrates the difference between mathematics and engineering.

 

[micromass]

Thanks Micro, its as I thought the proof checkers themselves are custom built for the proof and that means human error can be introduced as well. Originally, I thought that perhaps some new standardized technique like encoding a proof using prolog as used to test its validity.

Prolog has some limitations in the kinds of problems it can solve/prove:

http://www.cs.rochester.edu/~scott/173/notes/09_pred_logic

I guess there are two kinds of proof checkers really. For example, the original proof of the four colour theorem involved computers which check multiple cases. These kind of "proof checkers" were indeed built specifically for this theorem. It is indeed plausible that bugs could enter the program.
But there are also other proof checkers which can (in principle) check almost all of mathematics in existence. These universal proof checkers give a very big guarantee of the correctness of a result, because their code can be checked manually. Nevertheless, some things can still go wrong:

1) The axioms used in the proof checkers may be inconsistent.
2) The computer program might have a bug which everybody fails to see
3) Due to cosmic radiation, the computer program might malfunction and see a proof as correct while it is wrong. One of my favorite statements regarding this can be found in "Structure and Interpretation of computer programs" by Abelson and Sussman:

Numbers that fool the Fermat test are called Carmichael numbers, and little is known about them other than that they are extremely rare. There are 255 Carmichael numbers below 100,000,000. The smallest few are 561, 1105, 1729, 2465, 2821, and 6601. In testing primality of very large numbers chosen at random, the chance of stumbling upon a value that fools the Fermat test is less than the chance that cosmic radiation will cause the computer to make an error in carrying out a ``correct'' algorithm. Considering an algorithm to be inadequate for the first reason but not for the second illustrates the difference between mathematics and engineering.

 

[jedishrfu]

Don't forget the famous Intel floating pt FPU error:

http://en.wikipedia.org/wiki/Pentium_FDIV_bug

We will never know if the current crop of devices has some sort of similar type of error.

 

[zoobyshoe]

See also Arnold's point of view with a very controversial (but in my opinion correct) first sentence: http://pauli.uni-muenster.de/~munsteg/arnold.html

That is a lively, blunt article, which I found very entertaining. Here's a quote relevant to this thread:

At this point a special technique has been developed in mathematics. This technique, when applied to the real world, is sometimes useful, but can sometimes also lead to self-deception. This technique is called modelling. When constructing a model, the following idealisation is made: certain facts which are only known with a certain degree of probability or with a certain degree of accuracy, are considered to be "absolutely" correct and are accepted as "axioms". The sense of this "absoluteness" lies precisely in the fact that we allow ourselves to use these "facts" according to the rules of formal logic, in the process declaring as "theorems" all that we can derive from them.

It is obvious that in any real-life activity it is impossible to wholly rely on such deductions. The reason is at least that the parameters of the studied phenomena are never known absolutely exactly and a small change in parameters (for example, the initial conditions of a process) can totally change the result. Say, for this reason a reliable long-term weather forecast is impossible and will remain impossible, no matter how much we develop computers and devices which record initial conditions.

In exactly the same way a small change in axioms (of which we cannot be completely sure) is capable, generally speaking, of leading to completely different conclusions than those that are obtained from theorems which have been deduced from the accepted axioms. The longer and fancier is the chain of deductions ("proofs"), the less reliable is the final result.

Complex models are rarely useful (unless for those writing their dissertations).

 

[jedishrfu]

This is also related to the issue of using simulations in court cases where because it looks plausible the it must be so which means jurors can draw the wrong conclusions.

 

[phion]

Cool read.

 

[Jeff Rosenbury]

micromass said "The physical universe is obviously consistent. "

This is not obvious to me.

Stories we humans tell seem much more consistent than the universe. The universe is wrong more often than not. (Well from our infallible human point of view anyway).