Hacker News Reader

Comment by qubex | Hacker News Reader

If I do not remember incorrectly, the proof of the Four Colour Theorem is essentially a brute-force one: a method of generating every possible graph that represents adjacency of tiling polygons on a 2D surface, and a subsequent colouring scheme for each and every one of them that never uses more than the desired four colours.

View on HN

There is a step in the proof which is brute force. The proof is sort of giving a recursive algorithm for 4-coloring: for certain subgraphs, you simplify it, color the result, and use the coloring to color the original graph. There are 633 cases ("reducible configurations") in the recursion, and the annoying part is checking that all 633 actually work. After Haken and Appel, Gonthier wrote a Coq proof http://www.ams.org/notices/200811/tx081101382p.pdf

Sometimes I imagine that if we had much larger short term memories, an argument with only 633 cases would be obvious.

I think the FCT proof doesn't generate every possible graph in that category (as there are infinitely many of them) but rather enumerates a very large set of compositional planar graphs such that all planar graphs are composed of combinations of subgraphs within the enumerated set

Yes, I think you are correct. I looked at it, and I looked into it, but only to grasp the general gist of it. The point was that essentially they reduced the infinite opportunities for tiling to a finite set of graphs whose composition covered the full spectrum of cases.

Everyone already strongly suspected that the FCT was true. Nobody was surprised by the result, it just took a computer to prove it.

The same is true of P != NP. And yet proving that would be a very big deal indeed (much as the FCT was).

Proving the opposite would be even bigger.

You clearly are not a mathematician (nor am I). There's a huge, unimaginably broad chasm cognitive chasm between "suspected", "conjectured", and "proved".

There is, according to quite a few, also a huge etc. chasm between 'proved' and 'proved by a computer'. Especially if it's a proof through exhaustive enumeration.

I disagree wholeheartedly. Proof by enumeration of finite cases is the most iron clad and idiot proof form of proof one can possibly aspire to. Proof by enumeration is fine and dandy. Some might cast a pall of disreputability upon a proof by enumeration by computer, but really it is no different — the computer and its program are merely a formal system somewhat more complicated and thus harder to inspect than mathematicians are used to, but this does not pose any real conceptual disconnect.

I understand the difference between the concepts. Im just saying the FCT result was not a 'surprising one', which the poster I responded to was implying.

Reply on news.ycombinator.com