How does Lean compare to other formalized math?

Stream: general

[Jin]

HI! I'm glad people have been working hard on formalizing mathematics. One thing confuses me however.. I wonder why don't people stay in one framework, and just contribute to that. Right now, there are many frameworks for formalizing mathematics.. as a programming newbie.. I don't really see why that's the case. Wouldn't it be better if everyone can concentrate on ONE AND ONLY ONE framework, so all efforts add together?

[Mario Carneiro]

Why do multiple programming languages exist? Part of the problem is that we have not yet collectively found the best way to do things, so there are lots of experiments trying to see if some proposed improvement can really deliver. There are also a number of philosophical differences among the major libraries. But really, I would say that there is quite a bit of gravity toward big projects, and there are at most 5 or 6 big projects out there as opposed to hundreds (although that can be also blamed on the overall small user base of formal theorem provers)

[Mario Carneiro]

On an individual level, I would say that most people invest in learning one language and use only it, championing the language as the one to rule the world eventually

[Reid Barton]

Relevant xkcd: https://xkcd.com/927/