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