r/programming • u/ngruhn • 3d ago

Lean explained with TypeScript

https://gruhn.me/blog/2026-08-29/
75 Upvotes

92% Upvoted

12 comments sorted by

30

u/Hot-Employ-3399 3d ago

> Lean has gained hugely in popularity with the advent of LLMs. LLMs write tons of code quickly but verification is laborious

I'm surprised that this llm-popularity feels touched only Lean, not rocq/isabelle/agda/whatever. At least when I see "proved", it's lean, not other systems.

38

u/Smallpaul 3d ago

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 3d ago

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.

11

u/Smallpaul 3d ago

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 2d ago

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 1d ago

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

6

u/dyingpie1 3d ago

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

5

u/kid_vio 3d ago

Slop article? Asking for a friend.

24

u/ngruhn 3d ago

100% human written. Pinky promise 

4

u/kid_vio 3d ago

Verified, and up vote confirmed :) 👍

4

u/770grappenmaker 2d ago

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.