Comment by CGamesPlay

If there's a bug in the theorem prover and it proves itself, it still has that bug.