Comment by rbanffy

Unless humans understand them, can we trust such formalisations? We can prove the formalisation is correct, but we can't prove it accurately reflects what we are trying to prove.