[FOM] Talk on Formal Verification

[Lawrence Paulson]

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