"Why not just use Lean?"
This title could be clearer and more informative.Try out Clickbait Shieldfor free (5 uses left this month).
A veteran researcher in formal mathematics pushes back against the assumption that Lean is the only viable proof assistant, tracing the 60-year history of formalised mathematics from AUTOMATH (1968) through Boyer-Moore, LCF, HOL, Coq/Rocq, and Isabelle. The post argues that Lean's dominance reflects community momentum rather than technical superiority, highlights Isabelle's advantages (best automation via sledgehammer, legible proofs, no dependent types), critiques the 'propositions as types' monoculture, and notes that AI-assisted proving may eventually make the choice of proof assistant less consequential.
Table of contents
In the beginning, there was AUTOMATHAnd just after, there were Boyer and MooreAfter LCF: Coq, HOL and IsabelleThe emergence of the Lean communityNot everything is “propositions as types”LCF (again): we don’t need proof objects!Why should you use Isabelle?To the futureMizar, with apologiesSort: