FYI --
Brent
-------- Original Message --------
http://www.simonsfoundation.org/quanta/20130222-in-computers-we-trust/
In Computers We Trust?
As math grows ever more complex, will computers reign?
By: Natalie Wolchover
February 22, 2013
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.
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.”
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 comp
uter code.
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.
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
