Soundness bugs in lean are not unheard of. That's why they recommend using external checkers for "malicious" proofs.

https://github.com/leanprover/lean4/issues/14576