[FOM] Talk on Formal Verification

[Lawrence Paulson]

On 11 Feb 2016, at 06:23, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> 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.

It’s worth noting how these technologies work. A good chess playing program is capable of very powerful search, but in addition, has an enormous “opening book” to guide it at the start of the game, and moreover has access to an immense database of grandmaster games going back many decades. So for millions of positions likely to occur in real games, the machine knows the move played by a human grandmaster as well as the outcome of that game. This is very good for playing chess, but not at all relevant to proving new results in mathematics. (I can’t comment about Go.)

At the moment, machine learning can solve problems such as the following: consider a class C of hard problems (large polynomials to factor, for example). We have two algorithms at our disposal, F and G. We know that F outperforms G on some problems while G outperforms F on others. And it is simply too expensive to try both. It frequently happens that machine learning can be used to decide between F and G more effectively than human-written code. It’s a valuable technology, but it’s not intelligence.

The mutilated chessboard illustrates two distinct issues. One is the idea of an insight, where even a child can see the answer immediately. We don’t know how to automate such thinking. But the other issue is the near-impossibility of creating a formal proof that the mutilated chessboard cannot be tiled with dominoes. Any explicit proof looks ludicrously baroque given the obviousness of the result. Contrast this with Cantor’s theorem, a deep result that has a trivial proof. Note that this issue has nothing to do with AI.

Larry Paulson