Remix clone Hacker News

new | show | ask | jobs Github

▲

tossandthrow 2 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.

▲

Jaxan 2 hours ago | parent | next [-]

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.)

	▲	tossandthrow 2 hours ago \| parent [-]
		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.

▲

Jblx2 2 hours ago | parent | prev [-]

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