Much of the point is that you have to understand the lean statement, not its proof. If the proof checker says it's good and reports that it just uses the usual axioms, then you can trust that they imply the statement. And the statement is never the 500k line part.

> but given that we’re being asked to accept 500k+ line Lean proofs that check but could easily have major semantic errors hidden in them, what’s the plan?

What does it mean for a semantic error to be "hidden in" a proof? The proof has premises and a conclusion, and if you trust the lean kernel it isn't possible for the innards of a proof to contain an error of any kind.

There could be a semantic mismatch between the statement you claim to have proved and the statement that the proof proves, but that has nothing to do with what's inside the proof - it's all right there on the surface.