Computers proving mathematical theorems: How artificial intelligence could change math.

How Computers Could Change Pure Mathematics

How Computers Could Change Pure Mathematics

The state of the universe.
March 23 2015 8:18 AM

Mathematicians of the Future?

Why it matters that computers could someday prove their own theorems.

World Chess champion Garry Kasparov IBM's Deep Blue computer.
Chess enthusiasts watch World Chess champion Garry Kasparov at the start of his sixth and final match, May 1997, against IBM's Deep Blue computer in New York.

Photo credit should read Stan Honda/AFP/Getty Images

Herbert Simon, the Nobel-prize winning economist, was a techno-enthusiast. In 1956 he predicted that, “within 10 years, computers would beat the world chess champion, compose ‘aesthetically satisfying’ original music, and prove new mathematical theorems.” His timing was off: Chess had to wait more than 40 years before Deep Blue beat Garry Kasparov; "aesthetic satisfaction" remains in the ear of the listener; and although some people purport to have attained the third of Simon's milestones, most pure mathematicians are skeptical of the examples supporting these claims.

In recent years, however, some of the world's most distinguished pure mathematicians have been teaming up with computer scientists in what looks like a frontal attack on Simon's third goal. Tom Hales of the University of Pittsburgh, like Vladimir Voevodsky of Princeton's Institute for Advanced Study (IAS), sees proof-checking by electronic mathematicians as a necessity in an age when some proofs have grown too complex to be certified reliable by human readers. While their immediate projects treat computers as an adjunct to human imagination, Hales and Voevodsky have both made it clear that they also expect the new technology to transform the way mathematics is done. Similarly, Sir Timothy Gowers, at Cambridge University, expects collaboration with a "semi-intelligent database" to "take a great deal of the drudgery out of research."

But some mathematicians' ambitions go further. Gowers and his collaborators are seeking to design computer systems that reason synthetically, like human mathematicians, rather than relying on brute speed and storage capacity. Gowers has written that, although he "does not feel particularly happy" about the prospect, he anticipates a future of fully automated theorem-proving, with mathematicians reduced to running the machines and finding "interesting applications" for their theorems.


At this point, you may have one of three reactions. You may be alarmed that mathematicians are "summoning the demon," in the words of SpaceX and Tesla Motors CEO Elon Musk, or hastening "the end of the human race," as the physicist Steven Hawking fears; both have outlined doomsday scenarios that see artificial intelligence "superseding" the human race, as in the Terminator films. Or, on the contrary you may think this is great news, the latest "giant leap for mankind"; you may even feel the human race has outlived its welcome on Earth and is overdue for supersession. Or you may believe that Simon's milestone is impossible, that computers will never be able to replace human reason—and believe that neither the warnings of cyborg apocalypse nor the promises of cyborg utopia should be taken seriously.

a scene from the film '2001: A Space Odyssey', 1968.
Gary Lockwood, left, talks to Keir Dullea in a scene from 2001: A Space Odyssey. The computer HAL 9000, center, is able to read their lips.

Photo by Metro-Goldwyn-Mayer/Getty Images

I reserve judgment. It would be foolhardy to claim that computers will never be better at theorem-proving than human mathematicians. (Gowers guessed it would happen by 2099.) The research programs are dynamic, and I have no doubt that continued work along these lines will bring unexpected benefits, as well as unintended challenges, within the fields of computing and pure mathematics. It may well transform everyday life as well, as computers certainly have.

Perhaps such efforts will even lead to creation of expert systems that are able to prove mathematical theorems that are not only new but interesting. But the assumption that this would mean an end to human mathematics—short of putting an end to humans altogether—reflects a stunted vision of why humans do mathematics in the first place; a vision, at any rate, very different from the one I defend in my book Mathematics Without Apologies.

Mathematics is often compared to an art form. Usually not much thought goes into this comparison, but the analogy is valid insofar as mathematical research is considered a free, creative activity. This means in particular that it is not done to specifications on the orders of a higher authority. It also means, implicitly, that it is a fundamentally human activity. People everywhere in the world tune in to the Olympics to watch people run and jump, not to watch machines that can run faster and jump higher. Player pianos get the notes right, but don't perform to sell-out crowds: Why is that?

The answer, I suspect—and it shouldn't be necessary to say this—is that shared human experience still has intrinsic value. Or, to put it more directly, that value itself is measured relative to a community of human experience. The audience at a live concert or at a sporting event shares an experience with the performers or the athletes that they are not yet ready to share with robots. It's true that mathematical research is not a public spectacle and is not supported by ticket sales. But anyone who doubts that the practice belongs to a form of shared experience has probably never read an article about mathematics for a general audience, and probably shouldn't be reading this one.

HAL 9000, the onboard computer in Stanley Kubrick's 2001: A Space Odyssey, famously pulled the plugs on the human crew, having reasoned that they were in danger of jeopardizing the mission. What is the mission of human mathematics? Pierre Deligne, Voevodsky's colleague at Princeton's IAS, one of mathematics' brightest lights for nearly 50 years, suggests one answer. More than once he recalled how pleased he was as a student in Brussels to learn he could make a living "by playing, i.e. by doing research in mathematics." Playing music, playing sports, playing with our mathematical imagination. If the time ever comes when Deligne's motivation is not accepted as a legitimate reason to exercise our curiosity, then it won't matter whether or not the computers take over.