8
$\begingroup$

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.

$\endgroup$
13
$\begingroup$

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.

  2. W. T. Gowers, An experiment concerning mathematical writing.

  3. M. Ganesalingam, W. T. Gowers, A fully automatic problem solver with human-style output.

  4. M. Wenzel, Isabelle/Isar - a versatile environment for human-readable formal proof documents.

  5. F. Wiedijk, A Synthesis Of The Procedural And Declarative Styles Of Interactive Theorem Proving.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – SorcererofDM Jul 24 '15 at 16:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.