I read it more as him saying that at the end of the day a human is inputting symbols into Lean, and a human is interpreting the meaning of the proof that Lean h

I read it more as him saying that at the end of the day a human is inputting symbols into Lean, and a human is interpreting the meaning of the proof that Lean has verified. Not that the mechanics of the proof checking are in doubt, but that that meaning of it all is still a social consensus.