Re: Vladimir Voevodsky

["Daniel R. Grayson" <danielrich...@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 8699 bytes --]

Here is the relevant part of the oldest email I have from Vladimir about 
computer proof:

-----------------------------------------------------------------------------
    Date: Tue, 10 Sep 2002 09:15:21 -0400 (EDT)
    From: Vladimir Voevodsky <vlad...@ias.edu>
    To: d...@math.uiuc.edu
    Subject: Re: Fields Medal

    ...

    Vladimir.

    PS I am thinking again about the applications of computers to pure
    math. Do you know of anyone working in this area? I mean mostly some
    kind of a computer language to describe mathematical structures, their
    properties and proofs in such a way that ultimately one may have
    mathematical knowledge archived and logically verified in a fixed
    format.
-----------------------------------------------------------------------------

And here is a brainstorm of his about a computer oracle based on "homotopy
lambda-calculus".  Notice that the concepts of h-level and univalence are
already present, at least in some prescient form.  (Vladimir recently told 
me
that he thought his concept of h-level is much more important than the
univalence axiom.)  You may also notice the early appearance of Brazil.

-----------------------------------------------------------------------------
    From: Vladimir Voevodsky <vlad...@ias.edu>
    Subject: Re: computers and math and education
    Date: Fri, 29 Sep 2006 15:51:36 -0400
    To: d...@math.uiuc.edu

    Dear Dan,

    what you write about the conference is very interesting. Before I get  
    into more detailed comments, a request -- if you learn about some  
    interesting meetings related to this stuff please let me know.

    > The main lesson for me (from all the sessions, not that one tale)  
    > is that these
    > systems are mainly usable by the creator, because the creator can  
    > more or less
    > remember the names of 200 trivial theorems.  It won't scale up  
    > unless searching
    > is improved.  I think you have mentioned to me that searching is  
    > what you are
    > thinking about.

    My whole concept of what one should aim at while developing  
    "productivity software" for pure math has been evolving lately in the  
    following direction.

    Let us start with what would be a perfect system of such sort (such a  
    system is impossible but let's ignore it for a moment).

    Ideally one wants a math oracle. A user inputs a type expression and  
    the system either returns a term of this type or says that it has no  
    terms. The type expression may be "of level 0" i.e. it can correspond  
    to a statement in which case a term is a proof and the absence of  
    terms means that the statement is not provable. It may be "of level  
    1" e.g. it might be the type of solutions of an equation. In that  
    case the system produces a solution or says that there are non. It  
    may be "of level 2" e.g. It might be the type of all solvable groups  
    of order 35555. In that case the system produces an example of such a  
    group etc.

    A realistic approximation of such an oracle may look as follows.  
    Imagine a web-based system with a lot of users (both "creators" and  
    "consumers") and a very large "database". Originally the database is  
    empty (or, rather, contains only the primitive "knowledge" a-la  
    axioms). User A (say in Princeton) inputs a type expression and  
    builds up a term of this type either in one step (just types it in)  
    or in many steps  using the standard proof-assistant capabilities of  
    the system. Both the original and all the intermediate type  
    expressions which occur in the process are filed (in the real time)  
    in the database.  Enter user B (somewhere in Brazil), who inputs  
    another type expression and begins the process of constructing a term  
    of his type. All the intermediate type expressions which show up as  
    well as their negations are filed and also compared in real time with  
    the ones already in the database. If a match occurs the user is  
    informed that this and that type has been considered before and the  
    following terms of this type are known (or it negation has been and  
    terms are known in which case one assumes that the original type has  
    no terms).  Eventually, the database is large enough such that in  
    many cases the system will work like an oracle i.e. will provide  
    information on terms of the type which user B is interested in.

    Clearly, designing such a system may take decades and it can only  
    materialize if a lot of people work on it.  I can see a number of  
    reasonably independent tasks which have to be taken care of:

    1. To choose a formalization or formalizations of mathematics which  
    will be used to translate problems into type expressions. In the case  
    of multiple formalizations there should be modules which mechanically  
    translate from one to another.

    2. To design the proof-assistant part including modules which could  
    do computations (e.g. computational algebra)

    3. To understand what the system does when a request for a term of a  
    given type is submitted to the database.

    The basic operation is of course simple comparison with something  
    previously filed. In most cases however the submitted type expression  
    will be equivalent to a one already in the database not equal. On the  
    very elementary level this can be an equivalence which can be  
    recognized by some normalization procedure, using De Bruijn indexes  
    etc. On a slightly more complex level it can be say the permutation  
    of factors such as (A or B) versus (B or A).  More about this issue  
    below.

    Clearly the  system should consider both the original type and its  
    negation in parallel. It also should "split" combined types such as  
    (A or B) and (A and B) and analyze components separately. Finally, it  
    might look for types which obviously map to the one under  
    consideration and which have known terms.

    4. Implementation side which with at least two parts --  
    "networking" (where the "database" is kept, how it is done if it is  
    not centralized but distributed etc.) and "interface" (I personally  
    like drag-and-drop's :)) "Interface" part also includes the question  
    of what kind of hints one wants from the system when a complete  
    answer is not available e.g. if a user is trying to prove that  (A or  
    B) holds and the system can come up with a counterexample (a proof of  
    the negation) to A then should probably inform the user about it.  
    Similarly, if one tries to prove (A and B) and the system knows a  
    proof of A it should also let it be known.

    5. Eventually, there should be "daemons" which would  wonder around  
    the database, extend it and clean it up - this is an AI issue. It  
    might be real fun when we get there.

    It is clear that such a system can be useful only if it is good at  
    recognizing when two type expressions are equivalent. How easy or  
    hard it is depends a lot on the choice of the underlying  
    formalization. For example, the ZF formalization is notoriously bad  
    in this respect (also, it is not a type system but a first order  
    theory so the reduction of everything to the question of finding a  
    term of a particular type is not really applicable). If one writes   
    the following two statements:

    a. for all x in N such that x<1 one has x=0
    b. for all x in Z such that x>=0 and x<1 one has x=0

    in ZF they will look so different that it is hard to imagine a  
    program which will recognize their equivalence. Normally one would do  
    it but showing first that  the types N and Zplus=(all x in Z such  
    that x>=0) are equivalent.  In ZF however they are *not* equivalent  
    since it is easy to make a statement about one which is false for  
    another. E.g. empty set is an element of N but not of Zplus.

    My homotopy lambda calculus is an attempt to create a system which is  
    very good at dealing with equivalences. In particular it is supposed  
    to have the property that given any type expression F(T) depending on  
    a term subexpression t of type T and an equivalence t->t' (a term of  
    the type Eq(T;t,t')) there is a mechanical way to create a new  
    expression F' now depending on t' and an equivalence between F(T) and  
    F'(T') (note that to get F' one can not just substitute t' for t in F  
    -- the resulting expression will most likely be syntactically  
    incorrect).
-----------------------------------------------------------------------------


[-- Attachment #1.2: Type: text/html, Size: 11158 bytes --]