About the SA Blog Network

Guest Blog

Guest Blog

Commentary invited by editors of Scientific American
Guest Blog HomeAboutContact

The Future Role of Computers in Mathematics

The views expressed are those of the author and are not necessarily those of Scientific American.

Email   PrintPrint

At the end of the forum yesterday afternoon, the mathematics laureates took questions from the audience. One of the questions was about the role of computers in checking and generating proofs. The response of the mathematicians was mostly less than enthusiastic.

From left: Sir Michael Atiyah, Gerd Faltings, Stephen Smale, Endre Szemerédi, Srinivasa Varadhan, Cédric Villani, Avi Wigderson, Efim Zelmanov. Picture: HLFF @Berhnard Kreutzer

From left: Sir Michael Atiyah, Gerd Faltings, Stephen Smale, Endre Szemerédi, Srinivasa Varadhan, Cédric Villani, Avi Wigderson, Efim Zelmanov. Picture: HLFF @Berhnard Kreutzer

Efim Zelmanov spoke up first, saying, “A proof is what is considered to be a proof by all mathematicians, so I’m pessimistic about machine-generated proofs.” He mentioned the four-color theorem, which was the first major proof to be solved using a computer, in 1976. One hundred twenty-four years after it was first proposed, Kenneth Appel and Wolfgang Haken cleverly reduced the problem to checking the properties of 1,936 maps by computer. The result was hundreds of pages of hand analysis combined with thousands of lines of computer code. Many mathematicians hated this, not accepting the proof because it was impossible to check by hand. Michael Atiyah chimed in with a similar perspective: “We aim to get understanding in mathematics,” he said. “If we have to rely on an unintelligible computer proof, it’s not satisfactory.”

But Cédric Villani had a different perspective: “If the computer just gives an answer yes or no, it’s not satisfactory,” he said. “But the computer proof may be just part of the game.” He also pointed out that proof generation and proof checking are quite different. Georges Gonthier, for example, used computers to formally verify the proof of the four-color theorem, removing lingering doubts about the correctness of the proof. The process of formally verifying a proof using a computer, he pointed out, may lead to a deeper understanding of the mathematics, helping you to find errors or simplify the argument.

“I think it’s a romantic notion that a proof will always be simple or easy to understand,” Avi Wigderson said. “As much as we don’t like it, more and more evidence will be provided by computer systems.”

I wish that Vladimir Voevodsky had been there; apparently he planned on it, but he is ill. He has spearheaded a remarkable project that has united the fields of homotopy theory, mathematical logic, and the theory of programming languages — and in the process, it’s made computer-verified proofs usable for the working mathematician (at least in some fields), not just specialists like Gonthier. His talk tomorrow, titled “Univalent Foundations,” will describe this, if he makes it in time. The essential idea is that he and a huge team of collaborators have created new foundations that take the basic notions of homotopy theory as their axioms. This means that instead of having to prove, and formally verify, a vast edifice of earlier results in order to prove the simplest theorem in homotopy theory, a homotopy theorist can start verifying the things he or she is interested in right away, using language that’s very close to ordinary, natural mathematical language. Voevodsky’s team has already verified many of the fundamental proofs in homotopy theory.

And the fascinating thing about this is that the mathematicians involved have described a very different way of using a computer than the laureates here were discussing. For them, the computer has become a partner, a collaborator. They verify their proofs (at least some of the time) as they develop them, and the process of doing so helps them to refine their ideas. This is a very different role for computers in proof-making, and I suspect that the young mathematicians here will come to see computers as essential partners that they can’t imagine doing mathematics without.



This blog post originates from the official blog of the 1st Heidelberg Laureate Forum (HLF) which takes place September 22 – 27, 2013 in Heidelberg, Germany. 40 Abel, Fields, and Turing Laureates will gather to meet a select group of 200 young researchers. Julie Rehmeyer is a member of the HLF blog team. Please find all her postings on the HLF blog.

Julie Rehmeyer About the Author: Julie Rehmeyer is a freelance math and science writer who writes the Math Trek column at Science News. She also writes frequently for Discover Magazine and Wired. She studied algebraic topology at the Massachusetts Institute of Technology. Follow on Twitter @julierehmeyer.

The views expressed are those of the author and are not necessarily those of Scientific American.

Comments 2 Comments

Add Comment
  1. 1. jh443 5:57 pm 09/26/2013

    I remember the 1980′s versions of visions into the future – and many of the predictions are no closer to being true today than they were then. Just as visions of flying cars was common in 1939, visions of virtual reality and artificial intelligence would appear almost monthly in computer magazines.

    Computers have made magnitudes of magnitudes of advancements since 1980 (1Mhz single core single thread processor, 360Kb floppy drive, 10MB hard drives – if at all, 4-8kb RAM). So where are all these promises? Back then, the scapegoat was the claim that systems weren’t powerful enough. If they’re not yet powerful enough… when??

    About the only ever-present “vision of the future” that has materialized is picture phones. IMHO… big whoop-dee-doo.

    My point is simply this: It’s a waste of time to predict the future. The best we can do is set a goal and work toward it.

    Link to this
  2. 2. clocky clock 11:54 pm 01/17/2014

    Computers are very important because there is only so much the human brain can do. In our busy world, it can make our daily routine easier..computers can keep our calendars, keep us in touch with friends and family, and brings jobs into the home. so COmputer are very useful in our life it plays a special role in us, special to all mathematicians that really uses computers.

    Link to this

Add a Comment
You must sign in or register as a member to submit a comment.

More from Scientific American

Email this Article