Beyond the Lean Hype: Formal Mathematics' Six-Decade Heritage

While Lean now dominates formal mathematics discourse, the field has evolved over 60 years since AUTOMATH's emergence in 1968, with HOL, LCF, and ACL2 making significant contributions. The current hype risks obscuring the pioneering work and diverse methodologies that enabled today's progress, underscoring how transformative breakthroughs emerge from independent thinking rather than following prevailing trends.