Wednesday, 9 July 2003

Proofs and computers

Listening to:

Francesco Silvestrino, O dio se vede chiaro. From a BBC Music Magazine CD called The Glory of Venice, featuring 16th century Venetian music.

Weapons of mass destruction; can’t live with ’em, can’t live without ’em.

A recent article from Nature on a proof whose status is unclear because a computer was used to check lots of tedious cases. The proof of the four colour theorem was also constructed with a computer's help and is viewed with similar suspicion. (But maybe a proof in a theorem-proving system would be worthy of more respect? Some people are working on this, including Gertrud Bauer and Tobias Nipkow.)

A nice article on irony, what it is and isn’t.