Sort 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".
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
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.
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.
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
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))
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.
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.
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.
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.
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.
