[FOM] shocked?

[Rob Arthan]

> Message: 8
> Date: Tue, 28 Oct 2003 13:12:54 -0500
> From: Harvey Friedman <friedman at math.ohio-state.edu>
> Subject: [FOM] shocked?
> To: fom <fom at cs.nyu.edu>
> Message-ID: <BBC41BD6.6F33%friedman at math.ohio-state.edu>
> Content-Type: text/plain; charset="US-ASCII"
>
> I seem to be somewhat shocked that the recent thread concerning "what is a
> proof" does not seem to be taking into account the rather massive
> literature concerning Proof Assistants, where actual human beings actually
> interact with actual computers to get humanly created proofs checked. No
> line by line Hilbert style system is even remotely used in such systems.
> Instead, they are based on variants of natural deduction, with an emphasis
> on lemma refinement, just like most ordinary proofs humans like.

This is not strictly true. Many practical mechanized theorem-proving systems  
follow Milner's LCF paradigm (e.g., the several variants of Mike Gordon's 
HOL, ProofPower, Isabelle, NuPrl etc.). These systems do, in effect, check 
line-by-line primitive inferences at the lowest level of their operation. 
However, this is analogous to the machine code level in programming and, as 
in programming, not many users work at this level.

Typical users constructs proofs using higher-level tools. The higher level 
tools are analogous to (fairly intelligent) interpreters or compilers that 
can generate a string of primitive inferences to prove goals in a given 
class. Very commonly, the higher-level tools include a framework for 
goal-oriented proof, based on Larry Paulson's ideas, which provides a natural 
deduction-like look and feel.  However in a useful system, the higher-level 
tools will also include automatic decision procedures and heuristics for 
equational reasoning, first order reasoning, arithmetic etc. etc.

The existence of good automation does change your strategy a little compared 
with "ordinary proofs humans like": a common technique is to transform a 
given problem, ideally via an equivalence, into a domain where there is a 
decision procedure (e.g., use induction to reduce a diophantine problem into 
linear arithmetic) and then throw the decision procedure at the result 
(without much caring whether the transformed problem is easy for a human to 
understand, since the decision procedure is better at that kind of thing than 
a human is).

Regards,

Rob Arthan.