[FOM] Talk on Formal Verification

[Josef Urban]

The problem is with "current computer technology". If I write a 1000-line
program that combines existing AI toolkits to do this, is it "current" or
"new"?

We do use evolutionary algorithms to improve theorem provers. Again, they
are very simple to program, i.e., to "build using current technology".

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.

Josef
On Feb 11, 2016 8:55 PM, "Harvey Friedman" <hmflogic at gmail.com> wrote:

> On Mon, Feb 8, 2016 at 9:59 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote
> > It is paradoxical that, on the one hand, many such efforts have been
> wildly successful, but on the other hand, they show no signs of any
> capability in regard to the sort of insights we have been discussing on
> this list. Geometry theorem-proving programs produce very impressive
> results, but rely on Gröbner bases; integration is now done by algorithm,
> etc. The situation is reminiscent of computer chess, where on the one hand,
> a computer program can beat the world champion, but on the other hand, no
> chess-playing program can explain why a given move is good or bad, or
> compare two positions to state whether an idea that works in one would be
> likely to work in the other. A proof found using our technology can be
> compared with a 10-move checkmate found by chess-playing software, The
> difference is that it is possible to play good chess purely by calculation,
> without having any concept of idea, strategy, plan or theme. But the world
> of chess is an 8 x 8 board, and the world of mathematics is quite a bit
> bigger than that.
> >
>
> I would be very interested in seeing a proof of a result of the following
> form.
>
> The kind of algorithms involved in chess, and more recently go, under
> machine learning, or "deep" machine learning, is first given a
> reasonably general rigorous formulation. Then one takes a reasonably
> nontrivial theorem over ZFC like Zermelo's well ordering theorem, and
> asks the algorithm to find a proof of it. The algorithm is given ZFC
> and the statement of Zermelo's well ordering theorem. It is also given
> samples of various proofs of other theorems from ZFC.
>
> THEOREM?. The algorithm will not come up with a proof of Zermelo's
> well ordering theorem, given this data, in < exp(1M) years with
> current computer technology.
>
> Obviously, a direct attack on this is not very promising right now, so
> the real question is this. How do we frame some good attainable toy
> results of this kind?
>
> In any case, the model of machine learning, deep or otherwise, to be
> used, cannot be so general as to include evolutionary biological
> systems. For these are in fact able to come up with the proof of
> Zermelo's well ordering theorem with this data, and even less, in
> reasonable time frames. Namely, us.
>
> 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/20160211/ddd2ef90/attachment-0001.html>