Hacker News Reader

That's a bad analogy. LEAN is a leading bleeding edge proof verification tool.

Fortran used to be the only programming language (and even cutting edge by default). People went off and created new ones anyway.

And maybe somebody will create something better than LEAN. That has nothing to do with the original argument.