9 ms·

“Why not just use Lean?”

304 points by ibobev 6mo ago

MarkusQ 6mo ago
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.
- sdenton4 6mo ago
  It depends! Every time you go off the beaten path, you're locking yourself into less documentation, more bugs (since there's less exploration of the dark corners), and fewer people you can go to for help. If you've got 20+ choices to make, picking the standard option is the right choice on average, so you can just do it and move on. You have finite attention, so doing a research report on every dependency means you're never actually working on the core problem. The exceptions to this are when a) it becomes apparent that the standard tool doesn't actually fit your use case, or b) the standard tool significantly overlaps the core problem you're trying to solve.
  - c-linkage 6mo ago
    Which shows the lie of the common engineering trope "use the right tool for the job." It really should be "use the same tool that everyone else is using so you don't have decide which tool is the right one -- the herd made that decision for you!"
  - MarkusQ 6mo ago
    > You have finite attention, so doing a research report on every dependency means you're never actually working on the core problem. Reading that took five minutes and gave a good intro to the counter argument to Curry-Howard-all-the-things monomania. If having invested those five minutes, Lean still seems like the way to go (for whatever reason) fine. You are making a (closer to) informed choice, and likely better off than if you'd spent those five minutes doubling down on the conventional solution. Most deviations from the group consensus are mistakes, but all progress comes from seeing past the group consensus. So making frequent small bets on peeking around your blinders is a good strategy.
- lmm 6mo ago
  Completely disagree; IMO we build far too many frameworks and alternatives (probably because it's fun) instead of a) enhancing the things that already exists to have the thing we want or b) just getting on with the actual work. The whole field would be much better off if we had half as many languages, half as many libraries, half as many build tools...
zermelo44 6mo ago
Good post! +1
kccqzy 6mo ago
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/ 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/Native/Deflate.lean https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...
- readthenotes1 6mo ago
  I recall an experiment in proving software correct from the 1990s that found more errors in the final proof annotations than in the software it had proved correct. Then, I foresee 2 other obstacles, 1 of which may disappear: 1. Actually knowing what the software is supposed to do is hard. Understanding what the users actually want to do and what the customers are paying to do --which aren't necessarily the same thing--is complex 2. The quality of the work of many software developers is abysmal and I don't know why they would be better at a truth language than they are at Java or some other language. Objection 2 may disappear to be replaced with AI systems with the attention to do what needs to be done. So perhaps things will change in that to make it worthwhile...
  - jsmorph 6mo ago
    Re 1: Discussing and guiding the desirable theorems for general-purpose programs has been a major challenge for us. Proofs for their own sake (bad?) vs glorious general results (good but hard?). Actual human guidance there can be critical there at least for now.
  - gr_norm 6mo ago
    Mind linking the experiment? Sounds interesting.
smj-edison 6mo ago
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.
- bowsamic 6mo ago
  This makes it good for formal maths, but bad for philosophy, since it means it can’t encode the speculative movement
  - drdeca 6mo ago
    Which logic are you saying “can’t encode the speculative moment”? I think the two logics can emulate one another? Or, at the very least, can describe what the other concludes. I know intuitionistic logic can have classical logic embedded in it through some sort of “put double negation on everything”. I think if you add some sort of modal operator to classical logic you could probably emulate intuitionistic logic in a similar way?
    - bowsamic 6mo ago
      Any logic with LEM
    - zozbot234 6mo ago
      You don't even need to add a modal operator since modal logic itself can be embedded in classical logic via possible-world semantics. Of course the whole thing becomes a bit clunky - but that's the argument for starting with intuitionistic logic, where you wouldn't need to do that.
groundzeros2015 6mo ago
Type theory and lean is more interesting to people who like computers than to people who like math.
- baq 6mo ago
  citation needed, Tao certainly is on record using Lean and that carries some weight. also, https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... i.e. there's no reason it should be as you say.
  - groundzeros2015 6mo ago
    The link is exactly what I’m saying. I only hear cs people talk about it. For mathematicians a proof is a means to an end, or a medium of expression - they care about what they say and why. The correspondence isn’t about C programs corresponding to proofs in math papers. It’s a very a specific claim about kinds of formal systems which don’t resemble how math or programming is done.
    - gowld 6mo ago
      Mathematicians care about interesting ideas, not whether their theorems are true :-)
      - groundzeros2015 6mo ago
        They care about if it’s true. But the role of the formal proof is a kind of spell checker or static analysis after they have the idea.
        j16sdiz 6mo ago
        > They care about if it’s true. Not always. If it is NOT true, they sometimes simply play "what if" and construct a new system where it could be true.
waffletower 6mo ago
[flagged]
jsmorph 6mo ago
Slightly off topic: This project https://agentcourt.ai/arb/analysis/index.html 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/engine 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 6mo ago
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.
- zozbot234 6mo ago
  > 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". One issue with this is that coming up with a quickly-checkable certificate for UNSAT is not exactly a trivial problem. It's effectively the same as writing a formal proof.
- vintermann 6mo ago
  Last I checked, Isabelle/HOL used a custom Emacs mode as their interface. (I could be mixing it up with one of the other HOLs).
  - c0balt 6mo ago
    The current GUI interface is Isabelle/jedit. Afaik, no Emacs interface is officially provided atm.
- thaumasiotes 6mo ago
shaguoer 6mo ago
[flagged]
gorgoiler 6mo ago
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.
- hutao 6mo ago
  To clarify: ML started out as a scripting language for Robin Milner's proof assistant, LCF. The formal system, or "logic," is implemented in a minimal, trusted kernel, and the proof data structure is protected as an abstract data type that can only be constructed through the trusted kernel. On top of the kernel, tactic scripts may be defined to manipulate proof objects and facilitate proof search/automation. Then, ML grew into a general-purpose programming language (both OCaml and Standard ML are dialects).
nrds 6mo ago
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.
- burakemir 6mo ago
  A proof object in dependent type theory is just the term that inhabits a type. So are you saying the Lean implementation can construct proofs without constructing such a term?
  - nrds 6mo ago
    No, I'm saying it is checked and then discarded. (Or at least, discarded by the kernel. Presumably it ends up somewhere in the frontend's tactic cache.) That matches perfectly the metaphor, "rubs out earlier parts of proofs to make space for later ones". The shared misconception seems to be in believing that because _conceptually_ the theory implemented by Lean builds up a massive proof term, that _operationally_ the Lean kernel must also be doing that. This does not follow. (Even the concept is not quite right since Lean4 is not perfectly referentially transparent in the presence of quotients.)
- vilhelm_s 6mo ago
  Yeah. I guess the abstract type approach saves some memory, but it's a constant factor thing, not an asymptotic improvement. The comment that Lean wastes "tens of megabytes" seems telling: it seems like something that would be a critical advantage in the 1980s and 1990s, when Paulson first fought these battles, but maybe less important today...
rzerowan 6mo ago
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.
- bradleyy 6mo ago
  The two hardest problems in CS: * naming * cache invalidation * off by one errors
- InkCanon 6mo ago
  Wait till you hear what Rocq was originally called!
heliumtera 6mo ago
>The recommended way to install Lean is through VS Code Is that enough reason?
- EFreethought 6mo ago
  Yes. I am tired of my time in tech being just using MS products that all depend on each other.
loglog 6mo ago
"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.
- strbean 6mo ago
  Well, assembly languages are generally Turing complete. Not sure what the parallel would be in proof engines.
  - rowanG077 6mo ago
    [dead]
pstoll 6mo ago
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”.
- ModernMech 6mo ago
  > once you have a community at critical mass around a reasonably good tool, that trumps most other things This matters a lot less in the age of AI. AI doesn't need a massive number of community-built libraries, it can just write its own. It doesn't need a million tutorials floating out there on the interwebs because unlike most programmers, it will actually read the spec and documentation (tutorials are just projections of the docs/spec anyway). AI doesn't have to avoid languages with no job market because it just needs to do the job at hand, not build a career. This makes it easier for small languages and DSLs to gain usage where they never would have before. I think AI might spell the end of the language monoculture (top 20 are mostly slight variations on languages circling the same design) that has persisted in programming.
  - tehjoker 6mo ago
    It's the opposite and has been recognized for years. AI depends on training data and this nearly freezes the use of languages that were popular at the time of inception. Hopefully that is not true. AI needs community libraries if there is to be interoperability and baseline quality between systems. At least at this level of quality and development.
    - ModernMech 6mo ago
      > Hopefully that is not true. I'm here saying this "PL ossification theory" is probably wrong, that it's not going to be the case at all. Yes, AI depends on training data, but that doesn't imply that AI can only use those programming languages or only reason in languages that existed at the time of their training. In fact the AI is able to reason able new languages the same way humans can -- by drawing inferences to the next closest language that it knows, pattern matching to things that are different from other languages, and also figuring out the semantics and reasoning through execution itself where it doesn't have training examples. > AI needs community libraries if there is to be interoperability and baseline quality between systems. Not everyone is looking to do the kind of work you're doing, and that's my point. Up until now, programming languages have been written by and for people who want to do businey/mathy/sciencey things with computers. But there's a huge world out there of other stuff to do with programming languages that have never been considered because the proposition of making languages for those domains is daunting and outside of the wheelhouse of normal people. Now, DSLs are sprouting up where they have no business existing because of AI, just proliferating all over the place. Some of them are going to find communities (of people, AI, or both) and they will flourish completely apart from the systems we are building now in the tech world. It's not going to be the case that AI writes in Python for the rest of time because it writes in and was trained on Python today.
danilafe 6mo ago
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.
- moomin 6mo ago
  Thing is, it comes after both. Maybe it is just being a jack of all trades, but something made it success when the others remain fairly niche.
  - portly 6mo ago
    When I woke up this morning I could not have predicted someone calling a proof assistant a "Jack of all trades"
    - moomin 6mo ago
      “All trades in an extremely specific bounded context”!
  - capitalhilbilly 6mo ago
    I think its pretty clear that being too early has been as bad as being too late for most technologies. There are a few that have gradually gained community after decades but it is easier to make a poor copy of one of them and have better momentum and less skepticism.
- btilly 6mo ago
  In other words, it is a network effect. My perspective is that network effects are far less long-lasting than they feel in the moment. For example if being decent at everything and having a huge community was the only thing that mattered, Perl would still be a big deal. Many similar examples exist. In the case of Lean, being the first with a huge library really makes a difference. Just as Perl got a big boost from having CPAN. (Which was an imitation of CTAN, except for a programming language instead of TeX.) But, based on scaling laws, we should expect the value of a large library for most users to grow around the log of the size of the library. (See https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/docs/others/2005/odlyzko2005a.pdf https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do... for the relevant scaling laws.) When your library is small, this looks like an insurmountable barrier. But you don't have to match the scale for factors of usability to become more important. And porting mathematical libraries is a good target for LLMs. The source is verified, the target is verifiable, and the reasoning path generally ports. The flip side of this is that, thanks to LLMs, working on a minority platform isn't the barrier that you might expect. Because if their library can be ported to your platform, then your proof can probably be ported to their platform as well!
ibobev 6mo ago
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?
- ted_dunning 6mo ago
  Oddly enough, most uses of Lean never actually run the program. The fact that it type checks is enough to prove the theorem in question. That said, if execution is seriously required for your problem along with strong logic on the side, you may prefer Dafny which transpiles the computation part of your proof to C++ or Go.
  - ibobev 6mo ago
    But still, Lean is executable and can be used as an ordinary programming language.
WhitneyLand 6mo ago
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 6mo ago
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.
- icosahedron 6mo ago
  It's a paradigm shift, that's for sure. I'm still in the throes of learning it myself, and it's quite the journey. I love the promises behind it, but I'm not yet far enough along to know if they are kept or if it's just kool aid (or perhaps purple drank?)
  - ifh-hn 6mo ago
    I've never heard of purple drank before, not American. Which came first? The language or drug?
- jojomodding 6mo ago
  Its a software where you type your maths proofs in and a "yes" comes out. Except if your proof is broken, then a "no" comes out. Of course, sometimes the computer is just a bit dumb at intuiting the intermediate steps, so you need to explain like a 10-year-old child (or else you get a "no" as you failed to convince the computer). And storing all these explanations takes memory. And you have to speak the somewhat idiosyncratic language of the computer, which you can imagine a bit like LaTeX but more easily parseable and less ambiguous. The blog article author is saying that Lean is like a younger child (that needs more intermediate steps explained), stores proofs more inefficiently (taking more memory) and that its computer proof language is harder to read for humans. Additionally there is a technical point about dependent types, which are the principle around which the computer proof language is organized (the same way a programming language might be organized around object-orientism).
  - ifh-hn 6mo ago
    Thanks for taking the time to explain, rather than drive by downvote. It doesn't seem like this would be useful to me, or certainly I have no use for it that I can think of.
asdfman123 6mo ago
I am going to build an alternative to Lean called Purple Drank
- bradleyy 6mo ago
  Do not be surprised when I fork and call it Sizzurp.
- asparagui 6mo ago
  I was going to call my project that but Claude said that wasn't professional. rip "a delightful mixture of lean"
red-iron-pine 6mo ago
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 6mo ago
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 https://digama0.github.io/mm0/thesis.pdf [100]: https://www.cs.ru.nl/~freek/100/ https://www.cs.ru.nl/~freek/100/
c7b 6mo ago
Lean isn't the most loved proof assistant by mathematicians, it's not the most suited to formal verification of software, it just sort of works for both. Yet it's got the thing that's arguably the hardest to achieve, momentum. Compounded by the fact that in the AI age, the amount of publicly available human-written code directly affects how well agents can produce new code.
j2kun 6mo ago
If you write an article shitting on a popular thing because it eclipses the popularity of your favorite thing (and essentially calling the people who use it ignorant sheep), chances are good you are part of a self-fulfilling prophecy, pushing people away from your community.
jojomodding 6mo ago
I do not get why not needing proof objects is desirable. It seems good to have a defined way to store proofs that has a very tight spec and can thus have competing implementations, like in https://arena.lean-lang.org/ https://arena.lean-lang.org/. The LCF approach couples the proof format to the module system of a programming language. Occasionally, inspecting that proof term is useful to see what happened in a proof. Then again, I also like dependent types.
- zozbot234 6mo ago
  You can use reflection in dependently-typed proof systems to avoid storing proof objects for expensive computations and replace them with a proof of a general algorithm instead (much like in the LCF approach: the general algorithm proof is the equivalent of a compiler checking that the module system use in a LCF tactic is sound).
BlanketLogic 6mo ago
I think the author is confkating two different things. There are technical problems with sticking to constructive purity when it comes to mathematics (setoid hell, avoiding excluded middle, real number formalization etc). Then there are social aspects. The community's 'cultist' ( his words) adherence to constructive logic. Saying this is the reason rocq lost out to lean seems wrong. 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.
still_grokking 6mo ago
Can someone ELI5 that for me? 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?
- BlanketLogic 6mo ago
  Paulson is a lead developer of Isabelle , a proof assistant that is not based on dependent types. > Is this the mathematician's variant of "my language is better than your language", Almost. A closer analogy is comparing paradigms, say OOP vs functional programming. Isabelle is different from the big three - rocq. lean and agda. The latter three have propositions as types. The type of your function is the theorem statement. The function body is the proof. Isabelle works differently. Author makes a convoluted argument that (a) one doesn't have to stick to the currently popular paradigm and (b) in conjunction with AI, Isabelle offers distinct benefits.
ianhorn 6mo ago
I remember trying to play around with Coq/Rocq and a few others about 15 years ago, and I couldn’t make heads or tails of them. Not the concepts, but the software. What’s weird about proof assistants/interactive provers is that the “interactive” part makes it a combo of IDE and language and they seem to get pretty tightly coupled in practice. You can’t talk about the language without talking about the environment you use it in. 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.
bawolff 6mo ago
> I have been told that when proposing to formalise mathematics these days, you have to explain why you are not using Lean....Amidst the hype around today’s progress, we must remember how we got here. It was not by people following the crowd. 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.
arjunthazhath 6mo ago
[dead]
singularity2001 6mo ago
Formal proofs are made to be done by AI. 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.

304 points by ibobev 6mo ago

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.

sdenton4 6mo ago
It depends! Every time you go off the beaten path, you're locking yourself into less documentation, more bugs (since there's less exploration of the dark corners), and fewer people you can go to for help. If you've got 20+ choices to make, picking the standard option is the right choice on average, so you can just do it and move on. You have finite attention, so doing a research report on every dependency means you're never actually working on the core problem. The exceptions to this are when a) it becomes apparent that the standard tool doesn't actually fit your use case, or b) the standard tool significantly overlaps the core problem you're trying to solve.
- c-linkage 6mo ago
  Which shows the lie of the common engineering trope "use the right tool for the job." It really should be "use the same tool that everyone else is using so you don't have decide which tool is the right one -- the herd made that decision for you!"
- MarkusQ 6mo ago
  > You have finite attention, so doing a research report on every dependency means you're never actually working on the core problem. Reading that took five minutes and gave a good intro to the counter argument to Curry-Howard-all-the-things monomania. If having invested those five minutes, Lean still seems like the way to go (for whatever reason) fine. You are making a (closer to) informed choice, and likely better off than if you'd spent those five minutes doubling down on the conventional solution. Most deviations from the group consensus are mistakes, but all progress comes from seeing past the group consensus. So making frequent small bets on peeking around your blinders is a good strategy.
lmm 6mo ago
Completely disagree; IMO we build far too many frameworks and alternatives (probably because it's fun) instead of a) enhancing the things that already exists to have the thing we want or b) just getting on with the actual work. The whole field would be much better off if we had half as many languages, half as many libraries, half as many build tools...

zermelo44 6mo ago

Good post! +1

kccqzy 6mo ago

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/ 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/Native/Deflate.lean https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

readthenotes1 6mo ago
I recall an experiment in proving software correct from the 1990s that found more errors in the final proof annotations than in the software it had proved correct. Then, I foresee 2 other obstacles, 1 of which may disappear: 1. Actually knowing what the software is supposed to do is hard. Understanding what the users actually want to do and what the customers are paying to do --which aren't necessarily the same thing--is complex 2. The quality of the work of many software developers is abysmal and I don't know why they would be better at a truth language than they are at Java or some other language. Objection 2 may disappear to be replaced with AI systems with the attention to do what needs to be done. So perhaps things will change in that to make it worthwhile...
- jsmorph 6mo ago
  Re 1: Discussing and guiding the desirable theorems for general-purpose programs has been a major challenge for us. Proofs for their own sake (bad?) vs glorious general results (good but hard?). Actual human guidance there can be critical there at least for now.
- gr_norm 6mo ago
  Mind linking the experiment? Sounds interesting.

smj-edison 6mo ago

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.

bowsamic 6mo ago
This makes it good for formal maths, but bad for philosophy, since it means it can’t encode the speculative movement
- drdeca 6mo ago
  Which logic are you saying “can’t encode the speculative moment”? I think the two logics can emulate one another? Or, at the very least, can describe what the other concludes. I know intuitionistic logic can have classical logic embedded in it through some sort of “put double negation on everything”. I think if you add some sort of modal operator to classical logic you could probably emulate intuitionistic logic in a similar way?
  - bowsamic 6mo ago
    Any logic with LEM
  - zozbot234 6mo ago
    You don't even need to add a modal operator since modal logic itself can be embedded in classical logic via possible-world semantics. Of course the whole thing becomes a bit clunky - but that's the argument for starting with intuitionistic logic, where you wouldn't need to do that.

groundzeros2015 6mo ago

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

baq 6mo ago
citation needed, Tao certainly is on record using Lean and that carries some weight. also, https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... i.e. there's no reason it should be as you say.
- groundzeros2015 6mo ago
  The link is exactly what I’m saying. I only hear cs people talk about it. For mathematicians a proof is a means to an end, or a medium of expression - they care about what they say and why. The correspondence isn’t about C programs corresponding to proofs in math papers. It’s a very a specific claim about kinds of formal systems which don’t resemble how math or programming is done.
  - gowld 6mo ago
    Mathematicians care about interesting ideas, not whether their theorems are true :-)
    - groundzeros2015 6mo ago
      They care about if it’s true. But the role of the formal proof is a kind of spell checker or static analysis after they have the idea.
      - j16sdiz 6mo ago
        > They care about if it’s true. Not always. If it is NOT true, they sometimes simply play "what if" and construct a new system where it could be true.

waffletower 6mo ago

[flagged]

jsmorph 6mo ago

Slightly off topic: This project https://agentcourt.ai/arb/analysis/index.html 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/engine 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 6mo ago

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.

zozbot234 6mo ago
> 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". One issue with this is that coming up with a quickly-checkable certificate for UNSAT is not exactly a trivial problem. It's effectively the same as writing a formal proof.
vintermann 6mo ago
Last I checked, Isabelle/HOL used a custom Emacs mode as their interface. (I could be mixing it up with one of the other HOLs).
- c0balt 6mo ago
  The current GUI interface is Isabelle/jedit. Afaik, no Emacs interface is officially provided atm.
thaumasiotes 6mo ago

shaguoer 6mo ago

[flagged]

gorgoiler 6mo ago

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.

hutao 6mo ago
To clarify: ML started out as a scripting language for Robin Milner's proof assistant, LCF. The formal system, or "logic," is implemented in a minimal, trusted kernel, and the proof data structure is protected as an abstract data type that can only be constructed through the trusted kernel. On top of the kernel, tactic scripts may be defined to manipulate proof objects and facilitate proof search/automation. Then, ML grew into a general-purpose programming language (both OCaml and Standard ML are dialects).

nrds 6mo ago

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.

burakemir 6mo ago
A proof object in dependent type theory is just the term that inhabits a type. So are you saying the Lean implementation can construct proofs without constructing such a term?
- nrds 6mo ago
  No, I'm saying it is checked and then discarded. (Or at least, discarded by the kernel. Presumably it ends up somewhere in the frontend's tactic cache.) That matches perfectly the metaphor, "rubs out earlier parts of proofs to make space for later ones". The shared misconception seems to be in believing that because _conceptually_ the theory implemented by Lean builds up a massive proof term, that _operationally_ the Lean kernel must also be doing that. This does not follow. (Even the concept is not quite right since Lean4 is not perfectly referentially transparent in the presence of quotients.)
vilhelm_s 6mo ago
Yeah. I guess the abstract type approach saves some memory, but it's a constant factor thing, not an asymptotic improvement. The comment that Lean wastes "tens of megabytes" seems telling: it seems like something that would be a critical advantage in the 1980s and 1990s, when Paulson first fought these battles, but maybe less important today...

rzerowan 6mo ago

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.

bradleyy 6mo ago
The two hardest problems in CS: * naming * cache invalidation * off by one errors
InkCanon 6mo ago
Wait till you hear what Rocq was originally called!

heliumtera 6mo ago

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

EFreethought 6mo ago
Yes. I am tired of my time in tech being just using MS products that all depend on each other.

loglog 6mo ago

"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.

strbean 6mo ago
Well, assembly languages are generally Turing complete. Not sure what the parallel would be in proof engines.
- rowanG077 6mo ago
  [dead]

pstoll 6mo ago

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”.

ModernMech 6mo ago
> once you have a community at critical mass around a reasonably good tool, that trumps most other things This matters a lot less in the age of AI. AI doesn't need a massive number of community-built libraries, it can just write its own. It doesn't need a million tutorials floating out there on the interwebs because unlike most programmers, it will actually read the spec and documentation (tutorials are just projections of the docs/spec anyway). AI doesn't have to avoid languages with no job market because it just needs to do the job at hand, not build a career. This makes it easier for small languages and DSLs to gain usage where they never would have before. I think AI might spell the end of the language monoculture (top 20 are mostly slight variations on languages circling the same design) that has persisted in programming.
- tehjoker 6mo ago
  It's the opposite and has been recognized for years. AI depends on training data and this nearly freezes the use of languages that were popular at the time of inception. Hopefully that is not true. AI needs community libraries if there is to be interoperability and baseline quality between systems. At least at this level of quality and development.
  - ModernMech 6mo ago
    > Hopefully that is not true. I'm here saying this "PL ossification theory" is probably wrong, that it's not going to be the case at all. Yes, AI depends on training data, but that doesn't imply that AI can only use those programming languages or only reason in languages that existed at the time of their training. In fact the AI is able to reason able new languages the same way humans can -- by drawing inferences to the next closest language that it knows, pattern matching to things that are different from other languages, and also figuring out the semantics and reasoning through execution itself where it doesn't have training examples. > AI needs community libraries if there is to be interoperability and baseline quality between systems. Not everyone is looking to do the kind of work you're doing, and that's my point. Up until now, programming languages have been written by and for people who want to do businey/mathy/sciencey things with computers. But there's a huge world out there of other stuff to do with programming languages that have never been considered because the proposition of making languages for those domains is daunting and outside of the wheelhouse of normal people. Now, DSLs are sprouting up where they have no business existing because of AI, just proliferating all over the place. Some of them are going to find communities (of people, AI, or both) and they will flourish completely apart from the systems we are building now in the tech world. It's not going to be the case that AI writes in Python for the rest of time because it writes in and was trained on Python today.

danilafe 6mo ago

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.

moomin 6mo ago
Thing is, it comes after both. Maybe it is just being a jack of all trades, but something made it success when the others remain fairly niche.
- portly 6mo ago
  When I woke up this morning I could not have predicted someone calling a proof assistant a "Jack of all trades"
  - moomin 6mo ago
    “All trades in an extremely specific bounded context”!
- capitalhilbilly 6mo ago
  I think its pretty clear that being too early has been as bad as being too late for most technologies. There are a few that have gradually gained community after decades but it is easier to make a poor copy of one of them and have better momentum and less skepticism.
btilly 6mo ago
In other words, it is a network effect. My perspective is that network effects are far less long-lasting than they feel in the moment. For example if being decent at everything and having a huge community was the only thing that mattered, Perl would still be a big deal. Many similar examples exist. In the case of Lean, being the first with a huge library really makes a difference. Just as Perl got a big boost from having CPAN. (Which was an imitation of CTAN, except for a programming language instead of TeX.) But, based on scaling laws, we should expect the value of a large library for most users to grow around the log of the size of the library. (See https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/docs/others/2005/odlyzko2005a.pdf https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do... for the relevant scaling laws.) When your library is small, this looks like an insurmountable barrier. But you don't have to match the scale for factors of usability to become more important. And porting mathematical libraries is a good target for LLMs. The source is verified, the target is verifiable, and the reasoning path generally ports. The flip side of this is that, thanks to LLMs, working on a minority platform isn't the barrier that you might expect. Because if their library can be ported to your platform, then your proof can probably be ported to their platform as well!

ibobev 6mo ago

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?

ted_dunning 6mo ago
Oddly enough, most uses of Lean never actually run the program. The fact that it type checks is enough to prove the theorem in question. That said, if execution is seriously required for your problem along with strong logic on the side, you may prefer Dafny which transpiles the computation part of your proof to C++ or Go.
- ibobev 6mo ago
  But still, Lean is executable and can be used as an ordinary programming language.

WhitneyLand 6mo ago

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 6mo ago

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.

icosahedron 6mo ago
It's a paradigm shift, that's for sure. I'm still in the throes of learning it myself, and it's quite the journey. I love the promises behind it, but I'm not yet far enough along to know if they are kept or if it's just kool aid (or perhaps purple drank?)
- ifh-hn 6mo ago
  I've never heard of purple drank before, not American. Which came first? The language or drug?
jojomodding 6mo ago
Its a software where you type your maths proofs in and a "yes" comes out. Except if your proof is broken, then a "no" comes out. Of course, sometimes the computer is just a bit dumb at intuiting the intermediate steps, so you need to explain like a 10-year-old child (or else you get a "no" as you failed to convince the computer). And storing all these explanations takes memory. And you have to speak the somewhat idiosyncratic language of the computer, which you can imagine a bit like LaTeX but more easily parseable and less ambiguous. The blog article author is saying that Lean is like a younger child (that needs more intermediate steps explained), stores proofs more inefficiently (taking more memory) and that its computer proof language is harder to read for humans. Additionally there is a technical point about dependent types, which are the principle around which the computer proof language is organized (the same way a programming language might be organized around object-orientism).
- ifh-hn 6mo ago
  Thanks for taking the time to explain, rather than drive by downvote. It doesn't seem like this would be useful to me, or certainly I have no use for it that I can think of.

asdfman123 6mo ago

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

bradleyy 6mo ago
Do not be surprised when I fork and call it Sizzurp.
asparagui 6mo ago
I was going to call my project that but Claude said that wasn't professional. rip "a delightful mixture of lean"

red-iron-pine 6mo ago

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 6mo ago

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 https://digama0.github.io/mm0/thesis.pdf [100]: https://www.cs.ru.nl/~freek/100/ https://www.cs.ru.nl/~freek/100/

c7b 6mo ago

Lean isn't the most loved proof assistant by mathematicians, it's not the most suited to formal verification of software, it just sort of works for both. Yet it's got the thing that's arguably the hardest to achieve, momentum. Compounded by the fact that in the AI age, the amount of publicly available human-written code directly affects how well agents can produce new code.

j2kun 6mo ago

If you write an article shitting on a popular thing because it eclipses the popularity of your favorite thing (and essentially calling the people who use it ignorant sheep), chances are good you are part of a self-fulfilling prophecy, pushing people away from your community.

jojomodding 6mo ago

I do not get why not needing proof objects is desirable. It seems good to have a defined way to store proofs that has a very tight spec and can thus have competing implementations, like in https://arena.lean-lang.org/ https://arena.lean-lang.org/. The LCF approach couples the proof format to the module system of a programming language. Occasionally, inspecting that proof term is useful to see what happened in a proof. Then again, I also like dependent types.

zozbot234 6mo ago
You can use reflection in dependently-typed proof systems to avoid storing proof objects for expensive computations and replace them with a proof of a general algorithm instead (much like in the LCF approach: the general algorithm proof is the equivalent of a compiler checking that the module system use in a LCF tactic is sound).

BlanketLogic 6mo ago

I think the author is confkating two different things. There are technical problems with sticking to constructive purity when it comes to mathematics (setoid hell, avoiding excluded middle, real number formalization etc). Then there are social aspects. The community's 'cultist' ( his words) adherence to constructive logic. Saying this is the reason rocq lost out to lean seems wrong. 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.

still_grokking 6mo ago

Can someone ELI5 that for me? 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?

BlanketLogic 6mo ago
Paulson is a lead developer of Isabelle , a proof assistant that is not based on dependent types. > Is this the mathematician's variant of "my language is better than your language", Almost. A closer analogy is comparing paradigms, say OOP vs functional programming. Isabelle is different from the big three - rocq. lean and agda. The latter three have propositions as types. The type of your function is the theorem statement. The function body is the proof. Isabelle works differently. Author makes a convoluted argument that (a) one doesn't have to stick to the currently popular paradigm and (b) in conjunction with AI, Isabelle offers distinct benefits.

ianhorn 6mo ago

I remember trying to play around with Coq/Rocq and a few others about 15 years ago, and I couldn’t make heads or tails of them. Not the concepts, but the software. What’s weird about proof assistants/interactive provers is that the “interactive” part makes it a combo of IDE and language and they seem to get pretty tightly coupled in practice. You can’t talk about the language without talking about the environment you use it in. 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.

bawolff 6mo ago

> I have been told that when proposing to formalise mathematics these days, you have to explain why you are not using Lean....Amidst the hype around today’s progress, we must remember how we got here. It was not by people following the crowd. 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.

arjunthazhath 6mo ago

[dead]

singularity2001 6mo ago

Formal proofs are made to be done by AI. 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.