Mathematical Turing test: Readable proofs from your computer

April 15, 2013 by Artem Kaznatcheev 10 Comments

We have previously discussed the finicky task of defining intelligence, but surely being able to do math qualifies? Even if the importance of mathematics in science is questioned by people as notable as E.O. Wilson, surely nobody questions it as an intelligent activity? Mathematical reasoning is not necessary for intelligence, but surely it is sufficient?

Note that by mathematics, I don’t mean number crunching or carrying out a rote computation. I mean the bread and butter of what mathematicians do: proving theorems and solving general problems. As an example, consider the following theorem about metric spaces:

Let X be a complete metric space and let A be a closed subset of X. Then A is complete.

Can you prove this theorem? Would you call someone that can — intelligent? Take a moment to come up with a proof.

One of the beauties of mathematics, is that theorem proving is a creative and unique endeavour — different individuals can come up with very different proofs and present them in a variety of ways. As an example, consider three proofs of the above theorem:

Consider an arbitrary Cauchy sequence $(x_n)_{\{n \in \mathbb{N}\}}$ in $A$ . As $X$ is complete, $(x_n)$ has a limit in $X$ . Suppose $\lim_{n \rightarrow \infty} x_n = x$ . Because $A$ is closed, $x$ belongs to $A$ . We’ve proved that every Cauchy sequence in $A$ has a limit point in $A$ . So $A$ is complete.
Let $(a_n)$ be a Cauchy sequence in $A$ . Then, since $X$ is complete, we have that $(a_n)$ converges. That is, there exists $a$ such that $a_n \rightarrow a$ . Since $A$ is closed in $X$ , $(a_n)$ is a sequence in $A$ and $a_n \rightarrow a$ , we have that $a \in A$ . Thus $(a_n)$ converges in $A$ and we are done.
Let $(a_n)$ be a Cauchy sequence in $A$ . We want to show that $(a_n)$ tends to a limit in $A$ .

Since $A$ is a subset of $X$ , $(a_n)$ is a Cauchy sequence in $X$ . Since $X$ is complete, $a_n \rightarrow a$ , for some $a \in X$ . Since $A$ is a closed subset of $X$ , it must contain all its limit points, so $a \in A$ . So $a_n \rightarrow a$ in $A$ . So $A$ is complete.

Since the theorem is simple the ideas of the three proofs are the same, but the presentation differs. How would you rate these proofs on clarity and style?

On March 25th, this is exactly the question that Fields medalist Timothy Gowers asked his blog readers about this and four other theorems. The comments flooded with ratings and discussions of the proofs. Nobody suspected that the authors of the proofs were a graduate student, undergraduate student, and unsupervised computer. Eight days later, Gowers revealed the identity of the authors but not which wrote each answer. Instead, he asked his readers to identify which proof was written by an artificial intelligence. What do you think? Can you distinguish mathematician from machine?

Similar to the economic and psychometric Turing tests we saw earlier, this is a restriction on modality of the standard Turing test. In the standard test, the judge uses an instant messaging program to chat with the human and the machine, without knowing which is which. At the end of a discussion (which can be about anything the judge desires), she has to determine which is man and which is machine. If judges cannot distinguish the machine more than 50% of the time then it is said to pass the test. In Gowers’s mathematical Turing test, instead of asking questions, the judge can provide theorem statements and the participants must respond with a proof.

Theorem provers and assistants were some of the earliest motivations of artificial intelligence and — in one form or another — have existed for decades. Unfortunately, these computers presented their convoluted arguments in symbolic gibberish that one could only find human analogues of on the pages of Russell and Whitehead’s Principia Mathematica:

Professional mathematicians, however, usually really on English mixed with only occasional symbols. In fact, mathematics has a language all its own. A linguist’s dream, the language has the basic flavor and ambiguities of English combined with the precision of logical deduction. It provides a way to go beyond completely artificial syntactic structures of abstract languages without being lost in ambiguity and semantics as colorless green ideas sleep furiously.

Conviniently, Mohan Ganesalingam defended his computational linguistics Ph.D. with a complete analysis of formal mathematical language. In the three years since his graduation, he has been working with Gowers in developing the ideas behind a theorem prover that imitates human mathematicians and writes proofs in the language you might find in textbooks or journals.

The results of the Mathematical Turing test are presented to the right. The figure plots the results of the regular readers of Gowers’s Weblog. There are five columns corresponding to the questions, question 3 is the one at the start of this post. Blue shows the proportion that properly identified the computer, the green shows those that thought the undergrad was a computer, yellow thought the graduate was a computer, and red could not identify any of the three proofs as computer generated. The white line marks the 50% performance, and the black line marks the 33% performance — the expected result if the judges were guessing randomly. For question 3, at least, the AI passed the mathematical Turing test. For the other four questions, almost half of the respondents could not accurately identify the computer.

These results are preliminary, and shared on web in the the spirit of open science that Gowers’s has worked hard to promote among mathematicians. The authors have not released their Haskell code, but it seems like they plan to. I can’t wait to see the final results, code, and write up for the project. Will we have to question the relationship between intelligence and mathematical reasoning? Until then, I encourage you to read Gowers’s post that presents the results and project in greater detail and reveals which proof is computer generated.

Ganesalingam M. (2013). The Language of Mathematics: A Linguistic and Philosophical Investigation, Lecture Notes in Computer Science, 7805 DOI: 10.1007/978-3-642-37012-0

Filed under Commentary Tagged with Alan Turing, artificial intelligence, Bertrand Russell, cognitive science, cstheory, current events, empirical, intelligence, philosophy of math, realistic model

About Artem Kaznatcheev
From the Department of Computer Science at Oxford University and Department of Translational Hematology & Oncology Research at Cleveland Clinic, I marvel at the world through algorithmic lenses. My mind is drawn to evolutionary dynamics, theoretical computer science, mathematical oncology, computational learning theory, and philosophy of science. Previously I was at the Department of Integrated Mathematical Oncology at Moffitt Cancer Center, and the School of Computer Science and Department of Psychology at McGill University. In a past life, I worried about quantum queries at the Institute for Quantum Computing and Department of Combinatorics & Optimization at University of Waterloo and as a visitor to the Centre for Quantum Technologies at National University of Singapore. Meander with me on Google+ and Twitter.