I wrote a reply to a MathForge article on computers and mathematical proofs, which in turn is about the New York Times article In Math, Computers Don't Lie. Or Do They?. An interesting tidbit (that would otherwise remain obscurely buried in noise) is that solovay proved 0=1 with the HOL-light proof verifier.