that's misunderstanding what lean does. It proves many statements of the form A implies C (I'll write this as A => C). If you chain many of these together, say A => B1 => B2 => ... => B500_000 => C, what you do is
1. examine A, and
2. examine C, and
3. rely on the Lean kernel to ensure that all of the interior transitions are correct.
Modulo a soundness bug in the lean kernel (which do occur), the entire proof is then correct, even if you only need to inspect the small fragments A and C to understand if this correct proof is interesting. But the semantics of the statements B1 ... B500_000 are irrelevant to the correctness of the final implication A => C (again, modulo soundness bugs in the lean kernel).
1. examine A, and
2. examine C, and
3. rely on the Lean kernel to ensure that all of the interior transitions are correct.
Modulo a soundness bug in the lean kernel (which do occur), the entire proof is then correct, even if you only need to inspect the small fragments A and C to understand if this correct proof is interesting. But the semantics of the statements B1 ... B500_000 are irrelevant to the correctness of the final implication A => C (again, modulo soundness bugs in the lean kernel).