Comment by Garlef

... and even if you formalize it, it could still be false due to an error in the theorem prover itself.