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.

6 Comments:

Blogger Philip 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 Unknown 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 Unknown 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