> What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode

I don't think the comments are missing that at all. If the Lean compiler itself is bug-free, we can trust its verification of the 13 million lines of code. We don't need to verify them by hand.

The encoding of the theorem itself needs to be trusted, as does the compiler. The proof doesn't need to be trusted, it gets checked by the compiler.