6 ms·

My memory is that the Four Colour Theorem was one of the first computer search-assisted proofs which caused all sorts of epistemological questions. Specifically

My memory is that the Four Colour Theorem was one of the first computer search-assisted proofs which caused all sorts of epistemological questions. Specifically how to know whether the software had no bugs and ran correctly, and how re-running to get the same result only lowered the probability and did not yield absolute certainty. Seems sort of a quaint concern now. (Apologies for no reference. I hope I'm not misremembering.)

Dove 4y ago
You're remembering entirely correctly! I gave a talk on the Four Color Theorem as part of my master's degree in 2001, and it was a somewhat active epistemic debate among mathematicians at the time. I took the position that examining code was no different than examining a proof, that running it through a computer was no different than running it through your brain, and that mathematicians are not shy at all about "automating" processes over uncountable infinities in proofs, so why should we be shy about automating them over thousands mechanically? There is a fun faith-shaking element to the story, though. The Four Color Theorem, as a proof, actually contains a couple thousand smaller proofs. These were generated and checked by a computer, but it is humanly possible to check them with a great deal of effort. There was a guy -- I forget his name, and Google isn't helping me! -- who, as his Ph. D. thesis, actually went through them and checked them. And IIRC, he found about a dozen errors! They weren't fatal -- he was able to repair them -- but that whole process didn't really reassure people. ;)
- Dove 4y ago
  AMS has a good summary: https://blogs.ams.org/mathgradblog/2014/06/29/color-theorem https://blogs.ams.org/mathgradblog/2014/06/29/color-theorem
  - ghusbands 4y ago
    To save others the effort of reading - this only discusses the proof and not the by-hand check or "about a dozen errors" mentioned in the parent post.
- anonymousDan 4y ago
  How did the errors arise, some bug in the theorem prover?
  - Dove 4y ago
    That's a really good question. I may have known the answer to it twenty years ago, but I don't now. XD What I can tell you is that it wouldn't have been so straightforward as that. We're not talking about an axiom-to-result symbolic proof piece of software like you might attempt to write now. It wasn't a computer proof so much as a computer-assisted proof. Lots of human analysis to describe specific properties, and then a computer program to check that a long list of geometric configurations had those properties. I don't know exactly what the program output as its proof, but I can only imagine the problems would have been small assumptions built into its design failing in corner cases. The theorem is notoriously difficult to reason about rigorously, and there have been a number of accepted proofs over the years that turned out to be false. It really doesn't help the whole situation that not only is it the first major computer-assisted theorem, it just happens to deal with a result that people are already wary of.
  - puzzledobserver 4y ago
    The original computer assisted proof of the four colour theorem was written in IBM 370 assembler [0]. This was naturally susceptible to programming errors such as those discussed above. Gonthier's subsequent certified proof requires trust in a much smaller body of code and hardware [1]. [0] https://projecteuclid.org/journals/illinois-journal-of-mathematics/volume-21/issue-3/Every-planar-map-is-four-colorable-Part-II-Reducibility/10.1215/ijm/1256049012.full https://projecteuclid.org/journals/illinois-journal-of-mathe... [1] https://www.ams.org/notices/200811/tx081101382p.pdf https://www.ams.org/notices/200811/tx081101382p.pdf
- dchftcs 4y ago
  >The Four Color Theorem, as a proof, actually contains a couple thousand smaller proofs. These were generated and checked by a computer, but it is humanly possible to check them with a great deal of effort. There was a guy -- I forget his name, and Google isn't helping me! -- who, as his Ph. D. thesis, actually went through them and checked them I don't feel this is fundamentally different from the categorization of finite simple groups, which is also combining many small theorems and proofs, yet more widely accepted.
SilasX 4y ago
The same issues come up with interactive zero-knowledge proofs[A], where someone proves that they possess certain private information without leaking said information. The proofs have the form: 1) Give the prover a challenge that they only have a 50% chance[B] of passing if they don't possess the private info. 2) Repeat as necessary with new, independent challenges. 3) If they keep passing, hooray! The probability that it's a faker decays exponentially. You can get really high confidence, very quickly! Doing more rounds is just like re-running the computer proof. [A] I first learned about the issue from reading the Scott Aaronson lectures that became Quantum Computing Since Democritus [B] Doesn't have to be 50%, any figure will give the exponential decay and only require a linear increase in the number of rounds, so long as the probability stays the same between all rounds.
- bawolff 4y ago
  I fail to see the connection - new runs of the compuuter proof isn't going to randomize the code (like it does in zkp), so its not going to reduce the probability of error (excepting cosmic ray induced errors of course)
  - SilasX 4y ago
    Yes it is — the fact that the later computations got the same result is evidence that the earlier ones weren’t flukes. My comment above didn’t even mention randomization. That’s not necessary. All that’s necessary is that the tests be independent. Randomization is one way to achieve that but not a hard requirement. Even so, it seems you do see the connection, you just dispute one element that you think is critical.
    - bawolff 4y ago
      > My comment above didn’t even mention randomization. That’s not necessary. All that’s necessary is that the tests be independent. But they are obviously not independent. This is like flipping a coin once, looking at the result 20 times in a row (without flipping it again), concluding you have magic luck powers since you got heads twenty times in a row, and that would be really unusual in the analgous system where you flipped a coin 20 times instead of just looking at it. > Randomization is one way to achieve that but not a hard requirement. This is besides the point, but pray tell. How do you reduce the probability of an algorithm being incorrectly programmed by means of running it multiple times without changing the input or introducing some randomness somewhere? I don't think that's possible. Really the ZKP case isn't even checking the algorithm but checking a specific user input is consistent. I think this would be equivalent to denying that BPP without coin flips is P, which afaik it is. > Even so, it seems you do see the connection, you just dispute one element that you think is critical. I mean, i guess you could say that if you modify the system to add the connection you are trying to establish, then yes the connection becomes obvious.

Dove 4y ago

You're remembering entirely correctly! I gave a talk on the Four Color Theorem as part of my master's degree in 2001, and it was a somewhat active epistemic debate among mathematicians at the time. I took the position that examining code was no different than examining a proof, that running it through a computer was no different than running it through your brain, and that mathematicians are not shy at all about "automating" processes over uncountable infinities in proofs, so why should we be shy about automating them over thousands mechanically? There is a fun faith-shaking element to the story, though. The Four Color Theorem, as a proof, actually contains a couple thousand smaller proofs. These were generated and checked by a computer, but it is humanly possible to check them with a great deal of effort. There was a guy -- I forget his name, and Google isn't helping me! -- who, as his Ph. D. thesis, actually went through them and checked them. And IIRC, he found about a dozen errors! They weren't fatal -- he was able to repair them -- but that whole process didn't really reassure people. ;)

Dove 4y ago
AMS has a good summary: https://blogs.ams.org/mathgradblog/2014/06/29/color-theorem https://blogs.ams.org/mathgradblog/2014/06/29/color-theorem
- ghusbands 4y ago
  To save others the effort of reading - this only discusses the proof and not the by-hand check or "about a dozen errors" mentioned in the parent post.
anonymousDan 4y ago
How did the errors arise, some bug in the theorem prover?
- Dove 4y ago
  That's a really good question. I may have known the answer to it twenty years ago, but I don't now. XD What I can tell you is that it wouldn't have been so straightforward as that. We're not talking about an axiom-to-result symbolic proof piece of software like you might attempt to write now. It wasn't a computer proof so much as a computer-assisted proof. Lots of human analysis to describe specific properties, and then a computer program to check that a long list of geometric configurations had those properties. I don't know exactly what the program output as its proof, but I can only imagine the problems would have been small assumptions built into its design failing in corner cases. The theorem is notoriously difficult to reason about rigorously, and there have been a number of accepted proofs over the years that turned out to be false. It really doesn't help the whole situation that not only is it the first major computer-assisted theorem, it just happens to deal with a result that people are already wary of.
- puzzledobserver 4y ago
  The original computer assisted proof of the four colour theorem was written in IBM 370 assembler [0]. This was naturally susceptible to programming errors such as those discussed above. Gonthier's subsequent certified proof requires trust in a much smaller body of code and hardware [1]. [0] https://projecteuclid.org/journals/illinois-journal-of-mathematics/volume-21/issue-3/Every-planar-map-is-four-colorable-Part-II-Reducibility/10.1215/ijm/1256049012.full https://projecteuclid.org/journals/illinois-journal-of-mathe... [1] https://www.ams.org/notices/200811/tx081101382p.pdf https://www.ams.org/notices/200811/tx081101382p.pdf
dchftcs 4y ago
>The Four Color Theorem, as a proof, actually contains a couple thousand smaller proofs. These were generated and checked by a computer, but it is humanly possible to check them with a great deal of effort. There was a guy -- I forget his name, and Google isn't helping me! -- who, as his Ph. D. thesis, actually went through them and checked them I don't feel this is fundamentally different from the categorization of finite simple groups, which is also combining many small theorems and proofs, yet more widely accepted.

SilasX 4y ago

The same issues come up with interactive zero-knowledge proofs[A], where someone proves that they possess certain private information without leaking said information. The proofs have the form: 1) Give the prover a challenge that they only have a 50% chance[B] of passing if they don't possess the private info. 2) Repeat as necessary with new, independent challenges. 3) If they keep passing, hooray! The probability that it's a faker decays exponentially. You can get really high confidence, very quickly! Doing more rounds is just like re-running the computer proof. [A] I first learned about the issue from reading the Scott Aaronson lectures that became Quantum Computing Since Democritus [B] Doesn't have to be 50%, any figure will give the exponential decay and only require a linear increase in the number of rounds, so long as the probability stays the same between all rounds.

bawolff 4y ago
I fail to see the connection - new runs of the compuuter proof isn't going to randomize the code (like it does in zkp), so its not going to reduce the probability of error (excepting cosmic ray induced errors of course)
- SilasX 4y ago
  Yes it is — the fact that the later computations got the same result is evidence that the earlier ones weren’t flukes. My comment above didn’t even mention randomization. That’s not necessary. All that’s necessary is that the tests be independent. Randomization is one way to achieve that but not a hard requirement. Even so, it seems you do see the connection, you just dispute one element that you think is critical.
  - bawolff 4y ago
    > My comment above didn’t even mention randomization. That’s not necessary. All that’s necessary is that the tests be independent. But they are obviously not independent. This is like flipping a coin once, looking at the result 20 times in a row (without flipping it again), concluding you have magic luck powers since you got heads twenty times in a row, and that would be really unusual in the analgous system where you flipped a coin 20 times instead of just looking at it. > Randomization is one way to achieve that but not a hard requirement. This is besides the point, but pray tell. How do you reduce the probability of an algorithm being incorrectly programmed by means of running it multiple times without changing the input or introducing some randomness somewhere? I don't think that's possible. Really the ZKP case isn't even checking the algorithm but checking a specific user input is consistent. I think this would be equivalent to denying that BPP without coin flips is P, which afaik it is. > Even so, it seems you do see the connection, you just dispute one element that you think is critical. I mean, i guess you could say that if you modify the system to add the connection you are trying to establish, then yes the connection becomes obvious.