[markusde]

You can't prove something untrue (in the sense that it implies false) without proving that the theorem prover is is unsound, which I think at the moment is not known to be possible in Lean.

But you're exactly right. There's nothing linking theorem prover definitions to pen and paper definitions in any formal system.