Voevodsky and Proof Assistants

BLOG: Heidelberg Laureate Forum

Laureates of mathematics and computer science meet the next generation
Heidelberg Laureate Forum

Vladimir Voevodsky

Credit: © Heidelberg Laureate Forum Foundation / Flemming­ – 2016

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.

Avatar photo

Posted by

Peter Woit is currently Senior Lecturer in the Mathematics department at Columbia University. He began his career with a 1985 doctoral degree in theoretical physics from Princeton, then held postdoctoral positions in physics (Stony Brook) and mathematics (MSRI-Berkeley) before coming to Columbia in 1989. He is the author of a 2006 popular book, Not Even Wrong, and a textbook on quantum mechanics and representation theory to be published next year. Since 2004 he has been blogging about mathematics and physics-related topics at http://www.math.columbia.edu/~woit/blog

4 comments

  1. Proofs are also used to verify computer programs. A theory which allows checking of proofs or even construction of proofs would therefore not only help mathematics but also computer science.
    The article A new foundation for mathematics emphasizes the transformational power of Voevodsky’s approach:

    The innovative thing about Voevodsky’s approach is that he interprets the propositions of the formal system of type theory in the language of homotopy theory. In this interpretation, an additional feature applies, namely univalence, which Voevodsky adds to the foundations of mathematics as a new axiom. In it he relates the equality of logical-mathematical propositions to the equivalence in the sense of homotopy theory.

    The article further says about homotopy theory:

    Homotopy theory explains not only why “a equals b” but also how to get from a to b. In set theory, this information would have to be defined additionally, which makes the translation of mathematical propositions into programming language more difficult, says Felder. “The hope is that Voevodsky’s method will allow proofs to be translated into programming language more directly and verified more efficiently.“

  2. Peter Woit wrote (26. September 2016):
    > Vladimir Voevodsky [… proposed] the use of computers as “proof assistants”, checking the validity of the arguments of a proof.

    This reminds me on the proposal (part of the “Wiki Project Encyclopedic Network”, from the early 2000-ies) of using computers as “wikilink assistants”, for checking whether the appearance contents of a wikilink was already present in the text of the actual wikilink target article.

    > 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 or ensuring the reliability of mathematical proofs. […]

    Surely the internal consistency and cohesiveness of an (the?!) encyclopedia is a related, albeit perhaps more encompassing endeavor.
    (Sadly the reluctance of the corresponding community matched in scale …)

    • In order to be useful, it is not necessary that Voevodsky’s Proof assistents are used by all mathematicians. Proof assistents will automatically spread if they enhance confidence in the mathematical propositions for which they have been applied. I only see one negative side of proof assistents: They make it possible to push forward proofs, which are very complex and very long. And long proofs are less beautiful than short ones.
      Hence the need for a proof simplifier?

  3. Proof Assistents which support executable proofs (a mapping from a proof to a software code whichs checks the proof) could be cultural disruptive ( implying a fundamental change of work organisation) – not only in the area of mathematics but also in the field of computer programming and hardware specification, because proofs are already used for program and hardware specification.
    A sleek and efficient proof assistent could even support proof construction by a combination of knowledge, heuristics and combinatorics, because the proof assistent could immediately check whether the constructed proof is valid. And proof construction could be used for automatic software program derivation. In the future safety critical software could be constructed by a formal specification followed by program construction based on proof construction.
    And this would ultimately be an application of proof assistents which support efficient proof verification.

Leave a Reply


E-Mail-Benachrichtigung bei weiteren Kommentaren.
-- Auch möglich: Abo ohne Kommentar. +