5 ms·

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 contr

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?

qubex 9y ago
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.
- kmill 9y ago
  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 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.
- opportune 9y ago
  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
  - qubex 9y ago
    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.
- bjl 9y ago
  Everyone already strongly suspected that the FCT was true. Nobody was surprised by the result, it just took a computer to prove it.
  - opportune 9y ago
    The same is true of P != NP. And yet proving that would be a very big deal indeed (much as the FCT was).
    - cestith 9y ago
      Proving the opposite would be even bigger.
  - qubex 9y ago
    You clearly are not a mathematician (nor am I). There's a huge, unimaginably broad chasm cognitive chasm between "suspected", "conjectured", and "proved".
    - Confusion 9y ago
      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.
      - qubex 9y ago
        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.
    - bjl 9y ago
      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.
deleted 9y ago
[deleted]
netsec_burn 9y ago
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.
kirrent 9y ago
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_conjecture https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjec...
the6threplicant 9y ago
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.

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?

qubex 9y ago

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.

kmill 9y ago
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 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.
opportune 9y ago
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
- qubex 9y ago
  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.
bjl 9y ago
Everyone already strongly suspected that the FCT was true. Nobody was surprised by the result, it just took a computer to prove it.
- opportune 9y ago
  The same is true of P != NP. And yet proving that would be a very big deal indeed (much as the FCT was).
  - cestith 9y ago
    Proving the opposite would be even bigger.
- qubex 9y ago
  You clearly are not a mathematician (nor am I). There's a huge, unimaginably broad chasm cognitive chasm between "suspected", "conjectured", and "proved".
  - Confusion 9y ago
    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.
    - qubex 9y ago
      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.
  - bjl 9y ago
    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.

deleted 9y ago

[deleted]

netsec_burn 9y ago

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.

kirrent 9y ago

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_conjecture https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjec...

the6threplicant 9y ago

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.