I remember reading a blog post displaying two versions of the same proof, one written by a human and the other by a machine, and asked the readers to tell which is which. Trying to google the post again, I can't seem to find the right keywords; most things just direct me to pages on computer generated or computer assisted proofs.
So I'm wondering if anyone else remembers such a post, or better yet, can direct me to some surveys or other materials on this subject.