[FOM] Certainty of formal proofs

[Rene Vestergaard]

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.

Cheers,
Rene