Doesn't Lean also have libraries? Anyway, there could also be hardware errors, I suppose.
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.
alt Hacker News
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.