Hacker News Reader

Comment by bmc7505 | Hacker News Reader

Has there ever been a brute force proof that discovered the existence of a solution previously thought impossible? Something like a new tiling or proof by contradiction that found a positive example?

View on HN

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.

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.

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.

Probably not what you were thinking of, but the counterexamples to Euler's sum of powers conjecture springs to mind. Despite being around for centuries, it took the use of a computer to find a counterexample.

https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjec...

I tried bruteforcing the prime equation using known mathematical functions concatenated in different ways with arbitrary constants converging on the distribution of primes. What's pretty cool is I got close to some academic research the produced the 'closest equation for prime approximation', which was a bunch of logarithms in a fraction. Really fun and worthwhile to play around with for problems thought to be impossible.

There has been a lot of examples generated by computer proving conjectures of their existence, I think a people now call this experimental mathematics. For instance in finite geometries, construction of new generalized quadrangles, flocks etc.

Reply on news.ycombinator.com