[norlygfyd]

Soundness of Lean requires more than correctness of the kernel - it requires that the theory be sound. That, frankly, is a matter of mathematics folklore. "It is known" that the combination of rules Lean uses is sound... unless it isn't.

[munchler]

That would be a bug in math itself, rather than a bug in Lean. It's possible, of course, but even less likely.