[FOM] Talk on Formal Verification

[Harvey Friedman]

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