[FOM] Talk on Formal Verification

[Ben Sherman]

> On Fri, Jan 29, 2016 at 4:22 PM, Timothy Y. Chow <tchow at alum.mit.edu <mailto:tchow at alum.mit.edu>> wrote:
>      A typical semiformal proof of a major theorem should, nowadays, be
>      thought of as including a few hundred CPU hours of computation
>      with commercial software on a machine with a few terabytes of
>      space.

I think it's important to distinguish between computation required for proof search and computation required for proof checking. While I can imagine using lots of computation for proof search, I doubt that the verification of any "good" proof of a "major theorem" should require excessive computation (not including dependencies). The reason is that I think our own ability to understand proofs roughly scales with the computation required for a computer to check a formal proof, and we will not regard proofs which are difficult to understand as interesting mathematics.

> Even if you don't think this will happen, the point is that this sort of 
> thing could happen, and we are already witnessing baby examples of it 
> like the proof that checkers is a draw.

The proof that checkers is a draw is an excellent example to make my point: formally checking this proof requires excessive computation. Now, as far as I know, checkers has not died: people still play checkers, and were I to play, I certainly wouldn't play optimally. Why not? Because I don't understand the proof. If it turned out there were some simple, easily comprehensible "trick" one could follow to play optimally (i.e., an easily verifiable proof), everyone would stop playing checkers.

The checkers example is also interesting in that it should be a relatively short formal proof that requires a lot of computation to check. Which of these two metrics, generally, should we aim to minimize? Each seems to correspond to difficulty of understanding a proof, but in different senses.

Tim, perhaps I don't understand what you mean by a (computerized) semiformal proof. What springs to mind for me is, for example, a tactic script in Coq, which can indeed require far more computation to run (generate the formal proof term) than to check the formal term it generates. But many tactics (particularly the time-consuming ones) are more proof-search commands than proofs. In principle, one could replace the proof-search commands with the proof terms that are actually found, and arrive at a proof that is both quicker to run and more explanatory. In my mind, a semiformal proof is a document which explains to a human why a theorem is true, so I fail to see how computation would play a major role.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160130/62596c52/attachment-0001.html>