This article was published in Scientific American’s former blog network and reflects the views of the author, not necessarily those of Scientific American
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.
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.
On supporting science journalism
If you're enjoying this article, consider supporting our award-winning journalism by subscribing. By purchasing a subscription you are helping to ensure the future of impactful stories about the discoveries and ideas shaping our world today.
“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.