Q:

Humanifying computer-generated or computer assisted proofs

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. 

A:

You are probably thinking of Gower's work with Ganesalingam, based on the latter's MSc dissertation (1).  Gowers blogged about this in (2) and other places, and they've written a paper on the subject (3).  
There is other work in that direction, for example from the interactive proof assistant community.  The most well-known example here might be the Isar language (4).  This is quite an active area of research, see e.g. (5).  I know that this is also pursued by more linguistics oriented researchers, but I don't have references handy. 

M. Ganesalingam, A Language for Mathematics. 
W. T. Gowers, An experiment concerning mathematical writing. 
M. Ganesalingam, W. T. Gowers, A fully automatic problem solver with human-style output. 
M. Wenzel, Isabelle/Isar - a versatile environment for human-readable formal proof documents. 
F. Wiedijk, A Synthesis Of The Procedural And Declarative Styles Of Interactive Theorem Proving.