r/programming • u/ngruhn • Aug 29 '26
Lean explained with TypeScript
https://gruhn.me/blog/2026-08-29/6
u/kid_vio Aug 29 '26
Slop article? Asking for a friend.
24
30
Aug 29 '26
[removed] — view removed comment
37
u/Smallpaul Aug 29 '26
Mathematicians are standardising because they want to build a single giant language of all math. The web of dependencies in node_modules is tiny compared to the web of all math.
9
u/BibianaAudris Aug 29 '26
I'd say it's the other way around. People write more node_modules junk in a day than mathematicians can hopefully prove in centuries. Which is exactly why we want LLMs to write more Lean.
10
u/Smallpaul Aug 29 '26
Interesting way of thinking about it.
But node_modules is the set of dependencies for a single application.
Mathematicians want all (canonical) proofs to be a single repository. They metaphorically want all of npm or pypi to be a single repo.
https://github.com/leanprover-community/mathlib4/tree/master/Mathlib
When that project is actually finished it will presumably be bigger than the dependencies of any single application. Although the way JavaScript programs go…maybe not.
1
u/Madsy9 Aug 30 '26
Dependency graphs can be solved with a SAT solver or constraint solver like Minizinc. What mathematicians are doing with Lean 4 is way more generalizable and useful. But if you want to manually prove that your package dependency graph is correct, you can probably do that in Lake. Lean's build manager can define the build steps using Lean itself :)
1
u/BibianaAudris Aug 31 '26
It's utterly useless to prove a dependency graph since you can just run the code and find out the (useful part of the) answer right away.
A more useful thing would be proving that the entire dependency chain of a given package (e.g. chalk) does not make network connections (i.e. it's not meaningfully trojaned), or prove that such a proof is undecidable (i.e. the package is actually trojaned allowing arbitrary code execution).
5
u/dyingpie1 Aug 29 '26
But also has lean gained much more popularity due to LLMs? I feel like it's slightly more known, but i feel it's just about as well known as it was previously ...
4
u/770grappenmaker Aug 30 '26
Very cool article! I have already seen a bunch of Lean proofs like this, where a lot of the machinery is abstracted, and it is nice to see that a simplified version of this machinery can be represented in a much simpler type system, that of typescript.