A veteran formal methods researcher pushes back against the prevailing assumption that Lean is the only serious choice for formalizing mathematics. AUTOMATH, developed by N.G. de Bruijn in 1968, already contained most ingredients needed for formal proof — and by 1977, Jutting had used it to formalize Landau's Foundations of Analysis, proving Dedekind completeness of the real number line. That accomplishment went unmatched for 20 years.

The author argues that the Lean community's dominance stems partly from abandoning Rocq's "constructive proof" obsession, which hindered its application to mainstream mathematics. Other systems like ACL2 (from Boyer and Moore's computational logic) and HOL Light (where John Harrison proved the prime number theorem) took different paths and achieved remarkable results. The LCF approach, which uses abstract data types rather than storing massive proof terms, remains theoretically sound.

The piece concludes that "propositions as types" — the duality linking logical connectives to type constructors — is beautiful but not the only valid framework. AUTOMATH itself wasn't an instance of it, and de Bruijn understood 50 years ago that keeping types and propositions distinct was necessary for practical formalization.