3 ms·

Wow, yet another result found by computer proof. Mathematics is getting weird. Maybe there is some metamathematical proof that the computer proof was produced i

by jordigh 10y ago

Wow, yet another result found by computer proof. Mathematics is getting weird. Maybe there is some metamathematical proof that the computer proof was produced in the correct fashion. My puny human brain wants reassurance that this proof is correct. It is not unheard of that widely accepted results turn out to be false. It's rare, but it has happened. Here are some examples: http://mathoverflow.net/questions/35468/widely-accepted-mathematical-results-that-were-later-shown-wrong/35558 http://mathoverflow.net/questions/35468/widely-accepted-math...

ibejoeb 10y ago
This is years old and I'm not familiar with it, but generally, the proof is among the simplest and most straightforward, right? If I read it right, it's proof by exhaustion. The trick is that it was previously impractical.
phamilton 10y ago
I think in this case, the lower bound was theoretically proven, and now exhaustively it has been determined that there are no positions which exceed the theoretical lower bound. I'm pretty comfortable with that conclusion. From what I understand, the 12 million positions that require 20 moves is not considered definitive not completely accurate. They stated that the searches weren't looking for the optimal solution, but rather any solution that took 20 or less moves. Without the theoretical lower bound, all the exhaustive proof would demonstrate is that the upper bound is 20. I feel like the exhaustive proof of establishing a given upper bound is much easier than finding the optimal solutions for every possible position.
- jordigh 10y ago
  And how do you know the exhaustion was done correctly? What was the process that lead to it? Is that process correct? Could they have forgot to check some cases? How do we know they didn't? There are still questions pending. If you and I write bugs into our programs, they may well have done the same thing for their program that supposedly checks all cases.
  - phamilton 10y ago
    Isn't that the same weak point of theoretical proof? Papers get accepted, peer reviewed, published without anyone detecting the flaw. A good example is Hyman's mutual exclusion algorithm, which passed all the usual review without issue but later discovered to be flawed. The source is available and can,should be, and has been peer reviewed.
    - jordigh 10y ago
      There are just many more points of failure in a computer proof than a human proof (I don't like calling it "theoretical", that doesn't seem like a useful distinction, and it has connotations of not being "real" when it's opposed to "practical"). Maybe they used numbers so big that there was an overflow. Maybe they relied on some library that itself had bugs that didn't express itself until they tried it on large numbers. Hell, even bits flipping due to cosmic rays is a legitimate concern and not as far-fetched as you might think. There are different kinds of pitfalls in computer proofs, and I wonder how can we account for them. The errors in a computer program are far less forgiving than the errors in a human proof. A typo in a human proof doesn't grind the whole proof to a halt and usually the human reader can quickly mentally correct the typo, but computer proofs are more brittle.
      - phamilton 10y ago
        Eh... A decent compiler will cause a proof to grind to a halt on a typo. I don't really see the difference honestly, besides quantitative complexity. A computer run exhaustive proof is less brittle than a manual exhaustive proof. I think complexity of the proof is just a function of the length. And for a computer proof, that length includes the toolchain.

by jordigh 10y ago

ibejoeb 10y ago

This is years old and I'm not familiar with it, but generally, the proof is among the simplest and most straightforward, right? If I read it right, it's proof by exhaustion. The trick is that it was previously impractical.

phamilton 10y ago

I think in this case, the lower bound was theoretically proven, and now exhaustively it has been determined that there are no positions which exceed the theoretical lower bound. I'm pretty comfortable with that conclusion. From what I understand, the 12 million positions that require 20 moves is not considered definitive not completely accurate. They stated that the searches weren't looking for the optimal solution, but rather any solution that took 20 or less moves. Without the theoretical lower bound, all the exhaustive proof would demonstrate is that the upper bound is 20. I feel like the exhaustive proof of establishing a given upper bound is much easier than finding the optimal solutions for every possible position.

jordigh 10y ago
And how do you know the exhaustion was done correctly? What was the process that lead to it? Is that process correct? Could they have forgot to check some cases? How do we know they didn't? There are still questions pending. If you and I write bugs into our programs, they may well have done the same thing for their program that supposedly checks all cases.
- phamilton 10y ago
  Isn't that the same weak point of theoretical proof? Papers get accepted, peer reviewed, published without anyone detecting the flaw. A good example is Hyman's mutual exclusion algorithm, which passed all the usual review without issue but later discovered to be flawed. The source is available and can,should be, and has been peer reviewed.
  - jordigh 10y ago
    There are just many more points of failure in a computer proof than a human proof (I don't like calling it "theoretical", that doesn't seem like a useful distinction, and it has connotations of not being "real" when it's opposed to "practical"). Maybe they used numbers so big that there was an overflow. Maybe they relied on some library that itself had bugs that didn't express itself until they tried it on large numbers. Hell, even bits flipping due to cosmic rays is a legitimate concern and not as far-fetched as you might think. There are different kinds of pitfalls in computer proofs, and I wonder how can we account for them. The errors in a computer program are far less forgiving than the errors in a human proof. A typo in a human proof doesn't grind the whole proof to a halt and usually the human reader can quickly mentally correct the typo, but computer proofs are more brittle.
    - phamilton 10y ago
      Eh... A decent compiler will cause a proof to grind to a halt on a typo. I don't really see the difference honestly, besides quantitative complexity. A computer run exhaustive proof is less brittle than a manual exhaustive proof. I think complexity of the proof is just a function of the length. And for a computer proof, that length includes the toolchain.