As well as general intellectual interest and the study of artificial intelligence, automated theorem proving has been applied both to problems in pure mathematics and computer system verification, and I'll describe some interesting instances.