Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct?

How have we not merely substituted one verification problem for another?

The point of Lean is that it can be mechanically verified by a proof checker.