Blog post: The Math Is Haunted

Stream: new members

[Dan Abramov]

Wrote my first blog post about Lean: https://overreacted.io/the-math-is-haunted/

It might be a bit messy and I'm not sure it teaches a lot but I wanted to get it out of my head so I can move to other topics.

Any comments/corrections are appreciated!

[Arthur Paulino]

Just some context: Lean 3, the version that got traction with mathlib, was first and foremost an interactive theorem prover. Lean 4, as a full blown programming language, is a relatively recent breakthrough.

[suhr]

Every dependent type theory is a programming language. What makes Lean different is that it's a usable programming language.

[Dan Abramov]

Yeah, that's fair! I appreciate the breakthrough-ness of the breakthrough although it also makes explaining what Lean is a bit tricky. I think positioning it as primarily a theorem prover which also gained the runnable capability (same as the historical context) is maybe the least confusing way to explain it to programmers.

[Arthur Paulino]

suhr said:

Every dependent type theory is a programming language. What makes Lean different is that it's a usable programming language.

Yes, that's encoded in my imprecise terminology "full blown programming language". I mean, there was pretty much no special reason for some programmer to use Lean 3 to build an application. The main point I wanted to make was that, if you have some extra context, Lean 4 being a programming language used mostly by mathematicians is the most likely outcome.

[Dan Abramov]

HN discussion, which might be a good place to engage with folks curious about Lean: https://news.ycombinator.com/item?id=44739315#44739780