I am learning Lean myself so forgive me as I have an overly rosy picture of it as a beginner. My current goal is to write and prove the kind of code normal programmers would write, such as real-world compression/decompression algorithms as in the recent lean-zip example: https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

Specifically, the author seems to be under the impression that Lean retains proof objects and the final proof to be checked is one massive proof object, with all definitions unfolded: "these massive terms are unnecessary, but are kept anyway" (TFA). This couldn't be further from the truth. Lean implements exactly the same optimization as the author cherishes in LCF; metaphorically, that "The steps of a proof would be performed but not recorded, like a mathematics lecturer using a small blackboard who rubs out earlier parts of proofs to make space for later ones" (quoted by blog post linked from TFA). Once a `theorem` (as opposed to a `def`) is written in Lean4, then the proof object is no longer used. This is not merely an optimization but a critical part of the language: theorems are opaque. If the proof term is not discarded (and I'm not sure it isn't), then this is only for the sake of user observability in the interactive mode; the kernel does not and cannot care what the proof object was.

The language is different (not necessarily better) in comparison to Lean, but I do agree with some of the points on dependent types. It seems both languages mostly just made different tradeoffs, which imo, were fair and have shaped them into quite efficient tools for their domains. The domain of "proofs" is large and different paradigms just have different strengths/weaknesses, Lean just specialized for a different part of this space.

Sledgehammer is nice but probably just a question of time until an equivalent can be ported/created for Lean. It might also be nice to use for explorative phases but is a resource hog, it also makes proofs concise but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer".

Working on Isabelle itself however is painful (especially communicating with developers) in comparison to Lean. Things like "we don't have bugs just unexpected behaviour" on the mailing list just seems childish/unprofessional. The callout to RAM consumption of Lean and related systems is also a bit of joke when looking at Isabelle's gluttony for RAM.

[1] for those unfamiliar with math lingo, classical logic has a lot of powerful features. One of those is the law of the excluded middle, which says something can't be true and false at the same time. That means not not true is true, which you can't say in intuitionistic logic. Another feature is proof by contradiction, where you can prove something by showing that the alternative is unsound. There's quite a few results that depend on these techniques, so trying to do everything in intuitionistic logic has run into a lot of roadblocks.

For every "well of course, just...X, that's what everybody does" group-think argument there's a cogent case to be made for at least considering the alternatives. Even if you ultimately reject the alternatives and go with the crowd, you will be better off knowing the landscape.

Sure, except that once you have a community at critical mass around a reasonably good tool, that trumps most other things. Momentum builds. People write tutorials, explainers, better documentation, etc. it hits escape velocity.

Feels like Lean, with Terrance Tao as a strong proponent / cheerleader, is in that space.

Everyone who argues “but language X is better” … may not be wrong, but they are not making the argument that matters. Is it better than the thing everyone else knows and can use and has more people hours going into it to improve it?

Feels like a “worse is better” situation; or maybe “good and popular is good enough”.

I’m not the biggest VS code fan, but a battle honed extensible IDE used by zillions and maintained by $$$ has proved itself miles ahead of the environments for alternatives. As far as i can tell, the excellent onboarding path that is the Natural Numbers Game is possible because of VS code’s hackability and ecosystem.

My main concern as I’m learning lean is that the syntax extensibility seems to be a double edged sword. Once i’ve learned a language, i want to be able to read code written in it. If everything is in a project’s own DSL, that can get out of hand, but that comes down to community/ecosystem so i’m crossing my fingers.

Is this the mathematician's variant of "my language is better than your language", or what does this post actually discus? Something fundamental in the philosophy underpinning things or just the way to express them?

'Lean or purple drank is a polysubstance drink used as a recreational drug. It is prepared by mixing prescription-grade cough or cold syrup containing an opioid drug '

proving that one of the hardest problem in CS - 'naming things' still keeps on keeping on.

It has some advantages and compelling properties, not least of which is that it's very simple, so much so that there are many implementations of checkers; most other proof systems are ultimately defined by a single implementation. It's also astonishingly efficient — the entire database can be checked in less than a second. Set theory is also a familiar foundation for mathematicians, though the question of which is a better foundation compared with type theory is very controversial. Mario Carneiro pushed forward the development of Metamath in his thesis [0].

There are downsides also, including junk theorems, and automation is weaker. It's possible that types really help with the latter. Even so, I think it's worthy of study and understanding.

[0]: https://digama0.github.io/mm0/thesis.pdf

[100]: https://www.cs.ru.nl/~freek/100/

Im not a mathmatician, but in my experience if you are trying to do something novel, you should follow the crowd except for things that impact what you are trying to achieve. Otherwise you spend a lot of extra time sorting through issues on the part that doesn't matter which could be better spent on the novel part.

Occasionally, inspecting that proof term is useful to see what happened in a proof.

Then again, I also like dependent types.

If that momentum is strongest with Lean so be it. At the same time things become more machine verifiable, converting to a new system will also become easier. It can already be strongly assisted using a general agent like Claude Code.

If a green checkmark goes away so be it. AI might or may not understand how to fix it but it's no burden to the user / developer.

> Propositions as types is a duality linking the logical signs ∀ , ∃ , → , ∧ , ∨ with the type constructors Π , Σ , → , × , + . It is beautiful, fascinating and theoretically fruitful, but it is not the only game out there. I have seen “proof assistant”

Firstly, there is value of the attempt. By staying true to constructive logic, there was a lot of progress (compcert verified c compiler, cubical agda etc).

Secondly, there were other confounding variables (tooling, network effects). Claiming rocq lost out to lean due to community's obsession is a bit of reductive argument.

But author is an expert. I will defer to him. His point about sledgehammer approach working well in the new AI world is very interesting though.

Is that enough reason?