Machines No Threat to Mathematicians

Last month, a team of computer scientists from Google demonstrated a machine-learning program that can prove a class of mathematical theorems on its own. Like other such programs —whose applications now range from facial recognition to stock trading—the algorithms behind it were ‘trained’ on a data set. In this case, it was a set of theorems already proved by humans, their proofs, along with specific tactics used in the proofs. The Google team’s achievement is the latest milestone in a long journey to obtain computer-aided proofs of mathematical theorems. It started in the mid-1970s when a seemingly intractable mathematical problem—the Four Colour Theorem—was proved using a computer. Does this mean that eventually mathematicians will be as relevant as musketeers are now? Not quite. To understand why, we must dig a little deep into the practice of mathematics which entails four related tasks. The most sophisticated outsider would guess that a practising mathematician proves theorems. This brings me to the first task in the practice of mathematics: the identification of problems to solve. Discounting the merely amusing and the manifestly trivial—the playground of schoolchildren and amateurs—a mathematical problem worth solving is either a legacy (in that it has been passed on from generations before) or is discovered in a burst of inspiration. While the first makes intuitive sense—and fits the public’s understanding of what it means to solve a ‘hard maths problem’—it’s the second that is baffling. And what is even more curious is that often a newly discovered problem—even though not yet proved—may lead you to a proof of a legacy problem. Let me explain by means of a famous example. Consider the equation a²+b²=c² where ‘a’, ‘b’ and ‘c’ are natural numbers (1, 2, 3,…). Since the time of the ancient Greeks, it is known that this equation has infinitely many solutions—this just means that there are infinitely many ‘a’, ‘b’ and ‘c’ that satisfy it. Now, consider the slightly tweaked aⁿ+bⁿ=cⁿ where ‘n’ is a number greater than 2. How many solutions does this equation have? In 1637, French mathematician Pierre de Fermat claimed—without a proof—that it does not have any. While this would be proven for some special values of ‘n’ over the next two hundred years, the problem would stubbornly resist solution till 1994, when Princeton professor Andrew Wiles would succeed in proving this for all cases thereby establishing Fermat’s Last Theorem. How he would go about it illustrates the point I set out to make. Travel back to mid-1950s Japan when two mathematicians at the University of Tokyo, Yutaka Taniyama and Goro Shimura, make a spectacular conjecture between two completely unrelated objects in mathematics: elliptic curves (geometry) and modular forms (numbers) —something a computer program of the kind Google demonstrated last month would find inexplicable. The Taniyama-Shimura Conjecture has, on the face of it, nothing to do with Fermat’s Last Theorem. It was only in the 1980s that mathematicians showed that if one could prove this, one would automatically have a proof of Fermat’s Last Theorem—which is what Wiles did after a decade-long struggle. This story also brings me to the second task in the practice of mathematics: of building bridges and analogies between subdisciplines no one thought were related. In many ways, the maths we learn in school today also started this way. Euclid’s geometry gave way to calculating distances using algebra through coordinates. The resulting Cartesian geometry has linked algebra and geometry as a single mathematical subject. Or take the discipline of analytic number theory that uses methods of calculus (which is about continuity) to talk about the integers (which are discrete). Over the last 40 years or so, a powerful research program has emerged that has pushed these ideas stratospherically—towards an overarching ‘Theory of Everything’ of sorts in pure mathematics from which solutions to several outstanding problems in number theory would follow: for the cognoscenti, I am referring to the Langlands Programme. While significant progress has been made in the past 10 years in proving key statements in this mother-of-all-theories, large swathes of the program remain conjectural. And at the heart of this vast research agenda lies a mysterious mathematical core: motives. First intuited by mathematical legend Alexander Grothendieck, a ‘motive’ is a recurring pattern in many branches of modern number theory and geometry. If motives exist in ways mathematicians expect them to, several outstanding problems in number theory and geometry will be resolved. Recent work suggests that motives may also be relevant to the mathematics of particle physics and string theory. And therein lies the third task in the practice of mathematics: of cultivating imagination. Computers are not very good at this. And like humans, you can’t train them to imagine. But at the end of the day, mathematical mental leaps, however striking, must be given form through the cold clay of logic. This brings me to the final task in the practice of mathematics: establishing rigorous proofs of assertions. Modern mathematical theories are like soaring cathedrals albeit with intricate, delicate foundations of careful sequential, logical arguments—pull one little strand in the cellar and the whole thing would collapse. And this is where checking each step of every proof carefully in an elaborate mathematical theory becomes an imperative. This is where computer programs could come in. It is striking that one of the fathers of the theory of motives, the late Institute for Advanced Study, Princeton, mathematician Vladimir Voevodsky, initiated an entire research agenda to rewrite the foundations of mathematics so that computers could verify mathematical proofs after he found a mistake in one of his own papers related to that mysterious theory that binds numbers to shapes. (Abhijnan Rej is a defence analyst who studied, researched and taught pure mathematics and theoretical physics in three continents)