[FOM] Talk on Formal Verification

[Harvey Friedman]

Josef Urban responds to my
http://www.cs.nyu.edu/pipermail/fom/2016-February/019506.html

On Sat, Feb 13, 2016 at 3:12 PM, Josef Urban <josef.urban at gmail.com> wrote:
> This was just a wild guess based on (i) what we are able to do today on the
> Mizar corpus, (ii) how quickly the methods have been developing and how much
> performance boost they have brought, and (iii) some idea of what might be
> tried quite soon to further improve state of the art. I don't have
> Nate-Silver-style advanced statistical (or other) reasoning behind the bet.
>
> I can imagine systems (a la Lenat's AM, complemented by today's AI/ATP
> methods) that will develop the theorem and its proof fully automatically
> based on just the axioms. But one wild bet seems enough :-).
>
> I also have no idea about the Kolmogorov-style complexity of today's AI
> programs. Computing such metrics for real-life programs seems infeasible so
> far.
>
> Btw., the Mizar proof I mentioned is not based on ZFC but on the
> Tarski-Grothendieck axioms. It probably does not matter much for this
> debate.
>

My questions about Zermelo's well ordering theorem was inspired by the
postings of Larry Paulson

http://www.cs.nyu.edu/pipermail/fom/2016-February/019471.html
http://www.cs.nyu.edu/pipermail/fom/2016-February/019477.html
http://www.cs.nyu.edu/pipermail/fom/2016-February/019493.html

where I think he is taking quite a different point of view than is Josef Urban.

I read Larry Paulson as drawing a real distinction between brute force
and pattern matching and other AI methods, and "creative insight". It
is not clear to me how to make this more precise, and so I got
interested in exploring the boundaries by way of examples. Hence my
questions.

Now let me make this line of questioning so extreme that perhaps Josef
Urban may take a line more in common with Larry Paulson.

Suppose you have a decent general math library for all of undergrad
and grad math curriculum at major math departments worldwide.

When are we going to have a machine which, given all that data, and
the statement of FLT, produces a proof of FLT?

By the way, it may be relevant to add that, even in the case of chess,
the jury is still open on whether

*world champion level human plus computers*

crushes

*computers alone*

under correspondence time limits.

Coming to production complexity (variant of Kolmogorov complexity more
interesting for this discussion), I was suggesting the program of
getting better and better upper bounds on the production complexity
needed to prove various theorems in mathematics. This is of course
intimately connected with the normal research of trying to more
readily construct proofs of theorems - i.e., normal theorem proving
research.

My point is that maybe trying to extract a theoretical subject here
may motivate some research into proof structure which would not
normally be pursued by the theorem proving community because it isn't
directly relevant to their main purpose of facilitating the
construction of proofs.

Of course, there are other related theoretical investigations which do
not involve production complexity. Namely, concerning robust measures
of proof size, and some actual focusing on proof sizes for actual
theorems - normally clever upper bounds, and also some lower bounds
maybe for very toy examples. I will try to put together more
substantive ideas for theoretical investigations into actual proofs of
actual important theorems (toy and otherwise) in a numbered posting.

I agree with your last paragraph, that it doesn't make any difference
for this discussion whether we are using ZFC or some stronger class
theory. In fact, I believe that the move to class theory is not a good
one, and that ZFC is better, when sugared properly. E.g., with the
introduction of relations and functions hierarchically by explicit
definition, which should eliminate at least the most obvious needs for
classes.

Also, I continue to be suspicious of the popular to move toward
complicated typing setups, particularly after discussions with John
Harrison at a recent meeting on Semantic Representation of
Mathematical Knowledge.

Harvey Friedman