On last Thursday at the Heidelberg Laureate Forum, Vladimir Voevodsky gave perhaps the most revolutionary scientific talk I’ve ever heard. I doubt if it generated much buzz among the young scientists in advance, though, because it had the inscrutable title “Univalent Foundations of Mathematics,” and the abstract contained sentences like this one: “Set-theoretic approach to foundations of mathematics work well until one starts to think about categories since categories cannot be properly considered as sets with structures due to the required invariance of categorical constructions with respect to equivalences rather than isomorphisms of categories.”

Eyes glazed over yet?

But what actually happened was this: 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.

Oh, and by the way — just in case the computer scientists in the crowd think that this has nothing to do with them — 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. (He only touched on this connection in his talk, though.)

Here’s the story Voevodsky told to support these claims. A bit over a decade ago, he was wrapping up the work for which he’d won his Fields medal, he was out of big ideas in that area of mathematics, and he was looking for a new area to work in. He asked himself, “What would be the most important thing I could do for math at this period of development and such that I could use my skills and resources to be helpful?” His first idea was to develop more connections between pure and applied mathematics. “But I wasted two years,” he said, “because I totally failed.” So he turned to idea number two: To develop software that mathematicians could use in their everyday work, to do proofs.

He started by learning about existing computer proof systems. Rapidly, he figured out that every proof system but one was inadequate for what he had in mind. And that last one — Coq — he couldn’t understand. It was based on something called Martin-Löf type theory, and he just couldn’t get his head around it.

So he did what any good but confused student would do: He took a class in it. And in the middle of the midterm, it finally clicked. He realized that all this type theory stuff could be translated to be equivalent to homotopy theory, his field of mathematics. Not only that, but it could provide a new, self-contained foundation for all of mathematics.

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.

The same week as the Heidelberg Laureate Forum was a conference in Barcelona on univalent foundations, which Voevodsky skipped in order to be with us. A special issue of a journal (perhaps Automated Reasoning — Voevodsky couldn’t quite remember) will come out of the conference, with papers written by the participants. Almost all of them will be submitted together with the formalized proof in Coq. That’s most likely the first time such a thing has ever happened.

Some of those computer verifications rely on a library of verified proofs that Voevodsky himself has created, so Voevodsky decided to submit his library to ArXiv. He imagined a one-page description of what the library is, along with all of his Coq files. It turns out, however, that ArXiv isn’t yet up to the task — while it can accept attached files, they can’t have any directory structure. Voevodsky plans on pestering the folks who run ArXiv until they make it possible.

One more way that he’s leading the revolution.

See Voevodsky’s lecture at HLF13