> 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.
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.