Comment by tossandthrow
10 hours ago
The proof system is relatively easy to verify.
I am not entirely sure about lean, but the core algebras for systems like lean are in the 100s of lines of code.
You can likely convince yourself it is correct in a weekend or less - especially with an Ai to help you understand it.
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.
the Nanoda type-checker for Lean is ~5,000 lines of Rust:
https://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:
https://lawrencecpaulson.github.io/2026/07/30/Collatz.html