Lean does have libraries, but since they are also in lean they are subject to the same rules. It's basically a super strong type checker. If it compiles the proof is valid. Unless there is a bug in the type checker.