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.
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.
