Slashdot Mirror
Are Computers Ready to Create Mathematical Proofs?
DoraLives writes "Interesting article in the New York Times regarding the quandary mathematicians are now finding themselves in. In a lovely irony reminiscent of the torture, in days of yore, that students were put through when it came to using, or not using, newfangled calculators in class, the Big Guys are now wrestling with a very similar issue regarding computers: 'Can we trust the darned things?' 'Can we know what we know?' Fascinating stuff."
> 'Can we know what we know?' Fascinating stuff.
Reminds me of Rumsfeld... "Reports that say that something hasn't happened are always interesting to me, because as we know, there are known knowns; there are things we know we know. We also know there are known unknowns; that is to say we know there are some things we do not know. But there are also unknown unknowns -- the ones we don't know we don't know."
Depends whether it's a Pentium with an FDIV bug, I imagine...
--
Don't like it? Respond with words, not karma.
there will be a computer that will automatically post on slashdot.
no.
q.e.d.
-
ping -f 255.255.255.255 # if only
???
BOOM!
"Cleanup in aisle 10"
The answer is left as an exercise for the reader.
That's ok, Jesus likes me anyway.
Mathematics is just Symbol Manipulation. I suspect computers are pretty good at that.
;)
Also, chess is just Pattern Matching... I don't know if humans have the edge there or not.
The obvious solution is to have the computer create a new proof that shows that the algorithm it used to create the original proof is, in fact correct.
A marriage is always made up of two people who are prepared to swear that only the other one snores.
Come on, this is just comparing Appels and oranges
No matter what the proof, don't we still have to accept blindly on faith that A=A?
Sure, it seems highly probable but.. I just.. I guess I'm a skeptic. All of logic seems like a joke to me, as long as this one little potentially huge loophole looms in the background...
Spoon not. Fork, or fork not. There is no spoon.
Fortunately for you software researchers haven't programmed computers to create their own long sentences with so many prepositions that human readers of the created sentences are unable to remember the subject or figure out which verb, or possibly adjective, the trailing adverb applies to by the time they have read the entire sentence yet!
my blog
"I don't know, a proof is a proof. What kind of a proof is a proof? A proof is a proof and when you have a good proof it's because it's proven."
(PM Jean Chretien, when asked what kind of proof he would need of weapons of mass destruction in Iraq before deciding to send Canadians along on the Bush invasion-September 5th on CTV news)
"For a famous example, it would provide a great deal of peace of mind if we could prove that P != NP."
Well, P == NP for N = 1.
That's the beauty of a counter example.
DATA comments; PROC SORT DATA = comments BY score; PROC DELETE comments >> 1; RUN; DATA entertainment SET commen
i asked mine it said "no"
Can you please tell us The Question?
...No. But I'll tell you who can.
The Ultimate Question?
Yes!
Of Life, The Universe..
And everything?
And Everything.
Yes.
Tricky..
But can you do it?
Who? Tell us!
I speak of none, but the computer that is to come after me.
What computer?
A computer whose merest operational parameters I am not worthy to calculate and yet I will design it for you. A computer which can calculate The Question to the Ultimate Answer. A computer of such infinite and subtle complexity that organic life itself will form part of it's operational matrix. And it will be called.. The Earth.
What a dull name.