[FOM] Talk on Formal Verification

[Harvey Friedman]

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