Comment by Dove | Hacker News Reader

Comment by Dove | Hacker News Reader

Parent Full thread

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. ;)

AMS has a good summary: https://blogs.ams.org/mathgradblog/2014/06/29/color-theorem

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.

How did the errors arise, some bug in the theorem prover?

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.

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

[1] https://www.ams.org/notices/200811/tx081101382p.pdf

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

Reply on news.ycombinator.com