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 /.
(who calls it a prank), among many others
Today, 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.