Why not use Lean?

I have been told that when proposing to formalise mathematics these days, you have to explain why you are not using Lean. And that reminds me why I left the dependent-typed world 40 years ago: its cultism, insularity and conformity. Lean is a great language with good tools, a large library and a huge, enthusiastic user community that has lately accomplished astounding things. But let’s not forget that the formalisation of mathematics goes back nearly 60 years. Amidst the hype around today’s progress, we must remember how we got here. It was not by people following the crowd. In the beginning, there was AUTOMATH Part of the hype mentioned above is the frequent claim “Lean has made the formalisation of mathematics possible”. Sorry, we got there in 1968. NG de Bruijn’s AUTOMATH already included most of the necessary ingredients. By 1977, Jutting had used it to formalise Landau’s Foundations of Analysis, which covers the construction of the complex numbers starting from pure logic.…