God's Number is 20
cube20.orgSort of like the Four Color Theorem, in that it's something that was proven with computers and brute force. I remembering hearing mathemeticians were upset about it because it just felt wrong to prove it that way (this was the 70s, it may have been the first proof that was done by machine) http://en.wikipedia.org/wiki/Four_color_theorem
My math teacher in high school (this was before Wikipedia) told our calculus class at the beginning of the year if we could prove how to only use four colors on a map without any similar colors touching, he'd give us a 4.0 for the class.
Years later and long after I had forgotten most of the math I learned, I saw the four color theorem on Wikipedia and got such a kick out of the absurdity of my teacher's offer.
Brought it up with him when I randomly bumped into him a little bit ago, he got quite a kick out of it.
That's right, The Four Color Theorem was the first such proof.
Mathematicians weren't so much "upset" as "not sure what to make of it". Technically, the "proof" wasn't really a proof at all, because it relied on the operation of a computer program, and the compiler / OS / hardware stack upon which the program operated had not been rigorously verified.
Even if it HAD been verified, there's still the question of whether transistors always work in the way we believe....
Of course, over the years, the Four Color Theorem has been checked 100s of times, with many different software / hardware stacks. But to a purist, this still only counts as "strong evidence" rather than "proof".
It's weird to say that and still count written proofs. There's still the question of whether neurons always work in the way we believe...
Shh! Don't tell them that. You'll hurt their feelings.
I genuinely find it hard to believe mathematicians could function professionally as mind-body dualists, especially given how many major mathematicians are non-neurotypical.
>this still only counts as "strong evidence" rather than "proof".
Please allow me to disagree. Georges Gonthier proved the Four Color theorem using the proof assistant Coq, which is as much of a certainty as you're ever likely to get for a mathematical proof. http://www.ams.org/notices/200811/tx081101382p.pdf
I suppose you could just forge your own silicon and software and submit that as part of the proof.
No. That wouldn't be sufficient. Here's why.
Imagine that I built a machine and told you, "Press this button here. If P=NP, the lamp will turn on. If P!=NP, the lamp will not turn on." What would you make of it?
So what if I opened up the machine, and showed you all the components, would that convince you?
I think you'd only be convinced, if:
1. We could agree on some basic axioms of how the basic components of the machine operates.
2. From those axioms, I could prove the proposition that, for a machine of this design, the lamp will turn on if and only if P=NP.
I think that, one day, somebody WILL construct a formally verified silicon system capable of proving the four color theorem. (Putting aside the issue of unreliable logic gates.) But I don't think it will be in some high-level system like Coq, because there are so many layers of abstraction we would have to formally verify. I think it's more likely that the logic would be implemented directly in silicon.
It's still a proof, just an inelegant one. But I agree, it's considerably different than standard proofs, since it doesn't explain "why".
We broke the problem down into 2,217,093,120 smaller problems
Off topic, but this is a brilliant sentence to use especially outside of the original context. Like if you broke someone else's ugly vase.
If it's in that many pieces, I think the word is vaporized.
Aerosolized. Starting from a couple dozen moles, you'd end up with quintillions of atoms in each piece, which would be solid, invisible to the naked eye, but visible under a microscope (about an order of magnitude larger than the average eukaryote).
Vaporization would imply a complete dissociation of all the atoms.
I think we're quite a few orders of magnitude short of that. "Disintegrated" or "aerosolized" are probably closer.
aerosolved
There was significant discussion of this in an earlier submission: https://news.ycombinator.com/item?id=1587340
Discussion there is closed as it's so old, so if you want to say anything new, this is the place to do it.
These results are really cool because first when you look at such a problem space, the size may look insurmountable but with clever algorithms one can always hope to solve it in reasonable time. Whether 35 CPU years is reasonable, I don't know. :)
Other researchers did a similar thing to prove that a sudoku puzzle needs at least 17 clues to make a unique grid. They went from 6.7E21 possible grids to check, to 5.4E9 possible grids to check. http://www.youtube.com/watch?v=MlyTq-xVkQE
It's not. But if you've been donated the spare cycles, it's easier to use them than to spend time optimizing a difficult algorithm.
I wonder why Google donated spare cycles to solve the Rubik's cube when there are problems like Fold.it that could use it for science.
Probably for more or less the same reason that you are using your computer to chat online, rather than dedicating all of its cpu cycles for science.
>I wonder why Google donated spare cycles to solve the Rubik's cube when there are problems like Fold.it that could use it for science.
An equally absurd question: Why doesn't google use all of it's man/computing power for science instead of trying to make money from internet ads?
So you're implying that donating cycles to solve the Rubik's cube is making them money?
I don't see how my comment implied that, at all.
But yes, yes it did.
Probably? (jadedly) It's a cheap one off that earns them a lot of free publicity.
Folding and SETI have been at it for decades, and will be for decades more. That'd be a lot of power/hardware costs for little net gain modulo time spent.
(Note: 30 cpu years really isn't a lot of time when you start getting truly massive parallelism, and google is certainly at that scale. I'm honestly surprised to see this is pthreads based, I would have expected it to lean heavily on CUDA (or maybe I'm just showing my naivete to the field of parallel programming))
Just to put some numbers behind this:
35 CPU years = 35 * 365 = 12,775 CPU days
Let's assume that your standard Google machine has 2 8-core processors, that is 16 cores per machine
12,775 / 16 = 798 machines
800 machines is a lot for your average person, but for a company like Google it is a very small drop in the bucket. And that is assuming you need to do all of the calculations in one day. If you are willing to do the calculations over a month, you only need 26 machines.
Even if "CPU year" applies to one 8-core processor, that still means it is just 26 * 8 = 416 machines, which is a very small number for Google.
And remember, the machines are still doing other things, this is just using idle CPU (generally a plentiful resource for your standard internet giant workload).
It would seem to me that this kind of program would be heavily reliant on branching for which Vector processing (which is what GPUs excel at) is not the best choice.
CUDA is for GPUs (specifically NVIDIA GPUs). This is CPU processing. Pthreads is the way to go.
Google has also donated cycles to at least one scientist working on the protein folding problem; he's a friend of mine, and also happens to be a fan of the Rubik's cube.
Because it's cool.
One day someone will turn lead into gold. There will never be a "good" reason to do that, but the history behind it is sufficient. There's nothing wrong with taking some pride in accomplishing something you've always wanted to do.
The idea that someone somewhere should pick a goal and then all the resources anyone could conceivably spare must be devoted to it, on pain of a designation of "immoral", is a little more disturbing to me.
That's a valid question. Although I didn't appreciate fold.it that much since the software crashed immediately when I tried it.
I'm surprised we couldn't have proven this analytically.
I'm more surprised that they were able to prove it computationally.
You are? That surprises me. Do you have a background in algebra?
It is sad, but Erdos and Renyi are no more.
It's a shame about the religious babble brought into this by the people who ran it.
"One may suppose God would use a much more efficient algorithm"
It still could have been fun and been along the lines of "One may suppose a god would use a much more efficient algorithm"
But there's only one true god evidently. Lets ignore those stupid religions that have many gods.
I'm not religious and I do get pissed off by the idea of things like "teaching the controversy" when it comes to creationism and such, but the wording here doesn't really bother me at all; it just seems like a shorthand way of describing a being generally accepted to be omniscient to easily put forth the concept of a completely perfect solution regardless of the initial state.
While I'm reflexively inclined to disagree, one must remember how Einstein's casual pantheistic use of the word was twisted and distorted by others. The word 'god' is so overloaded with meaning that it's best to avoid even when the intent is honorable.
So yes, your rewording is a distinct improvement.
It's a metaphor that's probably understood by everyone who reads it, which is the point. Besides, the English lexicon is full of vestigial words and phrases relating to Greek polytheism, they're just as detached as this metaphor is.
>they're just as detached as this metaphor is.
Except it isn't. You are delusional if you think it is.
That's a great argument, I'm convinced.
It's shorthand for "optimal." Assuming an omniscient god, he would be able to always solve a Rubik's Cube in the minimum (optimal) number of moves.
You're reading too much into it, I think.
Interesting!
There are asians who solve the cube in less than 30 moves every time. ¿Are asians closest to be God?
i thought god's number was seven: https://www.youtube.com/watch?v=HsHITZRCgqs&feature=kp
Not really http://en.wikipedia.org/wiki/God's_algorithm
Dammit. Mine is 8 and She takes an absolute eternity at the cheese counter.