3 ms·

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 de

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

by Dove 4y ago

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.