"Why not just use Lean?"

Lawrence Paulson argues that while Lean has become dominant in formalizing mathematics, the field's actual history spans nearly 60 years. He traces crucial foundations in earlier systems like AUTOMATH (1968) and HOL Light, warning against overlooking this context amidst current Lean enthusiasm.