Humanifying computer-generated or computer assisted proofs
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.