Seventy four minutes of mathematics: An analysis of the third mini-polymath project

Alan Turing proposed to consider the question, “Can machines think?” in his famous article [38]. We consider the question, “Can machines do mathematics, and how?” Turing suggested that intelligence be tested by comparing computer behaviour to human behaviour in an online discussion. We hold that this approach could be useful for assessing computational logic systems which, despite having produced formal proofs of the Four Colour Theorem, the Robbins Conjecture and the Kepler Conjecture, have not achieved widespread take up by mathematicians. It has been suggested that this is because computer proofs are perceived as ungainly, brute-force searches which lack elegance, beauty or mathematical insight. One response to this is to build such systems which perform in a more human-like manner, which raises the question of what a “human-like manner” may be.
Timothy Gowers recently initiated Polymath [4], a series of experiments in online collaborative mathematics, in which problems are posted online, and an open invitation issued for people to try to solve them collaboratively, documenting every step of the ensuing discussion. The resulting record provides an unusual example of fully documented mathematical activity leading to a proof, in contrast to typical research papers which record proofs, but not how they were obtained.
We consider the third Mini-Polymath project [3], started by Terence Tao and published online on July 19, 2011. We examine the resulting discussion from the perspective: what would it take for a machine to contribute, in a human-like manner, to this online discussion? We present an account of the mathematical reasoning behind the online collaboration, which involved about 150 informal mathematical comments and led to a proof of the result. We distinguish four types of comment, which focus on mathematical concepts, examples, conjectures and proof strategies, and further categorise ways in which each aspect developed. Where relevant, we relate the discussion to theories of mathematical practice, such as that described by Polya [34] and Lakatos [22], and consider how their theories stand up in the light of this documented record of informal mathematical collaboration.