In Computers We Trust?

As math grows ever more complex, will computers reign?

This simple computation, written with a math software tool called Maple, verifies a formula for the number of integer triangles with a given perimeter. (Illustration: Simons Science News)

Illustration by Simons Science News

This simple computation, written with math software called Maple, verifies a formula for the number of integer triangles with a given perimeter. 

Comments (8)

print

Shalosh B. Ekhad, the co-author of several papers in respected mathematics journals, has been known to prove with a single, succinct utterance theorems and identities that previously required pages of mathematical reasoning. Last year, when asked to evaluate a formula for the number of integer triangles with a given perimeter, Ekhad performed 37 calculations in less than a second and delivered the verdict: “True.”

Shalosh B. Ekhad is a computer. Or, rather, it is any of a rotating cast of computers used by the mathematician Doron Zeilberger, from the Dell in his New Jersey office to a supercomputer whose services he occasionally enlists in Austria. The name — Hebrew for “three B one” — refers to the AT&T 3B1, Ekhad’s earliest incarnation.

“The soul is the software,” said Zeilberger, who writes his own code using a popular math programming tool called Maple.

Doron Zeilberger, a mathematician at Rutgers University, believes computers are overtaking humans in their ability to discover new mathematics. (Photo: Tamar Zeilberger)

Tamar Zeilberger

Doron Zeilberger, a mathematician at Rutgers University, believes computers are overtaking humans in their ability to discover new mathematics.

A mustachioed, 62-year-old professor at Rutgers University, Zeilberger anchors one end of a spectrum of opinions about the role of computers in mathematics. He has been listing Ekhad as a co-author on papers since the late 1980s “to make a statement that computers should get credit where credit is due.” For decades, he has railed against “human-centric bigotry” by mathematicians: a preference for pencil-and-paper proofs that Zeilberger claims has stymied progress in the field. “For good reason,” he said. “People feel they will be out of business.”

Anyone who relies on calculators or spreadsheets might be surprised to learn that mathematicians have not universally embraced computers. To many in the field, programming a machine to prove a triangle identity — or to solve problems that have yet to be cracked by hand — moves the goalposts of a beloved 3,000-year-old game. Deducing new truths about the mathematical universe has almost always required intuition, creativity and strokes of genius, not plugging-and-chugging. In fact, the need to avoid nasty calculations (for lack of a computer) has often driven discovery, leading mathematicians to find elegant symbolic techniques like calculus. To some, the process of unearthing the unexpected, winding paths of proofs, and discovering new mathematical objects along the way, is not a means to an end that a computer can replace, but the end itself.

In other words, proofs, where computers are playing an increasingly prominent role, are not always the end goal of mathematics. “Many mathematicians think they are building theories with the ultimate goal of understanding the mathematical universe,” said Minhyong Kim, a professor of mathematics at Oxford University and Pohang University of Science and Technology in South Korea. Mathematicians try to come up with conceptual frameworks that define new objects and state new conjectures as well as proving old ones. Even when a new theory yields an important proof, many mathematicians “feel it’s actually the theory that is more intriguing than the proof itself,” Kim said.

Computers are now used extensively to discover new conjectures by finding patterns in data or equations, but they cannot conceptualize them within a larger theory, the way humans do. Computers also tend to bypass the theory-building process when proving theorems, said Constantin Teleman, a professor at the University of California at Berkeley who does not use computers in his work. In his opinion, that’s the problem. “Pure mathematics is not just about knowing the answer; it’s about understanding,” Teleman said. “If all you have come up with is ‘the computer checked a million cases,’ then that’s a failure of understanding.”

Zeilberger disagrees. If humans can understand a proof, he says, it must be a trivial one. In the never-ending pursuit of mathematical progress, Zeilberger thinks humanity is losing its edge. Intuitive leaps and an ability to think abstractly gave us an early lead, he argues, but ultimately, the unswerving logic of 1s and 0s — guided by human programmers — will far outstrip our conceptual understanding, just as it did in chess. (Computers now consistently beat grandmasters.)

“Most of the things done by humans will be done easily by computers in 20 or 30 years,” Zeilberger said. “It’s already true in some parts of mathematics; a lot of papers published today done by humans are already obsolete and can be done using algorithms. Some of the problems we do today are completely uninteresting but are done because it’s something that humans can do.”

Zeilberger and other pioneers of computational mathematics sense that their views have gone from radical to relatively common in the past five years. Traditional mathematicians are retiring, and a tech-savvy generation is taking the helm. Meanwhile, computers have grown millions of times more powerful than when they first appeared on the math scene in the 1970s, and countless new and smarter algorithms, as well as easier-to-use software, have emerged. Perhaps most significantly, experts say, contemporary mathematics is becoming increasingly complex. At the frontiers of some research areas, purely human proofs are an endangered species.

“The time when someone can do real, publishable mathematics completely without the aid of a computer is coming to a close,” said David Bailey, a mathematician and computer scientist at Lawrence Berkeley National Laboratory and the author of several books on computational mathematics. “Or if you do, you’re going to be increasingly restricted into some very specialized realms.”

Constantin Teleman, a professor at the University of California at Berkeley, thinks proofs that rely heavily on computation tend not to deepen our understanding of the mathematical universe. (Photo: George Bergman)

George Bergman

Constantin Teleman, a professor at the University of California at Berkeley, thinks proofs that rely heavily on computation tend not to deepen our understanding of the mathematical universe.

Teleman studies algebraic geometry and topology — areas in which most researchers probably now use computers, as with other subfields involving algebraic operations. He focuses on problems that can still be solved without one. “Am I doing the kind of math I’m doing because I can’t use a computer, or am I doing what I’m doing because it’s the best thing to do?” he said. “It’s a good question.” Several times in his 20-year career, Teleman has wished he knew how to program so he could calculate the solution to a problem. Each time, he decided to spend the three months he estimated that it would take to learn to program tackling the calculation by hand instead. Sometimes, Teleman said, he will “stay away from such questions or assign them to a student who can program.”

If doing math without a computer nowadays “is like running a marathon with no shoes,” as Sara Billey of the University of Washington put it, the mathematics community has splintered into two packs of runners.

The use of computers is both widespread and underacknowledged. According to Bailey, researchers often de-emphasize the computational aspects of their work in papers submitted for publication, possibly to avoid encountering friction. And although computers have been yielding landmark results since 1976, undergraduate and graduate math students are still not required to learn computer programming as part of their core education. (Math faculties tend to be conservative when it comes to curriculum changes, researchers explained, and budget constraints can prevent the addition of new courses.) Instead, students often pick up programming skills on their own, which can sometimes result in byzantine and difficult-to-check code.

But what’s even more troubling, researchers say, is the absence of clear rules governing the use of computers in mathematics. “More and more mathematicians are learning to program; however, the standards of how you check a program and establish that it’s doing the right thing — well, there are no standards,” said Jeremy Avigad, a philosopher and mathematician at Carnegie Mellon University.

In December, Avigad, Bailey, Billey and dozens of other researchers met at the Institute for Computational and Experimental Research in Mathematics, a new research institute at Brown University, to discuss standards for reliability and reproducibility. From myriad issues, one underlying question emerged: In the search for ultimate truth, how much can we trust computers?

Computerized Math

Mathematicians use computers in a number of ways. One is proof-by-exhaustion: setting up a proof so that a statement is true as long as it holds for a huge but finite number of cases and then programming a computer to check all the cases.

More often, computers help discover interesting patterns in data, about which mathematicians then formulate conjectures, or guesses. “I’ve gotten a tremendous amount out of looking for patterns in the data and then proving them,” Billey said.

Using computation to verify that a conjecture holds in every checkable case, and ultimately to become convinced of it, “gives you the psychological strength you need to actually do the work necessary to prove it,” said Jordan Ellenberg, a professor at the University of Wisconsin who uses computers for conjecture discovery and then builds proofs by hand.

Increasingly, computers are helping not only to find conjectures but also to rigorously prove them. Theorem-proving packages such as Microsoft’s Z3 can verify certain types of statements or quickly find a counterexample that shows a statement is false. And algorithms like the Wilf-Zeilberger method (invented by Zeilberger and Herbert Wilf in 1990) can perform symbolic computations, manipulating variables instead of numbers to produce exact results free of rounding errors.

With current computing power, such algorithms can solve problems whose answers are algebraic expressions tens of thousands of terms long. “The computer can then simplify this to five or 10 terms,” Bailey said. “Not only could a human not have done that, they certainly could not have done it without errors.”

But computer code is also fallible — because humans write it. Coding errors (and the difficulty in detecting them) have occasionally forced mathematicians to backpedal.

In the 1990s, Teleman recalled, theoretical physicists predicted “a beautiful answer” to a question about higher-dimensional surfaces that were relevant to string theory. When mathematicians wrote a computer program to check the conjecture, they found it false. “But the programmers had made a mistake, and the physicists were actually right,” Teleman said. “That’s the biggest danger of using a computer proof: What if there’s a bug?”

This question preoccupies Jon Hanke. A number theorist and proficient programmer, Hanke thinks mathematicians have grown too trusting of tools that not long ago they frowned upon. He argues that software should never be trusted; it should be checked. But most of the software currently used by mathematicians can’t be verified. The best-selling commercial math programming tools — Mathematica, Maple and Magma (each costing about $1,000 per professional license) — are closed source, and bugs have been found in all of them.

“When Magma tells me the answer is 3.765, how do I know that’s really the answer?” Hanke asked. “I don’t. I have to trust Magma.” If mathematicians want to maintain the longstanding tradition that it be possible to check every detail of a proof, Hanke says, they can’t use closed-source software.

There is a free, open-source alternative named Sage, but it is less powerful for most applications. Sage could catch up if more mathematicians spent time developing it, Wikipedia-style, Hanke says, but there is little academic incentive to do so. “I wrote a whole bunch of open-source quadratic form software in C++ and Sage and used it to prove a theorem,” Hanke said. In a pre-tenure review of his achievements, “all that open-source work received no credit.” After being denied the opportunity for tenure at the University of Georgia in 2011, Hanke left academia to work in finance.

Although many mathematicians see an urgent need for new standards, there is one problem that standards can’t address. Double-checking another mathematician’s code is time-consuming, and people might not do it. “It’s like finding a bug in the code that runs your iPad,” Teleman said. “Who’s going to find that? How many iPad users are hacking in and looking at the details?”

Some mathematicians see only one way forward: using computers to prove theorems step by step, with cold, hard, unadulterated logic.

Proving the Proof

In 1998, Thomas Hales astounded the world when he used a computer to solve a 400-year-old problem called the Kepler conjecture. The conjecture states that the densest way to pack spheres is the usual way oranges are stacked in a crate — an arrangement called face-centered cubic packing. Every street vendor knows it, but no mathematician could prove it. Hales solved the puzzle by treating spheres as the vertices of networks (“graphs,” in math-speak) and connecting neighboring vertices with lines (or “edges”). He reduced the infinite possibilities to a list of the few thousand densest graphs, setting up a proof-by-exhaustion. “We then used a method called linear programming to show that none of the possibilities are a counterexample,” said Hales, now a mathematician at the University of Pittsburgh. In other words, none of the graphs was denser than the one corresponding to oranges in a crate. The proof consisted of about 300 written pages and an estimated 50,000 lines of computer code.

Thomas Hales, pictured in 1998, used a computer to prove a famous conjecture about the densest way to stack spheres. (Photo: Michigan Photography)

Michigan Photography

Thomas Hales, pictured in 1998, used a computer to prove a famous conjecture about the densest way to stack spheres.

Hales submitted his proof to the Annals of Mathematics, the field’s most prestigious journal, only to have the referees report four years later that they had not been able to verify the correctness of his computer code. In 2005, the Annals published an abridged version of Hales’ proof, based on their confidence about the written part.

According to Peter Sarnak, a mathematician at the Institute for Advanced Study who until January was an editor of the Annals, the issues broached by Hales’ proof have arisen repeatedly in the past 10 years. Knowing that important computer-assisted proofs would only become more common in the future, the editorial board has decided to be receptive of such proofs. “However, in cases where the code is very difficult to check by an ordinary single referee, we will make no claim about the code being correct,” Sarnak said by email. “Our hope in such a case is that the result being proved is sufficiently significant that others might write a similar but independent computer code verifying the assertions.”

Hales’ response to the refereeing dilemma could change the future of mathematics, according to his colleagues. “Tom is a remarkable person. He knows no fear,” Avigad said. “Given that people had raised concern about his proof, he said, ‘OK, the next project is to come up with a formally verified version.’ With no background in the area, he started talking to computer scientists and learning how to do that. Now that project is within a few months of completion.”

To show that his proof was unimpeachable, Hales believed he had to reconstruct it with the most basic building blocks in mathematics: logic itself, and the mathematical axioms. These self-evident truths — such as “x=x” — serve as the rule book of mathematics, similar to the way grammar governs the English language. Hales set out to use a technique called formal proof verification in which a computer program uses logic and the axioms to assess each baby step of a proof. The process can be slow and painstaking, but the reward is virtual certainty. The computer “doesn’t let you get away with anything,” said Avigad, who formally verified the prime number theorem in 2004. “It keeps track of what you’ve done. It reminds you there’s this other case you have to worry about.”

By subjecting his Kepler proof to this ultimate test, Hales hopes to remove all doubt about its veracity. “It’s looking very promising at this point,” he said. But that isn’t his only mission. He is also carrying the flag for formal proof technology. With the proliferation of computer-assisted proofs that are all but impossible to check by hand, Hales thinks computers must become the judge. “I think formal proofs are absolutely essential for the future development of mathematics,” he said.

Alternative Logic

Three years ago, Vladimir Voevodsky, one of the organizers of a new program on the foundations of mathematics at the Institute for Advanced Study in Princeton, N.J., discovered that a formal logic system that was developed by computer scientists, called “type theory,” could be used to re-create the entire mathematical universe from scratch. Type theory is consistent with the mathematical axioms, but couched in the language of computers. Voevodsky believes this alternative way to formalize mathematics, which he has renamed the univalent foundations of mathematics, will streamline the process of formal theorem proving.

Voevodsky and his team are adapting a program named Coq, which was designed to formally verify computer algorithms, for use in abstract mathematics. The user suggests which tactic, or logically airtight operation, the computer should employ to check whether a step in the proof is valid. If the tactic confirms the step, then the user suggests another tactic for assessing the next step. “So the proof is a sequence of names of tactics,” Voevodsky said. As the technology improves and the tactics become smarter, similar programs may someday perform higher-order reasoning on par with or beyond that of humans.

Some researchers say this is the only solution to math’s growing complexity problem.

“Verifying a paper is becoming just as hard as writing a paper,” Voevodsky said. “For writing, you get some reward — a promotion, perhaps — but to verify someone else’s paper, no one gets a reward. So the dream here is that the paper will come to a journal together with a file in this formal language, and referees simply verify the statement of the theorem and verify that it is interesting.”

Formal theorem proving is still relatively rare in mathematics, but that will change as programs like Voevodsky’s adaptation of Coq improve, some researchers say. Hales envisions a future in which computers are so adept at higher-order reasoning that they will be able to prove huge chunks of a theorem at a time with little — or no — human guidance.

“Maybe he’s right; maybe he’s not,” Ellenberg said of Hales’ prediction. “Certainly he’s the most thoughtful and knowledgeable person making that case.” Ellenberg, like many of his colleagues, sees a more significant role for humans in the future of his field: “We are very good at figuring out things that computers can’t do. If we were to imagine a future in which all the theorems we currently know about could be proven on a computer, we would just figure out other things that a computer can’t solve, and that would become ‘mathematics.’ ”

Teleman doesn’t know what the future holds, but he knows what kind of math he likes best. Solving a problem the human way, with its elegance, abstraction and element of surprise, is more satisfying to him. “There’s an element of a notion of failure, I think, when you resort to a computer proof,” he said. “It’s saying: ‘We can’t really do it, so we have to just let the machine run.’ ”

Even the most ardent computer fan in mathematics acknowledges a certain tragedy in surrendering to the superior logic of Shalosh B. Ekhad and accepting a supporting role in the pursuit of mathematical truth. After all, it’s only human. “I also get satisfaction from understanding everything in a proof from beginning to end,” Zeilberger said. “But on the other hand, that’s life. Life is complicated.”

Note: This article was updated on March 1, 2013, to provide additional background information about the debate over the role of computers in pure mathematics.

This article was reprinted on Wired.com.

Add a Comment

View Comments (8)

Comments for this entry

  • On some famous uses of computer proofs: Kenneth Appel and Wolfgang Haken proved the Four Colours Theorem in 1976 by checking automatically a large number of cases; more recently, the Feit-Thompson Theorem was checked formally in Coq.

  • Like in every other human endeavor assisted by technology, computers will ASSIST mathematicians, never replace them completely. Any mathematician afraid of being eliminated by a computer is a mathematician that needs to learn how to use modern technology. As this article pointed out, the more powerful computers become, the more humans will be needed to direct, interpret, and verify them. Have computers replaced architects? Have they replaced geneticists? Have they replaced any type of scientist? Of course not. They never will.

    I learned how to program a computer before I even first took algebra. Not surprisingly, traditional academic math always felt boring, pointless, and archaic to me. I quickly lost interest in academic math – but I eventually became a professional computer programmer – and have been one for over 20 years. When I think of mathematical or statistical problems, I naturally think of how I would approach them with computer programming.

    Computer programming is just an extension of the pencil, the number line, the abacus, the slide rule, the calculator, the multiplication tables learned in elementary school, and all the mathematical tools that have evolved over human history. Computers don’t “give you the answer” like this article seemed to portray at times. Computers only do EXACTLY WHAT YOU TELL THEM. They are no different than simpler mathematical tools. They only operate more quickly.

    If you’re a mathematician, learn to program a computer! It is one of the most fun things you will ever learn! I highly recommend it. If you can’t find anyone else to teach you, then I will teach you for free. That’s how much I believe in it. Enjoy!

  • “a formal logic system that was developed by computer scientists, called “type theory”

    Sorry. Intuitionistic Type Theory was introduced by a mathematician, Per Martin-Löf, building on the works of logicians like Curry, Howard, Tait and some others who were aware of the link between formal proofs and computer programs. Type Theory can be seen as a programing langage and a foundational theory for constructive mathematics (and Per Martin-Löf was aware of that fact some thirty years ago).

  • Perhaps computer generated proofs are really verifications – this approach of verifying a set of cases goes back to Euler who did it for relatively small finite sets by hand – it often requires a lot of insight to reduce the proof in question to a calculable set of cases to be verified. This all seems to be related to the famous P vs NP question.

  • Phil: Type theory does have an interesting history characterized by interplay between mathematics and computer science. As I understand it, the homotopy interpretation of type theory, the kind that Voevodsky and his colleagues are adapting for use in formal proof construction and verification, was developed and used by computer scientists based on an interpretation of Martin-Löf’s intuitionist type theory. Voevodsky mentioned to me that the proof assistant program Coq, in the form used to verify computer programs, actually verifies some incorrect mathematical statements. So, adaptation is not trivial. -Natalie Wolchover

  • Natalie, the theory of types is the invention of Bertrand Russell http://www.cfh.ufsc.br/~dkrause/pg/cursos/selecaoartigos/Russell(1905).pdf for an early formulation, and in its simplest form is present implicitly in Frege (1879); Frege was a trained mathematician but apart from his dissertation and habilitation published no work that was recognized as ‘mathematics’, all of it was either explicitly philosophy or his epoch making revision of the traditional core of philosophy, formal logic. He would be forgotten if it were not for Russell, Carnap and Wittgenstein, none of them any more than a mathematical amateur. Though the mathematicians accepted the new logic in the end, the theory of types never gained currency among them, though it continued to be developed by some logicians who were by profession either philosophers or mathematicians. From a contemporary point of view this subterranean tradition culminated in the spectacular system of Martin-Lof which though of course the work of a mathematician by training would hardly have been recognized as such by any mainstream mathematician. It is an expression of philosophical radicalism in the ‘foundations of mathematics’. Computer science had exactly nothing to do with any of this, and conventional mathematicians, who follow the herd as much as other people, ignored all of it and would have mocked it all if any of them had noticed it. It is only in the late 60’s and especially the 70’s that computer people began to take an interest in type theory — the most important figure perhaps being the great Robin Milner — and it was only 20 years later that they caught up with Martin-Lof — and only after he pointed out the evident connection in a famous paper http://intuitionistic.files.wordpress.com/2010/07/martin-lof-computer.pdf (one suspects he doesn’t know how to use a computer even now…) It can easily be shown that the importance of the type concept for the relevant branch of computer science is due to its possessing the generality characteristic of logic and philosophy – though brilliant applications of various mathematical methods made the matter tractable. It is surely only a slight exaggeration to say that the time of Hilbert and Ackermann no mathematician deemed important by conventional mathematicians has even possessed the idea of a type in the logical – that is, Russell’s, sense – until Voevodsky. One might be brazen enough to say that ‘mathematics’ and ‘computer science’, as cultures, deserve no credit at all for any type theoretic developments, but only discredit. People like Curry and Howard were outliers even among ‘mathematical logicians’ who had more and more allied themselves with untyped set theory in the period in question. We have all along to do with particular individuals who were generally unconventional and motivated by transparently philosophical considerations –starting from some elements of a straightforwardly philosophical character, introduced by philosophers (and abandoned by them too) — but who are by degrees being proved right. What is holding back the astounding connections that have by now been made and the power of type-theoretical ideas, is the barbaric conservatism of the computing industry. Note that when mathematicians employ programming languages it is almost invariably extremely debased untyped forms, survivals of the 50s and 60s that still prevail in ‘industry’. It really is true that no ‘proof’ employing these can possibly count as legitimate; it is to the credit of Hales that on reflection he recognized the need for a superior approach.

  • Hello Michael,
    You write
    ‘”…if it were not for Russell, Carnap and Wittgenstein, none of them any more than a mathematical amateur…”
    Does the author of “Principia Mathematica” (Russell) really deserve such a dismissal?

Leave a Comment

Your email address will not be published. Your name will appear near your comment. Required *

Quanta Magazine moderates all comments with the goal of facilitating an informed, substantive, civil conversation about the research developments we cover. Comments that are abusive, profane, self-promotional, misleading, incoherent or off-topic will be rejected. We can only accept comments that are written in English.