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