<p>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). </p>

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

<hr>

<ol>
<li><p>M. Ganesalingam, <a href="http://people.ds.cam.ac.uk/mg262/">A Language for Mathematics</a>.</p></li>
<li><p>W. T. Gowers, <a href="https://gowers.wordpress.com/2013/03/25/an-experiment-concerning-mathematical-writing/">An experiment concerning mathematical writing</a>.</p></li>
<li><p>M. Ganesalingam, W. T. Gowers, <a href="http://arxiv.org/abs/1309.4501">A fully automatic problem solver with human-style output</a>.</p></li>
<li><p>M. Wenzel, <a href="https://mediatum.ub.tum.de/doc/601724/601724.pdf">Isabelle/Isar - a versatile environment for human-readable formal proof documents</a>.</p></li>
<li><p>F. Wiedijk, <a href="http://arxiv.org/abs/1201.3601">A Synthesis Of The Procedural And Declarative Styles Of Interactive Theorem Proving</a>.</p></li>
</ol>

CC BY-SA 3.0
2015-07-24T16:30:50.397Z
Thanks for all the pointers. Reading Ganesalingam's paper with Gowers, I don't feel particularly convinced by its intuitions and methods. Some of the claims about the human mathematician don't feel grounded to me, like not having the problem of combinatorial explosion. It seems to me that it's more the case that the human mathematician is lazy in pursuing a full search.
SorcererofDM
CC BY-SA 3.0
2015-07-23T11:18:35.220Z
2015-07-23T14:22:54.667Z
2015-07-23T14:22:54.667Z
Martin Berger
<p>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.</p>

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

<proofs><proof-assistants>
Humanifying computer-generated or computer assisted proofs
SorcererofDM
# Humanifying computer-generated or computer assisted proofs

(Asked by: username_0 on 2015-07-23)

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.

**Tags:** proofs, proof-assistants

---

## 1 answers

### Answer by username_1 on 2015-07-23. Score: 13

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.

---

1. M. Ganesalingam, [A Language for Mathematics](http://people.ds.cam.ac.uk/mg262/).
2. W. T. Gowers, [An experiment concerning mathematical writing](https://gowers.wordpress.com/2013/03/25/an-experiment-concerning-mathematical-writing/).
3. M. Ganesalingam, W. T. Gowers, [A fully automatic problem solver with human-style output](http://arxiv.org/abs/1309.4501).
4. M. Wenzel, [Isabelle/Isar - a versatile environment for human-readable formal proof documents](https://mediatum.ub.tum.de/doc/601724/601724.pdf).
5. F. Wiedijk, [A Synthesis Of The Procedural And Declarative Styles Of Interactive Theorem Proving](http://arxiv.org/abs/1201.3601).

> **Comments:**
> **username_0**: Thanks for all the pointers. Reading Ganesalingam's paper with Gowers, I don't feel particularly convinced by its intuitions and methods. Some of the claims about the human mathematician don't feel grounded to me, like not having the problem of combinatorial explosion. It seems to me that it's more the case that the human mathematician is lazy in pursuing a full search.  

---

