Source: Scientific American, Oct 2013
Voevodsky told mathematicians that their lives are about to change. Soon enough, they’re going to find themselves doing mathematics at the computer, with the aid of computer proof assistants. Soon, they won’t consider a theorem proven until a computer has verified it. Soon, they’ll be able to collaborate freely, even with mathematicians whose skills they don’t have confidence in. And soon, they’ll understand the foundations of mathematics very differently.
he also showed that the theory of programming languages is in fact the same thing as homotopy theory, one of the most abstruse areas of mathematics. And both of them are the same thing as mathematical logic. The three fields express the same ideas in very different language.
The thing that’s so remarkable about this new foundation is that the fundamental concepts are much closer to where ordinary mathematicians do their work. In the usual foundation, Zermelo-Frankel set theory, it takes an enormous amount of work just to build up the basic concepts and theorems that mathematicians rely on every day. The result is that if you want a computer to check your proofs, you have to teach it all that theory first. Essentially, you have to give it the same education you got — except that you have to do it in a far more exacting way.
As a result, the only people so far who have used computer proof systems are computer scientists who specialize in it, and it takes them many years of effort to check a single new theorem. Georges Gonthier, for example, spent a decade checking the four-color theorem.
But this approach circumvents all that labor. Not only that, but the language the computer understands is far closer to natural mathematical language. Yes, mathematicians who want to use a proof assistant will have to learn some things – essentially, it’s learning a programming language – but once they’ve made that investment, the process of using the proof assistant becomes pretty natural. In fact, Voevodsky says, it’s a bit like playing a video game. You interact with the computer. “You tell the computer, try this, and it tries it, and it gives you back the result of its actions,” Voevodsky says. “Sometimes it’s unexpected what comes out of it. It’s fun.”
I asked him if he really thought all mathematicians were going to end up using computers to create their proofs. “I can’t see how else it will go,” he said. “I think the process will be first accepted by some small subset, then it will grow, and eventually it will become a really standard thing. The next step is when it will start to be taught at math grad schools, and then the next step is when it will be taught at the undergraduate level. That may take tens of years, I don’t know, but I don’t see what else could happen.”
He also predicts that this will lead to a blossoming of collaboration, pointing out that right now, collaboration requires an enormous trust, because it’s too much work to carefully check your collaborator’s work. With computer verification, the computer does all that for you, so you can collaborate with anyone and know that what they produce is solid. That creates the possibility of mathematicians doing large-scale collaborative projects that have been impractical until now.