(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’s 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’re 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’s not the whole story. You can’t just publish something you believe is true and move on; you have to convince others that you haven’t 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’s. 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’s 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’s 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’t?
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’d think. “Mathematicians 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? “They said: ‘We’re not going to recheck your thousand particular cases by hand, we don’t trust your program, and that’s 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. “It’s very difficult to check whether a given program does the proper calculation just by inspection,” says Georges Gonthier . “The 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. “It’s 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’s always possible, but these programs tend to be small and relatively easy to check by hand. “More importantly, this is code that is run over and over again,” says Gonthier. “You 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’t 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’s 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.
“You have to turn everything into algebra, and that forces you to be more precise,” says Gonthier. “That 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. “It has relatively few uses in the rest of mathematics,” says Gonthier. “It 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’s capacity to digest a meatier proof that touched many different branches of mathematics. “The perfect test case,” he says.
It was a success. “In the process they found a couple of minor mistakes in the books,” says Leroy. “They were easily fixable, but still things that every human mathematician missed.” People took notice, says Gonthier. “I 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’s 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’t 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’s and Hales’s research has shown that the approach can be applied to important mathematics. “The big theorems in maths that we’re 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’t bother.
That’s 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’t worry about this on a day-to-day basis. “People 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’s a problem. There are multiple ways to define certain mathematical objects in terms of sets. For us, that doesn’t matter, but if two computer proofs use different definitions for the same thing, they will be incompatible. “We cannot compare the results, because at the core they are based on two different things,” says Voevodsky. “The existing foundations of maths don’t work very well if you want to get everything in a very precise form.”
Voevodsky’s 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’t 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 “unformalised” it to produce something more human-friendly.
This backwards working changes the way mathematicians think, says Gonthier. “The 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’t have to constantly check each other’s work. “They’ve really started to popularise the idea that proof assistants can be good for the working mathematician,” says Leroy. “That’s a really exciting development.”
And it may be just the beginning. By making maths easer for computers to understand, Voevodsky’s 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?
“It is very difficult at the present to go into the high levels of complexity and abstraction, because it just doesn’t fit into our heads very well,” says Voevodsky. “It somehow requires abilities that we don’t 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’ll 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. “From a human viewpoint, there’s 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. “You 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. “We still don’t know why the result holds true,” says Lisitsa. “It 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. “For the next hundred years humans will still be needed as coaches to guide computers,” he says. But after that? “They 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. “The most optimal use of a mathematician’s time is knowledge transfer,” he says. “Teach 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. “The 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. “If 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: “Mathematics 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’t count as maths, says Voevodsky. “The 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.”
“To 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. “I don’t even know if it would be possible to formalise what he’s done,” says Hales. For now, humans remain the ultimate judge – even if we don’t always trust ourselves.
Read more: “Eureka by machine: How computers will be the mother of invention”
Leader: “Smart machines may discover things we can’t, but we still matter”
This article appeared in print under the headline “Proof of concept”
