[FOM] Certainty of formal proofs

[Harvey Friedman]

Reply to Vestergaard 11:07AM 6/22/03.

>In line with what has already been discussed, it is worth mentioning 
>that a number of theorem provers allow for their internal proof 
>states to be exported as, say, a typed lambda-term. Such exported 
>proof terms are independently checkable. Indeed, and as a 
>checker/parser is fairly simple to write, the idea is that anyone 
>wishing to verify the correctness of a proof someone has developed 
>in an arbitrarily complex theorem prover can simply write their own 
>(simple) checker and run it against the exported proof term. This 
>has the added benefit that the original theorem prover can be as 
>buggy as may be the case without affecting the certainty that can be 
>attached to the correctness of the products it produces. 
>Furthermore, and as checking really is a lot simpler than generating 
>the proof in the first place, the amount and complexity of software 
>that one must place trust in is vastly reduced.
>
>

Yes, I am aware of this. I just want to capitalize on this idea and 
push it to its absolute extreme, suggesting that the entire CORE 
PROOF CHECKER, including hardware, can be humanly verified. 
Furthermore, the human verification might be  subject to additional 
computer verification to create a special level of certainty.

I wouldn't think of using lambda calculus for this purpose. String 
lookups is the way to go.