[FOM] Talk on Formal Verification

Lawrence Paulson lp15 at cam.ac.uk
Wed Feb 3 09:32:13 EST 2016

Continuing the discussion…

> On 1 Feb 2016, at 04:49, Harvey Friedman <hmflogic at gmail.com> wrote:
> Are we missing some powerful fundamental principles that are
> still absolutely certain - e.g., derivable from ZFC (and fragments),
> that we are using implicitly? Or are we humans really operating on a
> fundamental intuition that defies any kind of direct formalization?
> And so the frustrating thing that we keep doing is ignoring these
> underlying unstated fundamental principles, and keep repeating
> different forms of the proof that these unstated principles are in
> fact derivable from ZFC?

Surely the latter is the case: insights derived from experience and general knowledge will always be light years ahead of deductive proofs. But the latter have the advantage of always being correct. I never sought to replace human intuition but to assist it. To give an example: Cantor’s theorem is regarded as a significant result, while the pigeon-hole principle is trivial and the famous problem of tiling the mutilated chessboard with dominoes is for children. But once formalised, Cantor’s theorem is the one with a trivial proof, while the pigeon-hole principle requires at least an induction and the mutilated chessboard needs an elaborate argument. (The 8X8 version of the mutilated chessboard can be solved automatically using a SAT solver, but only by brute force, and it can be defeated by making the board bigger.)

> Under current known methods for automated reasoning with no human interaction, how long would it take to come up with a proof of ZWOT (after posing ZWOT)?

Here’s a different example, due to Tim Gowers: does there exist a series of 100 consecutive composite numbers? (Of course there does, by the prime number theorem. But what about a constructive proof?) I don’t think that a computer has a hope with this type of problem. For all its achievements, AI has accomplished nothing that resembles insight or creativity. Our technology is good at taking a gigantic lemma library and finding the right way of putting together perhaps a dozen of them to prove a desired result. It’s a great way of closing small gaps in an argument that has been sketched out by a mathematician, but it doesn’t replace a mathematician. I don’t think that the well-ordering theorem could be proved automatically in any amount of time. Cantor’s theorem can be, simply because it has a very short proof.

> Of course, ifyour community actually does certify something that later turns out to be flawed, and top researchers were involved, then that is a whole new story. I assume that that hasn't happened, at least for a longtime?

As far as I’m aware, nobody has ever published a machine proof of a theorem that turned out to be false. A number of software errors have been reported in various systems, and it’s encouraging that generally these have been recognised by the users themselves. 

Larry Paulson

More information about the FOM mailing list