Likely Isabelle’s creator argues Lean’s dominance erases 60 years of proof assistant history and makes the technical case for Isabelle over dependent-typed systems.
Key Takeaways
AUTOMATH (1968) already contained most formalization ingredients; Jutting proved Dedekind completeness of the reals in 1977, decades before Lean existed.
The LCF approach (ML abstract data types, dynamic proof checking, no proof objects) is architecturally distinct from propositions-as-types and predates it by 50 years.
Lean’s community dominance came from abandoning Rocq’s constructive-proof obsession and from Tom Hales + Kevin Buzzard building a library and teaching culture around it, not from technical superiority.
Isabelle’s sledgehammer tactic has no peer; AI-generated proofs (including Claude-assisted ones) clean up well against it and remain human-readable.
Dependent types force undecidable type-checking; the intensional-equality workaround (where T(N+1) and T(1+N) are distinct types) creates real proof burdens that Isabelle avoids entirely.
Hacker News Comment Review
The most substantive pushback challenges a core technical claim: commenters assert Lean already implements proof-object elimination equivalent to the LCF optimization, making the “RAMmageddon” waste argument factually contested.
The Python parallel recurred across comments: once a tool reaches critical mass with evangelists like Terence Tao, technical shortcomings stop mattering; Lean may already be past escape velocity.
The Lean-vs-Mathlib distinction drew real discussion: Lean the language makes pragmatic tradeoffs, but Mathlib’s deliberate adoption of classical logic (law of excluded middle) is where the mathematical power actually comes from.
Notable Comments
@nrds: Directly refutes the proof-object waste claim, arguing Lean implements the same kernel optimization as LCF and does not retain large proof terms.
@ianhorn: Notes that Lean’s VS Code extension solved the IDE-coupling problem that made Coq/Rocq inaccessible for 15 years, a tooling advantage the post underweights.