Comment by kenferry
21 hours ago
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.
An error in the formalization could also be that you formally prove something different from what you think you proved.
All that needs to be checked to avoid that is the statement of the main theorem. Any divergence further inside means you proved the main theorem differently than you thought you did -- but you still proved it.
This assumes the Lean kernel itself isn't bugged, but getting it correct is a matter that affects all uses, not just this one, so the cost of making it correct is spread over all those uses.