# Lean 4 268 Hacker News commenters recommended Lean 4 and 100 criticized it, November 2025 to November 2026. It was recommended in 13 of 13 months; owners who said how long report a median of 1 years (6 owners). It meets the Hacker Approved badge rule. **Verdict:** A proof assistant and full functional language that pairs well with AI, whose small trusted kernel makes proofs highly reliable; critics cite slow checking and quirky general-purpose use. ## Why people recommend it - Trustworthy machine-checked proofs (6 comments): "The drudgery of mechanically applying logical rules is pushed onto the Lean kernel which is trusted, while the Human can concentrate on semantic correctness" ([source](https://news.ycombinator.com/item?id=50031648)) "A Lean proof has a much higher probability of being correct (in my opinion) than any published (either preprint or peer-reviewed) paper" ([source](https://news.ycombinator.com/item?id=50003650)) "the "core" of Lean is a somewhat "simple" core that does simple things to check the proof, so it's quite rare to find meaningful bugs" ([source](https://news.ycombinator.com/item?id=50329087)) - Works well with AI assistants (7 comments): "I use Lean and occasionally some other languages with expressive type systems, and like you I've found it to be a pretty great experience for working with LLMs" ([source](https://news.ycombinator.com/item?id=48860528)) "Let the LLM solve the nitty gritty details of proof, but use the higher-level theorem formation as the vessel for doing great things." ([source](https://news.ycombinator.com/item?id=46210532)) "the quick feedback loop between the AI prose and the Lean verification errors and warnings ensures that its logically consistent" ([source](https://news.ycombinator.com/item?id=48975530)) - Full general-purpose programming language (6 comments): "Lean 4 is a language supporting verification, and it's also a full programming language, so you can write your proofs/theorems in the same language that you program in." ([source](https://news.ycombinator.com/item?id=46297045)) "Lean feels like it could legitimately become a successor to Haskell as the go to functional programming language for software development." ([source](https://news.ycombinator.com/item?id=47927756)) "One of the things I like about Lean is precisely that it's an ordinary, Haskell-style functional programming language" ([source](https://news.ycombinator.com/item?id=47245222)) - Powerful dependent type system (4 comments): "it's type system is insanely powerful, indexed dependant inductive and quotient types allow the realization of "making invalid states unrepresentable"" ([source](https://news.ycombinator.com/item?id=49324671)) "It's dependent-types / theorem-proving-oriented type-system combined with AI assistants makes it the language of the future IMO." ([source](https://news.ycombinator.com/item?id=46108085)) "LEAN is a functional programming language with a type system strong enough to express cutting-edge mathematics" ([source](https://news.ycombinator.com/item?id=49369405)) ## What people warn about - Slow, unpredictable proof checking (3 comments): "Caching only works until you change a deeply nested constant. Then you must wait 2 hours as Lean re-checks every transitive dependency" ([source](https://news.ycombinator.com/item?id=49754441)) "The slowness is relatively unpredictable, too: sometimes changing a 'rewrite' to a 'with' can increase memory usage tenfold." ([source](https://news.ycombinator.com/item?id=47928624)) "Lean is apparently so slow that for Fermat's Last Theorem proof verification runs only 1 order of magnitude faster" ([source](https://news.ycombinator.com/item?id=49650628)) - Quirky outside of mathematics (3 comments): "using Lean to model things humans care about (business logic, user interfaces, physical environments, dynamic regulations) quickly hits a dead end" ([source](https://news.ycombinator.com/item?id=47099509)) "It's a great language for math, perhaps the best choice right now. But as a general purpose language it's incredibly quirky." ([source](https://news.ycombinator.com/item?id=47766899)) "Lean is line noise. It's like assembly language for math, which is great, but not what humans should be using day to day." ([source](https://news.ycombinator.com/item?id=46384636)) - Kernel and runtime bugs exist (3 comments): "The core of Lean got a lot less correct when a well-meaning AI system probed Lean for corner cases (bugs) that would "prove" a false conjecture." ([source](https://news.ycombinator.com/item?id=49368318)) "The main bug found was actually in the lean runtime, affecting all proofs using scalar arrays where the size of the array is not bounded." ([source](https://news.ycombinator.com/item?id=47760387)) "the Lean kernel has a lot of fancy features that aren't yet perfectly understood from a type-theoretic perspective" ([source](https://news.ycombinator.com/item?id=49323510)) - Weak libraries for program reasoning (3 comments): "Lean's just a little bit too focused on talking about results to tidily talk about how those results are computed." ([source](https://news.ycombinator.com/item?id=49836832)) "the main downside with Lean is that libraries for reasoning about program logic are comparatively less developed" ([source](https://news.ycombinator.com/item?id=49940161)) "Using LEAN or Coq requires you to basically convert your code to LEAN/Coq before you can start proving anything" ([source](https://news.ycombinator.com/item?id=47117373)) ## Alternatives hackers recommend - [Rocq](https://hackerapproved.com/p/rocq.md): 25 recommend - [Coq](https://hackerapproved.com/p/coq.md): 24 recommend - [Agda](https://hackerapproved.com/p/agda.md): 19 recommend - [Isabelle](https://hackerapproved.com/p/isabelle.md): 14 recommend - [Metamath](https://hackerapproved.com/p/metamath.md): 14 recommend ## Cite as Hacker Approved, "Lean 4", https://hackerapproved.com/p/lean/ (counts from 1,795,640 Hacker News comments, November 2025 to November 2026).