There are several proof assistants trying to do what lean is doing (Coq, Isabelle to name but a few). Some of them have very well funded research projects with similar goals: https://cordis.europa.eu/project/id/742178
When programming 'business logic', the multitude of programming languages is a good thing- it allows one to choose the best way to model a problem.
With computer aided proofs, I do wonder if the multitude of systems trying to create a mathematical library of Alexandria is a good thing.
Essentially they're re-formalising the same theorems across different languages. Certainly some languages will model a specific problem better, but it does feel like a duplication of effort.
When programming 'business logic', the multitude of programming languages is a good thing- it allows one to choose the best way to model a problem.
With computer aided proofs, I do wonder if the multitude of systems trying to create a mathematical library of Alexandria is a good thing.
Essentially they're re-formalising the same theorems across different languages. Certainly some languages will model a specific problem better, but it does feel like a duplication of effort.