Comment by dwohnitmok

The structure of Lean does impose that. The code isn't being run, it's being type checked. And that's it. The overwhelming majority of Lean code is never run. It exists only to be type checked (because type checking is equivalent to verifying the proof).

You could imagine the typechecker has bugs (and indeed another comment mentions examples of bugs!). Crucially though anytime the typechecker has a bug fixed you could rerun the typechecker on the code to see if it still type checks.

This is the whole promise of formal verification. It reduces the problem of verification purely to the typechecker. If the typechecker is correct, then the proof is verified, no matter how many lines of code the proof is. As a sibling comment puts it, the chance of bugs mainly scales with the number of lines of code in the typechecker, not in the amount of lines of Lean code.

Your question is akin to asking, "yes this spellchecker ran fine on your essay, but are you sure it runs fine on War and Peace? That's 1000x more words!" To which the answer is the number of words doesn't matter if the spell checker is correct (which it might not be! And longer passages might reveal more bugs! But you can always rerun it). The main source of bugs is more lines of code in the spell checker, not in number of words in the text.