(Image: Roya Hamburger)
AFTER three years, Shinichi Mochizuki is still waiting. In 2012, the highly respected mathematician at Kyoto University in Japan published more than 500 pages of dense maths on his website. It was the culmination of years of work. Mochizuki鈥檚 inter-universal Teichm眉ller theory described previously uncharted areas of the mathematical realm and let him prove a long-standing conundrum about the true nature of numbers, known as the ABC conjecture. Other mathematicians hailed the result, but warned it would take a lot of effort to check. Months passed, then years, with no conclusion.
Advertisement
Ask a mathematician what a proof is and they鈥檙e likely to tell you it must be absolute 鈥 an exhaustive sequence of logical steps leading from an established starting point to an undeniable conclusion. But that鈥檚 not the whole story. You can鈥檛 just publish something you believe is true and move on; you have to convince others that you haven鈥檛 made any mistakes. For a truly groundbreaking proof, this can be a frustrating experience.
It turns out that very few mathematicians are willing to put aside their own work and dedicate the months or even years it would take to understand a proof like Mochizuki鈥檚. And as maths becomes increasingly fractured into subfields within subfields, the problem is set to get worse. Some think maths is reaching a limit. Real breakthroughs can be too complicated for others to check, so many mathematicians occupy themselves with more attainable but arguably less significant problems. What鈥檚 to be done?
For some, the solution lies in employing digital help. A lot of mathematicians already work alongside computers 鈥 they can help check proofs and free up time for more creative work. But it might mean changing how maths is done. What鈥檚 more, computers may one day make genuine breakthroughs on their own. Will we be able to keep up? And what does it mean for maths if we can鈥檛?
The first major computer-assisted proof was published 40 years ago and it immediately sparked a row. It was a solution to the four-colour theorem, a puzzle dating back to the mid-19th century. The theorem states that all maps need only four colours to make sure no adjacent regions are coloured the same. You can try it as many times as you like and find it to be true (print out our puzzle to have a go). But to prove it, you need to rule out the very possibility of there being a bizarre map that bucks the trend.
In 1976, Kenneth Appel and Wolfgang Haken did just that. They showed you could narrow the problem down to 1936 sub-arrangements that might require five colours. They then used a computer to check each of these potential counterexamples, and found that all could indeed be coloured with just four colours.
Job done, or so you鈥檇 think. 鈥淢athematicians were reluctant to accept this as a proof,鈥 says Xavier Leroy for Research in Computer Science and Automation in Paris, France. What if there was an error in the code? 鈥淭hey said: 鈥榃e鈥檙e not going to recheck your thousand particular cases by hand, we don鈥檛 trust your program, and that鈥檚 not a real proof鈥.鈥
They had a point. Checking software that tests a mathematical conjecture can be harder than proving it the traditional way, and a coding mistake can make the results totally unreliable. 鈥淚t鈥檚 very difficult to check whether a given program does the proper calculation just by inspection,鈥 says Georges Gonthier . 鈥淭he computer goes over the code many times, so it can amplify even the smallest error.鈥
The trick is to use software to check software. Working with a type of program known as a proof assistant, mathematicians can verify that each step of a proof is valid. 鈥淚t鈥檚 a fairly interactive process, you type commands into the tool and then the tool will spellcheck it, if you like,鈥 says Leroy. And what if the proof assistant has a bug? It鈥檚 always possible, but these programs tend to be small and relatively easy to check by hand. 鈥淢ore importantly, this is code that is run over and over again,鈥 says Gonthier. 鈥淵ou have massive experimental data to show that it is computing properly.鈥
However, using proof assistants means embracing a different way of working. When mathematicians write out proofs, they skip a lot of the boring details. There is no point in laying out the foundations of calculus every time, for example. But such shortcuts don鈥檛 fly with computers. To work with a proof, they must account for every logical step, even apparent no-brainers such as why 2 + 2 = 4.
Software confirmed the best way to stack spheres (Image: James Day/Gallery Stock)
Translating human-written proofs into computer-speak is still an active area of research. A single proof can take years. One early breakthrough came in 2005, when Gonthier and his colleagues updated the proof of the four-colour theorem, making every part of it computer-readable. Previous versions, ever since Appel and Haken鈥檚 work in 1976, relied on an area of maths called graph theory, which draws on our spatial intuition. Thinking about regions on a map comes naturally to humans, but not computers. The whole thing needed reworking.
鈥淵ou have to turn everything into algebra, and that forces you to be more precise,鈥 says Gonthier. 鈥淭hat precision ends up paying off.鈥 Gonthier discovered that a part of the proof 鈥 widely assumed to be true because it seemed so obvious 鈥 had in fact never been proved at all because it was deemed not worth the effort. The assumption turned out to be correct, but it illustrates an added benefit of extra precision.
Tackling the four-colour theorem was just a warm-up, however. 鈥淚t has relatively few uses in the rest of mathematics,鈥 says Gonthier. 鈥淚t was a brain-teaser.鈥 So he turned to the Feit-Thompson theorem, a large and foundational proof in group theory from the 1960s. For many years the proof had been built upon and rewritten and it was eventually published in two books. By formalising it, Gonthier hoped to demonstrate the computer鈥檚 capacity to digest a meatier proof that touched many different branches of mathematics. 鈥淭he perfect test case,鈥 he says.
It was a success. 鈥淚n the process they found a couple of minor mistakes in the books,鈥 says Leroy. 鈥淭hey were easily fixable, but still things that every human mathematician missed.鈥 People took notice, says Gonthier. 鈥淚 got letters saying how wonderful it was.鈥
In both cases, the result was never in doubt. Gonthier was taking well-established maths and translating it for computers. But others have been forced to redo their work in this way just to get their proofs accepted.
In 1998, , Pennsylvania, found himself in a similar position to Mochizuki鈥檚 today. He had just published a 300-page proof of the Kepler conjecture, a 400-year-old problem that concerns the most efficient ways to stack a collection of spheres. As with the four-colour theorem, the possibilities boiled down to variations on a few thousand arrangements. Hales and his student Samuel Ferguson used a computer to check them all.
Hales submitted his result to the journal Annals of Mathematics. Five years later, reviewers for the journal announced they were 99 per cent certain that the proof was correct. 鈥Referees in mathematics generally do not want to check computer code. They don鈥檛 see that as part of their job,鈥 says Hales.
Convinced he was right, Hales started to rework his proof in 2003, so that it could be checked with a proof assistant. It essentially meant starting all over again, he says. He finally completed the project last year.
Gonthier鈥檚 and Hales鈥檚 research has shown that the approach can be applied to important mathematics. 鈥淭he big theorems in maths that we鈥檙e proving now seemed a distant dream 10 years ago,鈥 says Hales. But despite advances like the proof assistant, proving things with a computer is still a laborious process. Most mathematicians don鈥檛 bother.
That鈥檚 why some are working in the opposite direction. Rather than making proof assistants easier to use, at the Institute for Advanced Study in Princeton, New Jersey, wants to make mathematics more amenable to computers. To do this, he is redefining its very foundations.
True to type
This is deep stuff. Maths is currently defined in terms of set theory, essentially the study of collections of objects. For example, the number zero is defined as the empty set, the collection of no objects. One is defined as the set containing one empty set. From there you can build an infinity of numbers. Most mathematicians don鈥檛 worry about this on a day-to-day basis. 鈥淧eople are expected to understand each other without going down to that much detail,鈥 says Voevodsky.
Modelling and visualising airflow is a task computers handle well (Image: M. D. Sanetrik/Corbis)
Not so for computers, and that鈥檚 a problem. There are multiple ways to define certain mathematical objects in terms of sets. For us, that doesn鈥檛 matter, but if two computer proofs use different definitions for the same thing, they will be incompatible. 鈥淲e cannot compare the results, because at the core they are based on two different things,鈥 says Voevodsky. 鈥淭he existing foundations of maths don鈥檛 work very well if you want to get everything in a very precise form.鈥
Voevodsky鈥檚 alternative approach swaps sets for types 鈥 a stricter way of defining mathematical objects in which every concept has exactly one definition. Proofs built with types can also form types themselves, which isn鈥檛 the case with sets. This lets mathematicians formulate their ideas with a proof assistant directly, rather than having to translate them later. In 2013 Voevodsky and colleagues published a book explaining the principles behind the new foundations. In a reversal of the norm, they wrote the book with a proof assistant and then 鈥渦nformalised鈥 it to produce something more human-friendly.
This backwards working changes the way mathematicians think, says Gonthier. 鈥淭he book is entirely written in non-formalised prose, but if you have any kind of experience with using the computer system, you quickly realise that the prose closely reflects what is going on in the formal system.鈥
It also allows much closer collaboration between large groups of mathematicians, because they don鈥檛 have to constantly check each other鈥檚 work. 鈥淭hey鈥檝e really started to popularise the idea that proof assistants can be good for the working mathematician,鈥 says Leroy. 鈥淭hat鈥檚 a really exciting development.鈥
And it may be just the beginning. By making maths easer for computers to understand, Voevodsky鈥檚 redefinition might take us into new territory. As he sees it, mathematics is split into four quadrants (see chart). Applied maths 鈥 modelling the airflow over a wing, for example 鈥 involves high complexity but low abstraction. Pure maths, the kind of pen and paper maths that is far removed from our everyday lives, involves low complexity but high abstraction. And school-level maths is neither complex nor abstract. But what lies in that fourth quadrant?
鈥淚t is very difficult at the present to go into the high levels of complexity and abstraction, because it just doesn鈥檛 fit into our heads very well,鈥 says Voevodsky. 鈥淚t somehow requires abilities that we don鈥檛 posses.鈥 By working with computers, perhaps humans could access this fourth mathematical realm. We could prove bigger, bolder and more abstract problems than ever before, pushing our mastery of maths to ultimate heights.FIG-mg30360301.jpg
Or perhaps we鈥檒l be left behind. Last year and at the University of Liverpool, UK, published a computer-assisted proof so long that it totalled 13 gigabytes, roughly the size of Wikipedia. Each line of the proof is readable, but for anyone to go through the entire result would take several tedious lifetimes.
The pair have since optimised their code and reduced the proof to 鈥 a big improvement, but still impossible to digest. 鈥淔rom a human viewpoint, there鈥檚 not much difference,鈥 says Lisitsa. Even if you did devote your life to reading something like this, it would be like studying a photograph pixel-by-pixel, never seeing the larger picture. 鈥淵ou cannot grasp the idea behind it.鈥
Although it is on a far grander scale, the situation is similar to the original proof of the four-colour theorem, where mathematicians could not be sure an exhaustive computer search was correct. 鈥淲e still don鈥檛 know why the result holds true,鈥 says Lisitsa. 鈥淚t could be a limit of human understanding, because the objects are so huge.鈥
of Rutgers University in Newark, New Jersey, thinks there will even come a time when human mathematicians will no longer be able to contribute. 鈥淔or the next hundred years humans will still be needed as coaches to guide computers,鈥 he says. But after that? 鈥淭hey could still do it as an intellectual sport, and play each other like human chess players still do today, even though they are much inferior to machines.鈥
Zeilberger is an extreme case. He has listed his computer, nicknamed , as a co-author for decades and thinks humans should put pen and paper aside to focus on educating our machines. 鈥淭he most optimal use of a mathematician鈥檚 time is knowledge transfer,鈥 he says. 鈥淭each computers all their tricks and let computers take it from there.鈥
Spiritual discipline
But most mathematicians bristle at the idea of software that churns out proofs beyond human comprehension. 鈥淭he idea that computers are going to replace mathematicians is misplaced,鈥 says Gonthier.
Besides, computer mathematicians would risk churning out an accelerating stream of unread papers. As it stands, scientific results often fail to garner the recognition they deserve, but the problem is particularly marked for maths. In 2014 there were more than 2000 maths papers posted to the online repository each month, more than in any other discipline, and the rate is increasing. 鈥淚f you have too many new results that keep appearing, many just go unnoticed,鈥 says Leroy. Maybe we could at least create software to read everything and help humans keep up with the important bits, he says.
Gonthier feels this is missing the point: 鈥淢athematics is not as much about finding proofs as it is about finding concepts.鈥 The nature of maths itself is under scrutiny. If humans do not understand a proof, then it doesn鈥檛 count as maths, says Voevodsky. 鈥淭he future of mathematics is more a spiritual discipline than an applied art. One of the important functions of mathematics is the development of the human mind.鈥
鈥淭o make mathematical proof easier for computers, we must redefine maths itself鈥
All of this may be too late for Shinichi Mochizuki, however. His work is so advanced, so far removed from mainstream maths, that having a computer check it would be far more difficult than coming up with the original proof. 鈥淚 don鈥檛 even know if it would be possible to formalise what he鈥檚 done,鈥 says Hales. For now, humans remain the ultimate judge 鈥 even if we don鈥檛 always trust ourselves.
Read more: 鈥Eureka by machine: How computers will be the mother of invention鈥
Leader: 鈥Smart machines may discover things we can鈥檛, but we still matter鈥
This article appeared in print under the headline 鈥淧roof of concept鈥
