[FOM] Checkers is a draw

[Timothy Y. Chow]

Neelakantan Krishnaswami <neelk at gs3106.sp.cs.cmu.edu> sent me a very 
informative reply to my remarks/questions about formal verification, which 
I am forwarding to FOM with permission.

> Hi Timothy,
> 
> I work in formal verification, so maybe I can shed some light on the
> puzzle you posed in this and your earlier message.
> 
> The short answer is that proof-checking in most proof assistants (Coq,
> Isabelle, Lego, etc) is not NP-complete -- it is complete for
> higher-order arithmetic. That is, checking a proof can take time
> bounded by the longest-running function you can prove terminates with
> some version of higher-order arithmetic.
> 
> So proof checking can take a really stunningly huge amount of time.
> 
> The reason for this is that most proof checkers are basically variants
> of typed lambda calculus, whose type theories include a rule of the 
> following form:
> 
>   e : A     A <--> B
>   ------------------
>        e : B
> 
> where --> is the reduction relation for the lambda calculus. So if e
> is a proof of A, and A is beta-reducible to B or vice-versa, then e 
> is also a proof of B.
> 
> So you can write (total) programs as typed lambda terms, and proof
> checking can involve running those programs. We still know that proof
> checking will terminate, because well-typedness plus the consistency
> of the logic guarantees termination, but it can take a really long
> time.
> 
> To understand why this sort of rule is necessary, consider the example
> of showing that 170 * 40 = 6800. No one will do this proof by
> appealing to Peano's axioms, because it would be thousands of lines
> long. Instead we will /calculate/ that 170 * 40 gives 6800, and then
> appeal to reflexivity, which is a one-line proof plus some
> computation.
> 
> Poincare foresaw the need for this sort of rule a century ago; the
> story goes that upon seeing a formal proof of some trivial arithmetic
> fact he is supposed to have asked, "And how will you prove a real
> theorem?" In his essay, "Science and Hypothesis", he contrasted
> computation (which he called verification) with deduction proper, and
> argued that only deductive steps should be included in a formal proof,
> since the calculations can be re-done by the person checking the
> proof.
> 
> So in type theory this sort of conversion rule is sometimes called the
> Poincare principle.
> 
> It also means that proofs that are a mix of computation (say, to
> generate and test a huge but finite number of configurations) and
> deduction (to show that these configurations are all the ones you need
> to check) are very natural to represent in type theory. This is
> essential to Gonthier's formal proof of the four-color theorem, and to
> Hales's (ongoing) formal proof of the Kepler conjecture.
>
> -- 
> Neel R. Krishnaswami
> neelk at cs.cmu.edu