(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â
