HN

Comments (113)

• Menu

  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...
• Menu

  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.
• 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.
• Menu

  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.
• Menu

  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.
• Menu

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

  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.
• Menu

  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.
• 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?
• Menu

  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.
• 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.
• 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.
• shaguoer
  Interesting perspective. Would love to see more discussion.
• heliumtera
  >The recommended way to install Lean is through VS CodeIs that enough reason?
• waffletower
  [flagged]
• zermelo44
  Good post! +1
• Menu

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