Lean is like a statically typed programming language and validity is guaranteed if it compiles. The only room for errors is in translating a non-Lean theorem into Lean, so that you are not proving what you think you are proving.
> A design (or implementation) cannot ever be declared “correct” on its own. It can only ever be “correct with respect to a given specification.” Whether the formal specification correctly describes the problem to be solved is a separate issue.
