How to Avoid the Formal Verification of a Theorem Prover