Well, we do have proof assistants. I think people are starting to use those in more diverse fields of math now--I remember seeing an article about an algebraic

Well, we do have proof assistants. I think people are starting to use those in more diverse fields of math now--I remember seeing an article about an algebraic proof in Coq, but I don't remember any of the details.