God's Number is 20(cube20.org) |
God's Number is 20(cube20.org) |
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.
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".
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
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.
Vaporization would imply a complete dissociation of all the atoms.
Discussion there is closed as it's so old, so if you want to say anything new, this is the place to do 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.
So yes, your rewording is a distinct improvement.
Except it isn't. You are delusional if you think it is.
You're reading too much into it, I think.
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?
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))
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.
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.
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).