“Why not just use Lean?”

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.