“Why not just use Lean?”

MarkusQ

We need more of this. 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.

zermelo44

Good post! +1

kccqzy

For the HN crowd who are generally programmers but not necessarily mathematicians, it’s more relevant to consider the programming side of things. There is a very good book (one I haven’t finished unfortunately) that covers Lean from a functional programming perspective rather than proving mathematics perspective: https://leanprover.github.io/functional_programming_in_lean/ 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...

smj-edison

I think what's interesting about Lean is that Lean is a language, and what most people are talking about is a library called Mathlib. From what I've read about Mathlib, the creators are very pragmatic, which is why they encode classical logic in Lean types, with only a bit of intuitionistic logic[1]. [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.

groundzeros2015

Type theory and lean is more interesting to people who like computers than to people who like math.

jsmorph

Slightly off topic: This project https://agentcourt.ai/arb/analysis/index.html uses a Go/Lean hybrid design. The Go code is mostly glue, and the Lean code is the logic https://github.com/agentcourt/adjudication/tree/main/arb/eng... . It's not math-intensive. Really just functional programming with some interesting proofs (including soundness ideally). Go code can migrate to Lean code when that makes sense.

c0balt

Isabelle/HOL as a language is nice, but the tooling has deep flaws even outside the pure desktop-first app approach. 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.

gorgoiler

It’s been decades since I could claim to know anything about this field so I’m probably completely wrong in how I read this, but the idea that one might build a theorem prover (“ML!”) for one’s non-ML programming language and have the prover itself accidentally be a really good general purpose programming language … is very funny.

nrds

The author appears to have a serious misconception about Lean, which is surprising since he seems to be quite knowledgeable in the area. 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.

rzerowan

One of those names that forces a double take when seen disconnected from context: '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.

heliumtera

>The recommended way to install Lean is through VS Code Is that enough reason?

loglog

"I believe that almost anything that has been formalised today in any system could have been formalised in AUTOMATH. Its main drawbacks were its notation, which really was horrible, and its complete lack of automation. Proofs were long and unreadable." That's like saying that anything that could be programmed today in your modern language of choice could have been programmed 50 years ago in assembly. Technically yes, economically no.

pstoll

Feels like all the write ups that point out the short comings of eg Python for scientific computing. 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”.

danilafe

People tell me Lean is really good for functional programming. However, coming from Agda, it feels like a pretty clunky downgrade. They also tell me it's good for tactics, but I've found Coq's tactics more powerful and ergonomic. Maybe these are all baby-duck perceptions. So far, it feels like Lean's main strength isn't being the best at anything, but being decent at everything and having a huge community. I see the point and appeal, but it's saddens me that a bit of the beauty and power are lost in exchange.

ibobev

What about the performance characteristics of the Lean programs? I know it is a natively compiled language, but is the code it produces comparable to that of modern system programming languages in terms of performance?

WhitneyLand

The most important thing is keeping up the momentum to formalize more proofs and continue to strengthen the libraries and foundational work. 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.

ifh-hn

I keep seeing articles about Lean recently on HN. Never heard of it before. I'm not a mathematician and not a professional developer so my opinion might not mean shit, but I can't make head nor tail of it. I can't understand what half of what the website is talking about.

asdfman123

I am going to build an alternative to Lean called Purple Drank

red-iron-pine

ngl assumed this was about supply management or purple drank > 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”

raphlinus

People interested in alternatives to Lean should also look at Metamath. It has nowhere near the adoption that Lean is getting, but is holding its own in [100] theorems results. 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/