[FOM] Talk on Formal Verification

[Josef Urban]

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.

Josef
On Feb 13, 2016 6:26 PM, "Harvey Friedman" <hmflogic at gmail.com> wrote:

> Josef Urban responded to my
> http://www.cs.nyu.edu/pipermail/fom/2016-February/019498.html
> concerning the Mizar proof of the Zermelo well ordering theorem:
>
> On Thu, Feb 11, 2016 at 4:14 PM, Josef Urban <josef.urban at gmail.com>
> wrote:
> ...
> > The particular Mizar proof by Grzegorz Bancerek is at
> >
> http://mizar.cs.ualberta.ca/~mptp/8.1.03_5.29.1227/html/wellord2.html#T17
> .
> > I'd be willing to bet that in 20 years, a computer program (running on
> > today's hardware) will be able to prove it in 1 day when given all the
> > previous Mizar facts and their proofs.
> >
>
> How much does this estimate depend on the program being given "all of
> the previous Mizar facts and their proofs"?
>
> I.e., let 0 <= p <= 1, and the program is given the first fraction p
> of the previous Mizar facts and their proofs. Then how are the
> estimates "20 years, 1 day" affected by p?
>
> In thinking about this kind of question, I came up with an addition to
> my posting http://www.cs.nyu.edu/pipermail/fom/2016-February/019499.html.
> I'll mention it briefly here, but want to have more to say before
> creating an additional numbered posting.
>
> We use the following complexity measure of a string x in ASCI. Use a
> standard programming language. The production complexity of x is the
> least sum n+m, where n is the length of a program, m is the number of
> steps of computation till halting, and where the output is x.
>
> Let T be a theorem of some standard sugared ZFC. The hardness of T,
> hard(T), is the least production complexity of any proof in ZFC
> (primitive notation) of T.
>
> CHALLENGE. Estimate hard(T) for fundamental theorems T of sugared ZFC.
>
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160213/11989936/attachment.html>