Unfortunately Lean’s distribution went from somewhat about 15 MiB in times of Lean 3 to more than 2,5 GiB when unpacked nowadays for no good reason. This is too much. Even v4.0.0-m1 was a 90 MB archive. Looks like that Lean’s authors do not care about this anymore.
Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad.
Personally, I stopped using Lean after the last update broke unification in a strange way again.
i love lean4, best in class functional programming language. but i think its "perfectability" is kinda hamstrung by baking non-constructive axioms into the standard library. the kernel has to treat these as opaque constants that cannot be reduced.
i tend to stick with agda for doing mathy programming. i kinda want lean4 to replace haskell at some point in the future as the workhorse production typed fp language.
Are they actual project running some business in the wild? I only played with coq in university, while I saw F# being employed in insurance companies. I only heard about lean through HN posts.
I don't know about running per se but practical applications (as in done for product/service) exist. A notable practitioner for Isabelle and Lean is AWS[0]. There is also TLA+ for a more practical tool.
The most widely used variant of these proof assistants are probably formally verified compilers, like compcert, which are used in some highly regulated industries like aviation.
Indeed! I got to about 20 with A-B-C but it somehow became harder after those. The multitude of C-something is obvious but I didn't realize there's so many A* languages (apl, ada, agda, alice, algol, applescript, apex, ampl, assembly..)
> languages without types tend to grow them, like PHP in 7.4 and Python type annotations
Well ... that is a trend that is driven largely by people who love types.
Not everyone shares that opinion. See ruby.
It is very hard to try to argue with people who love types. They will always focus on "types are great, every language must have them". They, in general, do not acknowledge trade-offs when it comes to type systems.
So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types. I saw this happen "live" in ruby; I am certain this happened in python too.
> inevitably, people want to push types. even Go. C++ templates are the ultimate example. if it can be computed at compile time, at some point someone wants to, like Rust's ongoing constification.
And many people hate C++ templates. But comparing that language to e. g. ruby is already a losing argument. Languages are different. So are the trade-offs.
> dependent types can get you there. hence perfectable.
So the whole point about claiming a language is "perfectable", means to have types? I don't agree with that definition at all.
> most languages have no facility for this,
How about lisp?
> this lets you design APIs in layers and hide them behind syntax.
The language already failed hard syntax-wise. This is a problem I see in many languages - 99% of the language designers don't think syntax is important. Syntax is not the most important thing in the world, but to neglect it also shows a lack of understanding why syntax ALSO matters. But you can not talk about that really - I am 100% certain alok would disagree. How many people use a language also matters a LOT - you get a lot more momentum when there are tons of people using a language, as opposed to the global 3 or 4 using "lean".
> > languages without types tend to grow them, like PHP in 7.4 and Python type annotations
...
> Not everyone shares that opinion. See ruby.
All programming languages that have values (i.e. all of them) have types, because you cannot have a concrete value that doesn't have a type. This includes Ruby.
The only difference is whether the language lets you annotate the source code with the expected type of each value.
This is why you observe that all languages trend towards visible typing: The types are already there and it's only a matter of whether the language lets the programmer see it, or lets a linter enforce it, and everyone likes linters.
> So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types.
Maybe you misidentified where the type declaration is coming from? It might not be coming from people who want to see types in the source code, it most probably is coming from people who want a decent linter.
In 2026, programming without type-enforcement is like programming using an LLM; it's quicker, but less safe.
> So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types.
Who else would add them, besides people who want them? I'm confused about what you're even claiming here. It sounds like you feel that there's a vocal minority of type enthusiasts who everyone else is just humoring by letting them bolt on their type systems.
> For Eliza Zhang, who bet I couldn’t write a web app in C in one week using only the standard library. She was right. I didn’t know what any of those words meant. But I said the fuck I can’t, and that’s how I got into coding.
interesting the ones they chose to name; I would have probably started with 6502/68000/68020/z80 assembly, fortran, cobol, basic, c, ada, simula 67, sh, zsh, bash, napier 88, tcl, perl, rexx, before hitting the next generation of python, c++, etc.
The thing I found really surprising about Lean is that although it is really focused on proving stuff, it has some surprisingly enormous footguns. What do you think the result of these are?
The first should be a compile time error right, because `UInt8.ofNat` is going to require that its argument is 0-255. And the second should be a compile time error because subtraction should not give a `Nat` unless the first argument is definitely more than the second.
These are both pretty reasonable semantics for these functions. `UInt8.ofNat : Nat -> UInt8` might reasonably map the infinite number of `Nat` values to `UInt8` by taking the natural number modulo 256. And it's sensible enough that subtraction with natural numbers should saturate at 0.
These aren't the only reasonable semantics, and Lean will certainly let you define (for instance) a subtraction function on natural numbers that requires that the first argument is greater than or equal to the second argument, and fail at compile time if you don't provide a proof of this. These semantics do have the benefit of being total, and avoiding having to introduce additional proofs or deal with modeling errors with an `Except` type.
Who said that it should be a compile time error? That’s just a convention, and this is definitely not a bad one. No one is going to like the need to pass each time a proof that `a ≥ b` for every `a - b` invocation. Taking into account that this proof will most likely be an implicit argument, that would be a really annoying thing to use.
On the other hand, array indices by default do require such a proof, i.e., this code produces a compile time error:
What is up with so many people doing weird capitalization now? Is this some Bay-tech flex? Alok writes their own name, and other names, with leading caps, but not the first word in sentences? It makes it so uncomfortable to read.
Wow, I read the whole thing without noticing that.
But as someone who came of age in the AIM / ICQ / IRC days, it feels pretty normal. That's just how we wrote. I still fall into it by accident when the context is right and I'm not thinking about it (eg Slack at work). I hope youngsters aren't judging me for it.
I think this is just applying the same informal writing style used in, for example, online chats with friends, to a relatively-informal blog post. I don't think this has anything to do with the Bay Area or its tech industry in particular.
YES, THIS (capitalized on purpose). Folks, please use reasonably correct writing syntax. You CAN do better .. At least think of the AIs consuming your writings.
i notoriously ignore using my shift key when im typing informal stuff (comments, chats to coworkers, friends, etc). big ol emails = you'll see me using my shift key.
most of this comes from me noticing how funny sql looks with all the people trying to use caps all over the place as if anyones working in a place without syntax highlighting in 2026. sql is the wild west and everyones sql looks like shit there is no shame. i was told i needed to use caps more early on in sql and i lmfao'd, but i was new to the career and that scarred me. i write lower case sql just to spite others now and if you see something capitalized you know i meant it, but for the most part you have to pay me to use my shift key.
Only you can stop generational SQL abuse. Capitalize keywords, indent grouped syntax, and use prefix commas on newlines. Write readable code, for God’s sake, you filthy heathens.
> because it's perfectable. it's not perfect, but it is perfectable. you can write down properties about Lean, in Lean.
Homoiconicity anyone? Lisp is one of the oldest high-level programming languages, and it's still around.
Unfortunately Lean’s distribution went from somewhat about 15 MiB in times of Lean 3 to more than 2,5 GiB when unpacked nowadays for no good reason. This is too much. Even v4.0.0-m1 was a 90 MB archive. Looks like that Lean’s authors do not care about this anymore.
Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad.
Personally, I stopped using Lean after the last update broke unification in a strange way again.
Static linking wonders?
Originally Lean was coded in C++, and dynamically linked executable, if I remeber correctly.
Lean is far off the most bloated one. Isabelle most likely takes that spot, the main archive includes a whole vscodium among other things.
>> Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three.
> Lean is far off the most bloated one. Isabelle most likely takes that spot.
Among these three is the operative phrase here.
I hate to be pedantic, but we are talking about theorem provers here :)
i love lean4, best in class functional programming language. but i think its "perfectability" is kinda hamstrung by baking non-constructive axioms into the standard library. the kernel has to treat these as opaque constants that cannot be reduced.
i tend to stick with agda for doing mathy programming. i kinda want lean4 to replace haskell at some point in the future as the workhorse production typed fp language.
I've been messing around with a computer algebra simplifier in Lean:
https://github.com/dharmatech/symbolism.lean
Lean is astonishingly expressive.
Are they actual project running some business in the wild? I only played with coq in university, while I saw F# being employed in insurance companies. I only heard about lean through HN posts.
I don't know about running per se but practical applications (as in done for product/service) exist. A notable practitioner for Isabelle and Lean is AWS[0]. There is also TLA+ for a more practical tool.
The most widely used variant of these proof assistants are probably formally verified compilers, like compcert, which are used in some highly regulated industries like aviation.
[0]: https://isabelle.systems/zulip-archive/stream/247541-Mirror.... and https://lean-lang.org/ (Cedar)
Fortran, Basic, APL, Beta, Odin, Self, C, C++, Objective-C, C#, C--, D, Scheme, Clojure, F-Script, Eiffel, COBOL, Ocaml, Haskell, Snobol, Crystal, Forth, Python, Lisp, Brainfuck, Java, Oak, Javascript, TypeScript, Wasm, Logo, Elang, Elixir, Gleam, Elm, Zig, m4, Tcl, Simula, Smalltalk
Fun challenge. Unlike the author, I have nothing really to add.
I just wanted to say that "I did NOT write it with ..."
Indeed! I got to about 20 with A-B-C but it somehow became harder after those. The multitude of C-something is obvious but I didn't realize there's so many A* languages (apl, ada, agda, alice, algol, applescript, apex, ampl, assembly..)
this is the log post that put lean on my radar, though I haven't played with it yet: https://kirancodes.me/posts/log-ocaml-to-lean.html
Great post. Thanks!
XL is a very interesting modern iteration on extensible languages, unfortunately it seems abandoned.
i like this website, it shows documentation when hovering the code while i see similar stuffs really rare in web blog areas
I believe you can thank Verso for that:
https://github.com/leanprover/verso
Very nice!
I've been wanting to adopt Lean for a project but wasn't sure about the speed. Nice to hear that it should be good on that front.
> languages without types tend to grow them, like PHP in 7.4 and Python type annotations
Well ... that is a trend that is driven largely by people who love types.
Not everyone shares that opinion. See ruby.
It is very hard to try to argue with people who love types. They will always focus on "types are great, every language must have them". They, in general, do not acknowledge trade-offs when it comes to type systems.
So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types. I saw this happen "live" in ruby; I am certain this happened in python too.
> inevitably, people want to push types. even Go. C++ templates are the ultimate example. if it can be computed at compile time, at some point someone wants to, like Rust's ongoing constification.
And many people hate C++ templates. But comparing that language to e. g. ruby is already a losing argument. Languages are different. So are the trade-offs.
> dependent types can get you there. hence perfectable.
So the whole point about claiming a language is "perfectable", means to have types? I don't agree with that definition at all.
> most languages have no facility for this,
How about lisp?
> this lets you design APIs in layers and hide them behind syntax.
The language already failed hard syntax-wise. This is a problem I see in many languages - 99% of the language designers don't think syntax is important. Syntax is not the most important thing in the world, but to neglect it also shows a lack of understanding why syntax ALSO matters. But you can not talk about that really - I am 100% certain alok would disagree. How many people use a language also matters a LOT - you get a lot more momentum when there are tons of people using a language, as opposed to the global 3 or 4 using "lean".
> > languages without types tend to grow them, like PHP in 7.4 and Python type annotations
...
> Not everyone shares that opinion. See ruby.
All programming languages that have values (i.e. all of them) have types, because you cannot have a concrete value that doesn't have a type. This includes Ruby.
The only difference is whether the language lets you annotate the source code with the expected type of each value.
This is why you observe that all languages trend towards visible typing: The types are already there and it's only a matter of whether the language lets the programmer see it, or lets a linter enforce it, and everyone likes linters.
> So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types.
Maybe you misidentified where the type declaration is coming from? It might not be coming from people who want to see types in the source code, it most probably is coming from people who want a decent linter.
In 2026, programming without type-enforcement is like programming using an LLM; it's quicker, but less safe.
> So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types.
Who else would add them, besides people who want them? I'm confused about what you're even claiming here. It sounds like you feel that there's a vocal minority of type enthusiasts who everyone else is just humoring by letting them bolt on their type systems.
> do not acknowledge trade-offs when it comes to type systems
Could you elaborate?
Well Ruby kinda brought forth Crystal which while its own Programming Language is kinda Ruby but with Types.
> How about lisp?
I was wondering why lisp (and forth) were omitted from the initial list of languages named in the post.
I guess Scheme is in the list has ok macros.
A very polite reminder that Elixir exists.
> For Eliza Zhang, who bet I couldn’t write a web app in C in one week using only the standard library. She was right. I didn’t know what any of those words meant. But I said the fuck I can’t, and that’s how I got into coding.
interesting the ones they chose to name; I would have probably started with 6502/68000/68020/z80 assembly, fortran, cobol, basic, c, ada, simula 67, sh, zsh, bash, napier 88, tcl, perl, rexx, before hitting the next generation of python, c++, etc.
wait, I'm intrigued, it says the blog itself is lean code. How? It's rendered, like pollen?
It is verso. My understanding is that it's like really fancy javadocs that makes communicating Lean code easier for everyone.
https://github.com/leanprover/verso
clojure exists as an example of people trying types and then realising it's cruft and not needed.
The thing I found really surprising about Lean is that although it is really focused on proving stuff, it has some surprisingly enormous footguns. What do you think the result of these are?
The first should be a compile time error right, because `UInt8.ofNat` is going to require that its argument is 0-255. And the second should be a compile time error because subtraction should not give a `Nat` unless the first argument is definitely more than the second.Nope! Both give 0.
These are both pretty reasonable semantics for these functions. `UInt8.ofNat : Nat -> UInt8` might reasonably map the infinite number of `Nat` values to `UInt8` by taking the natural number modulo 256. And it's sensible enough that subtraction with natural numbers should saturate at 0.
These aren't the only reasonable semantics, and Lean will certainly let you define (for instance) a subtraction function on natural numbers that requires that the first argument is greater than or equal to the second argument, and fail at compile time if you don't provide a proof of this. These semantics do have the benefit of being total, and avoiding having to introduce additional proofs or deal with modeling errors with an `Except` type.
Who said that it should be a compile time error? That’s just a convention, and this is definitely not a bad one. No one is going to like the need to pass each time a proof that `a ≥ b` for every `a - b` invocation. Taking into account that this proof will most likely be an implicit argument, that would be a really annoying thing to use.
On the other hand, array indices by default do require such a proof, i.e., this code produces a compile time error:
Kevin Buzzard even wrote a blog post about a similar question about division by zero: https://xenaproject.wordpress.com/2020/07/05/division-by-zer...>The recommended way to install Lean is through VS Code and the Lean 4 VS Code extension,
Lol
There are community-built editor supports. For example,
- Emacs: https://github.com/leanprover-community/lean4-mode
- Neovim: https://github.com/Julian/lean.nvim
I'm using the Emacs lean4-mode and it's pretty good.
It makes complete sense to polish that usecase.
What is up with so many people doing weird capitalization now? Is this some Bay-tech flex? Alok writes their own name, and other names, with leading caps, but not the first word in sentences? It makes it so uncomfortable to read.
Wow, I read the whole thing without noticing that.
But as someone who came of age in the AIM / ICQ / IRC days, it feels pretty normal. That's just how we wrote. I still fall into it by accident when the context is right and I'm not thinking about it (eg Slack at work). I hope youngsters aren't judging me for it.
we wrote like that because each message was a single sentence
if you wanted more than one sentence you sent one then wrote the other
it's painful to read longform
the victorians didn't give up on punctuation and regular english just because they had the telegraph
I think this is just applying the same informal writing style used in, for example, online chats with friends, to a relatively-informal blog post. I don't think this has anything to do with the Bay Area or its tech industry in particular.
YES, THIS (capitalized on purpose). Folks, please use reasonably correct writing syntax. You CAN do better .. At least think of the AIs consuming your writings.
I ReSpEcTfUlLy DiSaGrEe FrIeNd -- PeOpLe LoVe SlOp. =3
It communicates a certain tone that is sometimes what one is going for. I do it in HN comments sometimes if I'm feeling, like, dry or dismissive.
its not caused by a habit of writing authentically formatted Homestuck rp smut
but surely its correlated
Is it due to the feature that the author claimed "this blog post is itself Lean code"?
It’s to show you’re too cool for grammar rules.
i notoriously ignore using my shift key when im typing informal stuff (comments, chats to coworkers, friends, etc). big ol emails = you'll see me using my shift key.
most of this comes from me noticing how funny sql looks with all the people trying to use caps all over the place as if anyones working in a place without syntax highlighting in 2026. sql is the wild west and everyones sql looks like shit there is no shame. i was told i needed to use caps more early on in sql and i lmfao'd, but i was new to the career and that scarred me. i write lower case sql just to spite others now and if you see something capitalized you know i meant it, but for the most part you have to pay me to use my shift key.
my trauma is now your trauma
Only you can stop generational SQL abuse. Capitalize keywords, indent grouped syntax, and use prefix commas on newlines. Write readable code, for God’s sake, you filthy heathens.
The swearing is another thing I keep seeing more of.