[FOM] Talk on Formal Verification

[Josef Urban]

On Sun, Feb 14, 2016 at 4:23 AM, Harvey Friedman <hmflogic at gmail.com> wrote:
> 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.

Yes, I am more optimistic (and I don't think Larry is a total
pessimist - he has just been in this field for much longer). The
reason why we are capable to prove lemmas over large libraries is
exactly our capability to learn some high-level intuition from them
and combine such high-level guessing with brute-force methods. I don't
see a reason why we should not eventually be able to extract all sorts
of guiding patterns from current formal (and eventually also informal)
math corpora, and use them to improve the brute-force algorithms. This
is quite a new approach to theorem proving, and we do not know yet
what are its limits.


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

I also don't see a good way how to "prove" this sort of beliefs, so I
express it as a bet.

I'd say that the distinction between brute-force and "insight" is
meaningful, but it will get more and more blurred. The "intuition"
part will get better and better, pruning the brute-force parts more
and more.

>
> 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?

Indeed, this is taking it to the extreme. I do have some private
opinions, but I'd leave this sort of public predictions to the
Singularity crowd :-)
(https://en.wikipedia.org/wiki/The_Singularity_Is_Near).

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

OK. There have certainly been many advances in automated theorem
proving thanks to people focusing on particular mathematical/logical
phenomena.

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

I don't think there is a popular move to foundational types. I'd
rather say that non-foundational soft-typing approaches as done e.g.
in Mizar have been discovered as "typeclasses" also in Isabelle and
Coq, and were even essential to Gonthier's work.

But this is a never-ending debate, I'll leave it to Freek Wiedijk and
others ;-).

Josef

>
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom