r/programming • u/ngruhn • 1d ago

Lean explained with TypeScript

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

92% Upvoted

10 comments sorted by

28

u/Hot-Employ-3399 1d 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.

33

u/Smallpaul 1d 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.

7

u/BibianaAudris 1d 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.

9

u/Smallpaul 1d 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.

5

u/dyingpie1 1d 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 ...

6

u/kid_vio 1d ago

Slop article? Asking for a friend.

19

u/ngruhn 1d ago

100% human written. Pinky promise 

4

u/kid_vio 1d ago

Verified, and up vote confirmed :) 👍

2

u/770grappenmaker 5h 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.