The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled.

Note to other users: don’t downvote this kind of comment, answer it.