### 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.

Comments