Why not just use Lean?
Summary
The article surveys the history of formalising mathematics from AUTOMATH to Lean and Isabelle, arguing that no single system owns the domain and that AI-assisted tooling will shape the future of formal proofs. It discusses the trade-offs of dependent types, proof objects, and readability, and advocates for Isabelle's balance of automation and legibility while acknowledging the Lean community. It also highlights how AI and cross-system translation could democratise formal mathematics.