the Nanoda type-checker for Lean is ~5,000 lines of Rust: https://leodemoura.github.io/blog/2026-3-16-who-watches-the-provers/ https://leodemoura.github.io/blo

the Nanoda type-checker for Lean is ~5,000 lines of Rust: https://leodemoura.github.io/blog/2026-3-16-who-watches-the-provers/ 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.html 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 https://lawrencecpaulson.github.io/2026/07/30/Collatz.html