“Why not just use Lean?”

Original Article ↗ Hacker News Discussion ↗

Lean, a popular interactive theorem prover and functional programming language, is drawing scrutiny from users of older systems like Isabelle/HOL who argue that dependent types, heavy tooling, and opaque automation aren’t obviously superior to more traditional LCF-style designs. Commenters weigh tradeoffs between constructive vs. classical logic, proof objects vs. abstract proof kernels, and the risks of increasingly automated, SMT/AI-driven proofs that humans can’t easily understand or maintain. Many conclude that Lean’s real advantage is momentum, ecosystem, and VS Code–based tooling rather than any clear technical dominance, while noting that AI could both erode current network effects and make translation between proof systems easier in the future.

Lean vs Other Proof Assistants

  • Many see Lean’s main strength as being “good enough at everything” (math + software verification + FP) plus having strong momentum and libraries (e.g., Mathlib, emerging CSLib), not technical purity.
  • Comparisons:
    • Isabelle/HOL: praised for LCF-style architecture and Sledgehammer; criticized for tooling, RAM use, and community interactions. Some think Lean could grow similar automation (grind vs Sledgehammer).
    • Coq/Rocq, Agda, Idris: some users find them more elegant or powerful (e.g., pattern matching, dependent types), but Lean wins on tooling, ergonomics, and community.
    • Other systems mentioned: Dafny, F*, Ada/SPARK, Metamath, TLA+, SeL4/CompCert as success stories for formal verification outside Lean.

Logic Foundations: Classical vs Constructive

  • Thread debates classical vs intuitionistic/constructive logic:
    • Classical logic: uses law of excluded middle (LEM), non-constructive existence proofs; convenient for mainstream math but less tied to computation.
    • Intuitionistic/constructive logic: proofs correspond to explicit constructions; better aligned with programming and data types (Curry–Howard, tagged unions, etc.).
  • Some argue intuitionism is a refinement that surfaces computational content; others say most CS/maths work effectively uses classical logic and gains little by forbidding LEM.
  • Multiple comments correct misunderstandings (LEM vs non-contradiction, what “proof by contradiction” means in each logic).

Practicality, Tooling, and Community

  • Strong sentiment that standardizing on one widely used tool is pragmatic: better docs, fewer bugs, more help, and less decision overhead.
  • Counterpoint: blindly following the herd stifles innovation; small exploratory bets on alternatives are valuable.
  • VS Code–centric onboarding is both praised (smooth interactive experience) and disliked (Microsoft dependency, installation friction; some prefer Emacs/Neovim).
  • Lean’s syntax extensibility and tactics are viewed as powerful but potentially leading to DSL sprawl and opaque proofs.

AI, Automation, and Future Dynamics

  • Several see proof assistants as a natural workload for AI: formal proofs are checkable, and AI can generate or port libraries across systems.
  • Others worry about opaque, AI-generated proofs becoming incomprehensible, especially when SMT/automation gives “ticks” that later break.
  • Debate over whether AI will reinforce dominant tools (due to training data) or weaken network effects by making smaller languages and DSLs more viable.