Comment by davesque

Regarding automatic formalization of proofs using AI, how do we know the formalization doesn't contain errors?