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.)
replyYou 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.
replyAnd 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.
the Nanoda type-checker for Lean is ~5,000 lines of Rust:
replyhttps://leodemoura.github.io/blog/2026-3-16-who-watches-the-...
...and for those who are looking to roll-their-own:
https://ammkrn.github.io/type_checking_in_lean4/title_page.h...
...and some thoughts on putting stuff in the kernel: