Timothy Gowers’ mathematical writing experiment, which we reported on last month, has now concluded and the results are available. The experiment concerned a set of proofs of results on metric spaces; Gowers sought opinions on how well-written and understandable each one is.
It turns out that experiment was a ruse!: Gowers revealed on his blog that he has been working on a program which can produce human-readable proofs of propositions, and its proofs were smuggled in amongst two others written by humans. After revealing that, he asked for people to tell him which proofs were the computer’s. He’s just published the results of that second experiment on his blog, along with a description of the program.