[FOM] Talk on Formal Verification

[Timothy Y. Chow]

Lawrence Paulson wrote:

> Here is my attempt at answering some of the questions posed by this 
> keynote lecture.
>
> IS THE SIZE OF PURELY FORMAL PROOFS OBTAINED FROM
> SEMIFORMAL PROOFS OF MAJOR THEOREMS REASONABLE? E.G., AT
> MOST TEN THOUSAND PRINTED PAGES? OR IS THERE AN EXPONENTIAL
> TYPE BLOWUP INVOLVED WHEN WE MOVE FROM THE USUAL SEMIFORMAL
> PROOFS CREATED BY MATHEMATICIANS TO A FORMAL PROOF?
>
> This is sometimes called the "de Bruijn factor?, after NG de Bruijn, who 
> posed a similar question in relation to his AUTOMATH system. Generally 
> the blowup is regarded as tolerable.

I've mentioned this point before but it seems worth repeating.  The right 
way to think about a "semiformal proof" is not as a few hundred pages of 
handwritten text.  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.  The relevant question is how much of a blowup is involved in 
converting the "standard" computation into a fully formalized one.  Note 
that the semiformal proof may in turn cite many other semiformally proved 
theorems with similar computational requirements.  If I cite the Kepler 
conjecture in my semiformal proof, does the formal verification of my 
theorem require re-running the Flyspeck computation?  We probably want the 
answer to be no, but then a new knowledge management problem creeps in if 
we maintain a large database of results that have supposedly been formally 
verified but that are never checked again.

Tim