Isabelle contributor argues formal mathematics predates Lean by 60 years and Isabelle offers superior automation, legibility, and avoids dependent-type complexity.
Key Takeaways
AUTOMATH (NG de Bruijn, 1968) and Jutting’s 1977 formalization of Landau’s Foundations of Analysis predate Lean; the claim Lean made formalization possible is false.
Lean’s community growth traces to Tom Hales’ Lean library initiative and Kevin Buzzard adopting it for teaching, not a technical breakthrough over rivals.
Lean gained ground on Rocq by dropping the “constructive proofs” requirement that had dominated Rocq’s culture and blocked mainstream mathematics use.
The LCF insight (Robin Milner): proof objects are unnecessary; ML abstract data types check proofs dynamically, avoiding the memory waste of storing giant proof terms.
Isabelle’s sledgehammer outclasses any comparable automation; AI-generated proofs pair well with it, and legible structured proofs can be translated across systems by language models.
