Voevodsky and Proof Assistants
Vladimir Voevodsky was awarded the Fields Medal in 2002 for his work on motivic cohomology leading to a proof of the Milnor conjecture. He’s here in Heidelberg for the HLF and I was glad to have the opportunity (see above) to talk with him and get some understanding of what he has been up to in recent years.
Voevodsky at some point radically changed the direction of his research, with one motivation being his growing concern about the increasing danger of mistakes in mathematical proofs. He had personal experience of this in his own work (see his discussion of the history of this here), and began to feel that the way mathematics research is now done, often under time pressure, all too easily leads to mistakes and flaws in proofs that no one is aware of. This can have a serious corrupting effect on mathematics, both in terms of the reliability of the results, and the entire process of how mathematicians work.
He sees the answer to this problem in the use of computers as “proof assistants”, checking the validity of the arguments of a proof. Though, to develop an effective proof assistant, he found it necessary to think deeply about the foundations of mathematics, which led to the development of what he calls “Univalent Foundations”. This has become an active field, and one part of Voevodsky’s talk here dealt with this.
His main motivation though remains not the new foundations themselves, but their use by computers to check arguments. A second part of his talk dealt briefly with the UniMath project he is working on to develop software for such a proof assistant.
One minor problem he mentioned brought back to mind some of my own history. When students work with him at Princeton, the lack of basic graduate level courses in mathematics (the Princeton department has never had many of these, feeling their incoming grad students often didn’t need them) means that students are more likely to take courses in computer science and be drawn away from mathematics in that direction. At Princeton I was a Ph.D. student in physics who was very interested in learning more mathematics, but the lack of appropriate courses discouraged this.
Voevodsky is well aware that mathematicians in general are far from sold on the idea of doing the kind of work necessary to use such a proof assistant, but he sees no other way of ensuring the reliability of mathematical proofs. There’s a lot more enthusiasm for his ideas in the computer science community, where they fit into already active research programs. Time will tell what direction this research will ultimately take, but the problem Voevodsky raises about the reliability of proofs is one of increasing importance as their depth and complexity increases with time.