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.)
Comments