Most systems i have seen are way beyond a 100 lines. And their GitHub repository contain many issues, often soundness bugs. (Granted, many get fixed very fast.)

You need to understand the concept of the core algebra and 100s (with the s), then I think you'd be better positioned to understand my comment.

And granted, I don't know the exact details about Lean. It might be that they don't have an incredibly simple core - as has elsewise been the norm.