Monday, August 28, 2006

Proof


I read an article in New Scientist today about how computers are bringing uncertainty back into mathematics. Apparently you can never be sure that a proof that relies too heavily on computers is in fact correct, since there may be a bug somewhere in the code. I'm sure that you could write a program that would prove that the first program is indeed correct.

11 Comments:

Blogger ktazaco said...

This comment has been removed by a blog administrator.

8/28/2006 10:58 PM

 
Blogger ktazaco said...

Mark,

It is an interesting comment. Most software programs do have bugs. The precision of the mathmatics also deteriate after the limitations of the computer software has been put to its limits. So there are two problems here... One is buggy software the other is precision limitations of the computer system. I believe that the computer precision will eventually be overcome, but buggy software may alsways exist.

regards,
Steve

8/28/2006 11:01 PM

 
Blogger ktazaco said...

Mark,

It is an interesting comment. Most software programs do have bugs. The precision of the mathmatics also deteriate after the limitations of the computer software has been put to its limits. So there are two problems here... One is buggy software the other is precision limitations of the computer system. I believe that the computer precision will eventually be overcome, but buggy software may alsways exist.

regards,
Steve

8/29/2006 12:00 AM

 
Blogger ktazaco said...

Mark,

It is an interesting comment. Most software programs do have bugs. The precision of the mathmatics also deteriate after the limitations of the computer software has been put to its limits. So there are two problems here... One is buggy software the other is precision limitations of the computer system. I believe that the computer precision will eventually be be overcome, but buggy software may alsways persist.

regards,
Steve

8/29/2006 12:02 AM

 
Blogger Philip Northover said...

Computers have been used to prove some chess endgames. Apparently, rook and knight verses two knights is a win in 243 moves with best play on both sides. The move sequences don't seem to make much sense in places, they just are what they are. If you wanted to disprove the "proof", you could look for bugs in the program, or play the computer and see if you last longer than 243 moves... ;-)

That reminds me of another one. Two knights verses a lone king is drawn because the defender can set up a stalemate, but two knights verses a lone king and pawn can be a loss if the defender has to move his pawn while the knights move to deliver checkmate. There have been a few cases where the defender manages to promote his pawn to a queen, which would ordinarily be a win, only to be checkmated on the next move by a knight.

8/29/2006 8:41 AM

 
Blogger John S. Meade said...

Hmmmmm...

It appears some buggy software does exist already.
Reminds me of the Steve Martin line: ("I divorceth thee")**3.

And then there is the up and coming Quantum Computer... (hooo-boy!!)

And while we're speaking in 3's, think of the creativity done by our GreatGrandParents. And then, ok. Here we are. and look at what we are creating.

Given the technology climb-rate is uh uh geometric? logrithmic? the cube of arctan One?

Now think of the creativity our GreatGrandChildren will live and breathe and love in*.

My guess is this: The physical limitations of (human) bodies will eventually be overcome. But the meta programming of the human biocomputer will always have bugs.
-------------
*You know we love each other it's plain to see
There's just one answer comes to me
Sister lovers -- some of you must know about water brothers
And in time maybe others -- D. Crosby, "Triad"

8/29/2006 9:02 AM

 
Blogger Kerry Mitchell said...

"Formal methods" and "automated theorem proving" are two fields using computers to prove or verify stuff. Formal methods is gaining traction in fields where a failure would be costly enough to justify the expense of proving that the control software is bug free. Can you imagine using an operating system that had been proven to have no errors? Automated theorem proving can work for relatively simple theorems; formal methods can be used to verify that the theorem prover is correct.

8/30/2006 12:28 AM

 
Blogger Tim said...

I really like these "image" orbit traps. I didn't know it was possible to make a fractal image out of a graphic like this. Those spiralling eyes have quite a surreal look.

8/30/2006 10:35 PM

 
Blogger Keith said...

Tim, lately I have been obsessed with imported images:
http://segami.deviantart.com

8/31/2006 1:20 AM

 
Blogger Kerry Mitchell said...

Tim,

There are utilities now to make "image orbit traps" easy. Here's an article I wrote 5 years ago about how to do it by hand.

http://www.fractalus.com/kerry/articles/using-photos/using-photos.html

8/31/2006 2:06 AM

 
Blogger Tim said...

Thanks for links guys. There's always something new in fractal art. Or at least, new to me. How about using animated gifs? Then the eyes could be blinking :)

9/01/2006 12:15 AM

 

Post a Comment

<< Home