Comment by Panoramix

How do we know the formalization itself doesn't have any errors? AFAIK it's very far from trivial to formalize something.