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 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 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). -----------------------------------------------------------------------------