I can't let you think that, Dave.

Two students at MIT recently wrote a program called SciGen, which randomly generates Computer Science research papers. Last week, one of their randomly generated papers got accepted to a conference. This was covered on /. and CNN (who calls it a prank), among many others.

Today, NewScientist.com is reporting that a Microsoft research lab in Cambridge, UK has verified a mathematical proof computationally. The Four-Color Theorem claims that any map in two dimensions can be colored using only four colors such that no two regions sharing a boundary are the same color. Benjamin Werner and Georges Gonthier translated a proof into Coq, a logic checking proof assistant, which subsequently verified the logical validity of their work. (Note that the Wikipedia entry on the Four-Color Theorem says happened in September 2004.)

The apparently belated report of this development by New Scientist also includes an interview with Randy Pollack from Edinburgh University. I agree with Pollack that the a logic checking application would be useful in computer programming, and extending this technology to other disciplines could be very useful. Pollack goes on to tell New Scientist that,

I've found instances where I'm doing things in a completely different way simply because I'm using a computer.

Me too, Randy, me too.