Well, the point of the _computer_ formalization is that it's checkable.

An error in the formalization would be a bug in lean. Which, as we know, certainly seems plausible (I've mused on if these giant proofs are incentivizing LLMs to find lean bugs to exploit), but at least it's a smaller surface area.