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

Rumsfeld, anyone?

[dolo666]

> 'Can we know what we know?' Fascinating stuff.

Reminds me of Rumsfeld [about.com]... "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."

'Can we trust the darned things?'

[FFFish]

Depends whether it's a Pentium with an FDIV bug, I imagine...

Next thing you know....

[Anonymous Coward]

there will be a computer that will automatically post on slashdot.

no

[sporty]

no.

q.e.d.

Rumsfeld, anyone?-Overload.

[Anonymous Coward]

???
BOOM!

"Cleanup in aisle 10"

Wait, I know this one...

[bomb_number_20]

The answer is left as an exercise for the reader.

making hard things easy...

[Polo]

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 stack might get a bit deep, but...

[Odin's Raven]

'Can we trust the darned things?' 'Can we know what we know?'

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.

And to prove that the proof of the proof can be trusted, have the computer create a proof of the proof of the proof.

And to prove that the proof of the proof of the proof can be trusted, ...

A rather timely Slashdot fortune

[Anonymous Coward]

What I see on the bottom of the page as I read this topic discussion is:

The truth of a proposition has nothing to do with its credibility. And vice versa.

Re:Rumsfeld, anyone?

[kfg]

Are you sure?

KFG

Re:4 color map problem

[Old Wolf]

Come on, this is just comparing Appels and oranges

identity

[chocolatetrumpet]

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...

Re:Create vs. Verify

[panaceaa]

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!

Canada's former prime minister's "proof"

[Anonymous Coward]

"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 [bayrak.ca], 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)

Re:Rumsfeld, anyone?

[Deraj DeZine]

Well, I had been in the don't care that I don't know category; now I'm in the don't care that I know. Great.

Re:Create vs. Verify

[sisco]

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

Re:Rumsfeld, anyone?

[jgabby]

Then there's:

My boss, who knows that he knows not;
But pretends that he knows that he knows;
And he's so convincing at it, that;
People who know that he doesn't know;
Beleive that he knows that he knows anyway.

are computers ready?

[fluxmix]

i asked mine it said "no"

Re:Create vs. Verify

[eliza_effect]

Can you please tell us The Question?

The Ultimate Question?

Yes!

Of Life, The Universe..

And everything?

And Everything.

Yes.

Tricky..

But can you do it?

...No. But I'll tell you who can.

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.